Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

Argh, I'm never going to get this right. Thanks Claude for you
watchfulness...

I looked at the ACSL manual for simpler ways to state the lemma. Here is
what I found:
- the proper "full" syntax is \round_double( \NearestEven, r)
- \round_double(\NearestEven, r) is equivalent to (double)r
- Frama-C's ACSL parser accepts 0.01d for \round_double(\NearestEven,
0.01), and 0.01f for \round_float(NearestEven, 0.01). The latter form is
documented in the ACSL manual, but I did not find mention of the former. I
may have missed it, though.

So, a correct (short) way to write the lemma is the following -- assuming
the desired rounding mode is nearest-even:
\forall double x; -1 <= x <= 1 ==> (double)((double)((double)(x*x) -
(double)(.2d * x)) + 0.01d) >= 0.;

My counter-example was indeed meant for the original "assert", or your for
your corrected lemma.

While we are on this topic, when ACSL was designed, did you consider the
introduction of a \Round operator that would change the meaning of all
arithmetic operators underneath it (à la Gappa)? Something similar already
exists for labels, with the \at operator.

On Sat, May 7, 2016 at 7:34 AM, Claude Marché <Claude.Marche at inria.fr>
wrote:

>
> 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.
>
>

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