--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] an example involving floats




David DELMAS wrote:
> Hello,
> 
> here is an apparently simple example :
> 
> /*@
> assigns \nothing;
> ensures E < A ==> \result == B;
> */
> float F(float E, float A, float B)
> {
>     if (E < A) return B;
>     else return 0.;
> }
> 
> The postcondition is proved by Z3, Yices and CVC3, but neither by Alt-
> Ergo, nor by Simplify.
> (of course it is proved by all if I change the float type to int)
> 
> I would appreciate some intuition on the reason why it is so.

First thing: by default, the jessie plugin interprets floats by 
mathematical real numbers. This might change later, but for the moment 
the default is such because true floating-point support is not fully 
operational.

So we have to think of E, A, B as real numbers. The VC for the "else" 
branch has the form

E >= A  (* for the negation of the test *)
implies the post-condition which is of the form E < A ==> some P

in principle, this seems trivial because P must be proved under 
contradictory hypotheses E >= A and E < A. The point is that here
 >= and < denote comparisons of real numbers, and for Simplify and 
Alt-Ergo, the support for reals numbers is void or very weak, in the 
sense that they do not even know that >= is the negation of <.

The authors of Alt-Ergo are certainly willing to improve their tool. We 
can hope for a better Alt-Ergo in the future (I forward this example to 
their dev team!).

On the other hand, Simplify will not evolve anymore so it will never 
support real numbers.

- Claude


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |