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] Axiomatic Definition of Rounding Function

Hi,

Interesting example. Via the Jessie plugin, both three provers CVC3
2.4.1, Z3 3.2 and Z3 4.3.1 are able to prove your assertions, except of
course the third (on 3.5) which is not true.

A few remarks:

1) the axiom

axiom exists_value:
    \forall real x; \exists integer n; lround(x) == n;

is pretty useless since lround returns an integer

2) since your asserts does not depend on your code, they should be
better stated as global lemmas, e.g.



//@ lemma round30: lround(3.0) == 3;
//@ lemma round31: lround(3.1) == 3;
//@ lemma round35: lround(3.5) == 4;
//@ lemma round39: lround(3.9) == 4;

3) I'm unable to prove that roundit(x) returns lround(x), but this is
another story.

Hope this helps,

- Claude

Le 19/06/2014 17:47, Frank Dordowsky a ?crit :
> Thanks for the hints and the link. The blog is very impressive and was
> surprising to me, but I must admit that I did not yet delve too much
> into floating point analysis.
> 
> Weakening the post-conditions leaves an ambiguity: if  x == 3.5 for
> example, both 3 and 4 satisfy the predicate.
> 
> I nevertheless modified my definition of lround, and also added
> another axiom that claims the existence of a function value:
> 
> /*@ axiomatic Rounding {
>   @ logic integer lround(real x);
>   @ axiom exists_value:
>   @    \forall real x; \exists integer n; lround(x) == n;
>   @ axiom rounded_value:
>   @    \forall real x ; -0.5  <= (x - lround(x)) <= 0.5;
>   @ }
>   @*/
> 
> I have also tried one of the implementation examples of the blog, and
> added some trivial assertions:
> 
> // file: round.c
> #include "round.h"
> 
> int roundit(float x)
> {
>   //@ assert lround(3.0) == 3;
>   //@ assert lround(3.1) == 3;
>   //@ assert lround(3.5) == 4;
>   //@ assert lround(3.9) == 4;
> 
>   if (x >= 0x1.0p23) return x;
>   return (int)(x+0.49999997f);
> }
> 
> I still cannot prove the post condition, but even the assertions are
> not proved, which surprises me, and I have no explanation for it.
> 
> Frank
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |