--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 2016 ---
My mistake. I coalesced two different things when replying to Maurice : - the validity of the lemma /*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */. It is indeed valid in ACSL, should be proven by WP whatever the model (since, as Loïc mentioned, it involves only real) , and (as all lemmas) is completely ignored by Value; - the validity status of the assert in double x1 = x*x - .2 * x + 0.01; /*@ assert x1 >= 0; */, which is invalid in ACSL, but can be proven by the Float model of WP. On Wed, May 4, 2016 at 2:07 PM, Claude Marché <Claude.Marche at inria.fr> wrote: > > Sorry to interfere, but I don't understand the meaning of "wrong in WP" > > According to ACSL manual, this lemma is a statement expressed purely in > mathematical real arithmetic, and as such it is valid. It is indeed > proved automatically by Z3 4.4.1. > > If you want to state a similar property talking about floating-point > arithmetic, it should be stated differently, typically using a program > > void f(double x) { > double y = x*x - .2 * x + 0.01; > //@ assert y >= 0.0; > } > > But I guess it probably wrong because of rounding, even with a > precondition like \abs(x) <= 1.0 > > My two cents, > > - Claude > > Le 04/05/2016 13:54, Loïc Correnson a écrit : > >> /*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */ > > > > This lemma is definitely wrong in WP with Real model (not float there). > > At least, it is not provable in the forthcoming release of Frama-C. > > Is there a bug in some existing release? > > L. > > > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > > > -- > Claude Marché | tel: +33 1 69 15 66 08 > INRIA Saclay - Ãle-de-France | > Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 ORSAY Cedex | > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > -- Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160504/62b6d84f/attachment-0001.html>