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] postcondition of sqr function

/*@
     ensures \result >= 0.0;
*/
double sqr(double x)
{
    return x * x;
}

1/ A lot of work has been done on floating-point operations
since the last release. That is to say, support for floating-point
operations will be much less partial in the next release than
in Lithium, both for Jessie and for the Value Analysis.

2/ With the value analysis you
need to indicate that the property must be analyzed
by case by adding an assertion x<=0 || x>=0, which
does not incur any additional proof obligation since it
can be verified to hold easily. The same trick may help
automatic theorem provers, if you somehow arrange for
this disjunction to be in the hypotheses, they may have
the idea to study what that means for x*x separately.

3/ With both Jessie or the Value Analysis you will get a 
proof obligation.
You will probably want to use the "strict" model in which
infinites and NaN are treated as unwanted errors when they
occur. In this case the proof obligation is that x*x should
not overflow.
Even with the Full model in Jessie your post-condition does
not hold because NaN is not >=0 (the result can be NaN
when the sqr function is applied to NaN).

Pascal