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



Thanks for the FP example.

[ I agree that predicates are either valid or invalid - I just wanted to 
clarify the language because sometimes people use 'invalid' to mean not 
provable by tool X. ]


On 5/6/2016 5:52 AM, Boris Yakobowski wrote:
> ACSL is a specification language with a two-valued logic (see Section 
> 2.2.2). So predicates can definitely be valid or invalid.
>
> Here, Maurice's assert is equivalent to the lemma
>
> \forall double x; -1 <= x <= 1 ==> x*x - .2 * x + 0.01 >= 0.;
>
> 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 :-)
>
> 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/~marche/ <http://www.lri.fr/%7Emarche/>
>>         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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160506/7be92311/attachment.html>