--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on May 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin



Sorry, my mistake with .2 instead of 2.

The lemma is definitely _correct_ and soundly proved by WP+Z3 in all float models, since the lemma only involves reals.

	L.

PS: it is still a mystery for me why Z3 succeed into proving this, but fails into proving (x2 - 2x + 1) >= 0… :-)


> Le 4 mai 2016 à 15:27, cok at frontiernet.net a écrit :
> 
> 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 <mailto: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 <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> >> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <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/ <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 <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 <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/33173396/attachment.html>