Frama-C-discuss mailing list archives

yannick.moy at gmail.com (Yannick Moy) · Thu, 12 Nov 2009 12:25:56 +0100

Being familiar with both Frama-C (I worked on the Jessie plugin during my
PhD) and SPARK (I am currently working at AdaCore on proof tools, together
with Praxis people), I can give you my personal feeling for this.

First, Frama-C has a wider range of applications than the SPARK tools, which
focus on modular program verification. So it makes more sense to compare the
Jessie plugin of Frama-C with the SPARK toolset. Then, I could summarize the
differences between the two by saying that Frama-C offers a more powerful
specification language (ACSL) and tools (SMT solvers, theorem provers) while
SPARK offers a more controlled way of expressing programs that simplifies
their verification.

More precisely:
1) The programming languages analyzed are semantically very different, not
even mentioning the well-definedness issue raised by Pascal Cuoq. C has the
full power of pointers, aliasing and access to raw memory through casts,
while SPARK has simple references, it syntactically enforces non-aliasing
and memory is statically strongly typed. Thus, it is possible to code in C
at different levels, using or not aliasing and casts, which allows to make
some assumptions that facilitate the verification. Those assumptions are
always true in SPARK. The Jessie plugin of Frama-C supports aliasing but it
does not support pointer casts. People in CEA explore currently various
memory models for C that allow or not aliasing and/or casts, which lead to
different Verification Conditions to prove. With SPARK, all equivalent low
level operations are done in the subset of Ada outside of SPARK, in parts of
the code that are marked #hide, and thus ignored by the tools.

2) The specification languages are quite different too. ACSL allows
expressing axiomatizations directly at the level of the C program, while
SPARK only allows declaring proof functions, which must be axiomatized with
Prolog rewrite rules in a separate file. SPARK defines #own variables that
are used for hiding and refinement. ACSL defines state labels that can be
used to denote a program point in logic functions and predicates. To answer
a question in a following email, both are supersets of first-order logic,
but quite different from each other.

3) The tools are very different. The SPARK Examiner enforces that no
uninitialized memory is read, as well as data-flow properties if instructed
to do so. No proof is performed here, it is a "simple" static analysis. The
SPARK Simplifier is based on a Prolog engine tailored for the Verification
Conditions produced by the Examiner, that attempts to prove VCs in a forward
style (from hypotheses to the goal). When the proof fails, the user may use
the SPARK Checker to manually apply the same rewrite rules. Frama-C does not
verify initialization of variables/memory before reads, but it generates VCs
for a wide variety of automatic and manual proof tools, through the Why tool
(SMT solvers such as Yices or Alt-Ergo, proof assistants such as Coq and
PVS), so that proofs that are not discharged automatically can be dealt with
manually in a proof assistant, using the assistant facilities (tactics,
external calls to an automatic prover, etc.).

So your feeling that Frama-C has a strong focus on mathematical proofs is
not completely wrong: Frama-C does allow you to express and prove hard
mathematical properties of your program, through the use of your preferred
proof assistant, while SPARK tools do not help you there.

I should add that we are in the process of plugging the Why tool for
verifying SPARK programs, at AdaCore/Praxis, but the results of this project
will not be available anytime soon.
In this same project, we will be working with people from Frama-C to verify
mixed Ada/C programs.

Hope this helps,
--
Yannick

On Wed, Nov 11, 2009 at 9:30 AM, CUOQ Pascal <Pascal.CUOQ at cea.fr> wrote:

> Hello and welcome,
>
> > I am not very familiar with either Frama-C or Ada/SPARK.
> > I am wondering whether anyone in the list would be able
> > to comment on how they compare against each other.
> > It seems as though Frama-C has a stronger focus on mathematic
> > proofs whereas SPARK is more like an static analyzer.
>
> This is not going to be a definitive answer because I
> am less familiar with SPARK than Frama-C.
>
> I do not quite agree with this characterization of Frama-C,
> unless by "static analyzer" you mean a tool to enforce
> coding rules, which indeed no provided Frama-C plug-in
> does (someone could still write their own plug-in to
> enforce coding rules, and in fact some people have,
> for their own needs), or a heuristic bug-finding tool,
> something we have not focused on given the already
> healthy existing microcosm of tools that do that for
> the C language.
>
> There is in principle nothing that prevents any static
> analysis applicable to C to be implemented as a plug-in,
> although those we provide for now are the Value Analysis,
> and plug-ins that exploit its results, with the limitations
> this implies.
>
> On the other hand, if I understand correctly what I have
> been told by someone from Praxis, SPARK relies on
> deductive techniques too.
>
> So the bottom line is that they are very similar.
> SPARK/Ada is an older, more mature framework,
> and it defines its own subset of Ada
> that it works with. Frama-C uses C, which
> is not as well defined as Ada in the first place
> (the standard is weak because it has to retrofit all the
> existing compilers, so embedded developers often have to
> rely on behaviors of their compiler that are not mandated
> by the standard, and to make things worse some compiler
> developers are actively trying to break these embedded
> developers' programs). Frama-C does not define a common
> subset of C, although each plug-in can of course refuse
> to handle this or that difficult C construct. We will soon have
> some very impressive demos of C programs with difficult
> constructs being verified in a collaborative approach where
> the participating plug-ins help each other navigate around
> the analyzed program's difficulties.
>
> Hope this helps,
>
> Pascal
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091112/2fde171c/attachment.htm 

Frama-C-discuss mailing list archives

[Frama-c-discuss] Frama-C vs Ada/SPARK