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



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> 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>
> 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
>> > 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/%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
>> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>>
>
>
>
> --
> Boris
>
>
> _______________________________________________
> Frama-c-discuss mailing listFrama-c-discuss at lists.gforge.inria.frhttp://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
>



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