Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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