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

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