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



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                    |