--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Introductory slides on Frama-C



Hi to all,

A few remarks from me, without mathematics:

slide 5: I don't think it is accurate to attach the term "formal
methods" to only abstract interpretation and deductive verification. I
don't think the spectrum of "formal methods" is that well defined,
indeed from my point of view the simple concept of using a computer
program to analyse another computer program is already a "formal
method", and in that sense all Frama-C plugins belong to formal methods.
For example, there is a research area called "formal testing". But
anyway, you could use "static analysis" to group abstract interpretation
and deductive verification. "Specification generation" could belong to
"static analysis" too.
See also http://www.fmeurope.org/, where even if the term is not very
clearly defined, it is obviously not limited to static analysis.

slide 7: I don't think Jessie is already "deprecated". Jessie3 simply
does not exist, even if it may exist in some future.

slide 9: probably more accurate is Why in 2001 and Caduceus 2004 (but
who cares...)

slide 10: a bit frightening, don't you think? First things one needs are
tutorials (including yours) and illustrative examples, no?

slide 24: Everything should be proved to "assume correct program"?
shouldn't it be to "guarantee the program correct" ?

slide 27: No ?IF p THEN q1 ELSE q2? ? But according to ACSL manual, one
may write (p ? q1 : q2). (May be it is not implemented...)



Le 03/09/2013 15:27, David MENTRE a ?crit :
> In slide 47, behaviours found and not_found have opposite logical
> condition for assumes clauses. However I find difficult to explain it
> without going back to first order logic (!(a ==> b) eq. !(!a || b) eq.
> ...) which I would like to avoid. Any idea on a way to explain that simply?

Though question indeed... using ==> instead of && after \exists is an
frequent mistake...

- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |