--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on September 2013 ---
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 |