--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2016 ---
But the original question is about x*x - .2*x + 0.01, not x*x -2*x + 0.01. With x = 0.5, we get x*x - .2*x + 0.01 == 0.25 - .1 + 0.01 ==.16 > 0 More to the point With x = 0.1, we get x*x - .2*x + 0.01 == 0.01 - .02 + 0.01 == something close to zero, depending... - David From: Loïc Correnson <loic.correnson at cea.fr> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> Sent: Wednesday, May 4, 2016 8:57 AM Subject: Re: [Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin With x = 0.5, we get x*x -2*x + 0.01 == 0.25 - 1.0 + 0.01 == -0.74 < 0 There is probably a confusion with (x2 - 2x + 1) = (x-1)2 >= 0, but Z3 is not able to prove it⦠However, Alt-Ergo succeed into proving (x-1)^2 >= 0, and (x^2 - 2*x + 1 == (x-1)^2.    L. > Le 4 mai 2016 à 14:07, Claude Marché <Claude.Marche at inria.fr> a écrit : > > > 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 _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160504/65b5f6a3/attachment-0001.html>