--- layout: fc_discuss_archives title: Message 4 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



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