--- layout: fc_discuss_archives title: Message 28 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



I am trying to introduce the rounding function axiomatically but my 
definition seems not to be sufficient. Here is my example:

// file: round.h

/*@ axiomatic Rounding {
   @ logic integer lround(real x);
   @ axiom rounded_value:
   @    \forall real x ; -0.5  <= (x - lround(x)) < 0.5;
   @ }
   @*/

/*@ requires 0.0 <= x <= 1000.0;
   @ ensures \result == lround(x);
   @*/
int roundit(float x);

The implementation is as follows:

// file: round.c
#include "round.h"

int roundit(float x)
{
   return (int)(x+0.5);
}

When I try to prove this function with the float model (using
Alt-Ergo), I get the following error:

------------------------------------------------------------
--- Alt-Ergo (stderr) :
------------------------------------------------------------
File "/tmp/wp067b74.dir/typed_ref_int_float/roundit_assert_3_Alt-Ergo.mlw", line 183, characters 23-47:typing error: real and int cannot be unified

What is the reason for it, I have assumed that logic type integer is a
subset of logic type real?

When I replace the float model by the real model, there is no such
error, but Alt-Ergo is not able to prove the post condition. I am
probably overlooking something trivial, so thanks for your patience.

Frank