--- layout: fc_discuss_archives title: Message 42 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



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);
}