--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Axiomatic Definition of Rounding Function



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