--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on May 2016 ---
Hi, Le 06/05/2016 11:52, Boris Yakobowski a écrit : > ACSL is a specification language with a two-valued logic (see Section > 2.2.2). So predicates can definitely be valid or invalid. Sure > Here, Maurice's assert is equivalent to the lemma > > \forall double x; -1 <= x <= 1 ==> x*x - .2 * x + 0.01 >= 0.; Wrong! because in logic formulas, those + , - , * are interpreted as operations on real numbers, not floats. Similarly, 0.01 and .2 denote real numbers and not their approximation as floats. If one really want to state a lemma equivalently to the code double t = x*x - .2 * x + 0.01; //@ assert t >= 0.; then one must write //@ lemma l: \forall double x; -1 <= x <= 1 ==> \round(\nearest_even, \round(\nearest_even, \round(\nearest_even,x*x) - \round(\nearest_even, \round(\nearest_even,.2) * x)) + \round(\nearest_even,0.01) >= 0.0; (I'm probably wrong with the syntax, but you got the idea) I indeed assumed the rounding mode was nearest_even, but of course I don't really know and if one wants to check this kind of property, it is important to think about what is the rounding mode > This lemma is invalid because it is refuted by the double value > 0x1.9999998p-4. (i.e. 1.5999999940395355*2^-4 or approximately > 0.0999999996275). See my message on May 1 for more floating-point gory > details :-) OK (I did not check but I trust you), a counterexample to the second variant of the lemma of course, not the first, which is valid. > On Thu, May 5, 2016 at 3:31 AM, David R. Cok <dcok at grammatech.com > <mailto:dcok at grammatech.com>> wrote: > > Sorry: when you say "invalid in ACSL" do you actually mean it is > invalid (because it is floating point, not real?) or do you mean it > is not provable (and by what) or do you mean it is not a well-formed > ACSL statement? ACSL is just a language, not a proof tool. If the > first, is it actually the case that there are double precision > numbers for which the assertion does not hold? > > - David > > > On 5/4/2016 2:14 PM, Boris Yakobowski wrote: >> 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 <mailto: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 >> <mailto: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 <tel:%2B33%201%2069%2015%2066%2008> >> INRIA Saclay - Ãle-de-France | >> Université Paris-sud, Bat. 650 | >> <http://www.lri.fr/%7Emarche/%0AF-91405>http://www.lri.fr/~marche/ >> F-91405 ORSAY Cedex | >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> <mailto:Frama-c-discuss at lists.gforge.inria.fr> >> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss >> >> >> >> >> -- >> Boris >> >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> <mailto: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 > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > > > > -- > Boris > > > _______________________________________________ > 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 |