--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on March 2009 ---
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 |