--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on September 2013 ---
Hello Claude, Le 04/09/2013 18:05, Claude March? a ?crit : > 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. I agree with your comment. "static analysis" is a better definition (with a nice counter balance for dynamic analysis for E-ACSL & Co.). I patched the slide (I don't have the source image). > slide 7: I don't think Jessie is already "deprecated". Jessie3 simply > does not exist, even if it may exist in some future. Fixed. Thanks for correcting my wrong impression. > slide 9: probably more accurate is Why in 2001 and Caduceus 2004 (but > who cares...) I do care! Fixed. > slide 10: a bit frightening, don't you think? First things one needs are > tutorials (including yours) and illustrative examples, no? I want to address the issue of Frama-C documentation, which is indeed complex. Those slides targets programmers in order to help them become autonomous with Frama-C. I nonetheless added some reassuring comments. > slide 24: Everything should be proved to "assume correct program"? > shouldn't it be to "guarantee the program correct" ? Yes, fixed. > 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...) Good catch. I checked, (p ? q1 : q2) is supported[1]. My comment "No ?IF p THEN q1 ELSE q2?" meaning is that no such logical operator exists. I corrected the slide and added (p ? q1 : q2). Many thanks for the detailed review! Best regards, david [1] Attached program is proved by WP but not by Value analysis with -slevel 10. I tried adding a "require x >= 0 || x < 0;" or "assert x >= 0 || x < 0;" to split the state space without success. Any idea on how to prove that with Value analysis? -- David MENTR? - Research engineer, Ph.D. Formal Methods and tools MITSUBISHI ELECTRIC R&D Centre Europe (MERCE) Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59 http://www.fr.mitsubishielectric-rce.eu -------------- next part -------------- /*@ ensures \old(x) >=0 ? \result == 1 : \result == -1; */ int sign(int x) { if (x >= 0) return 1; else return -1; } int main(int x) { return sign(x); }