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



Hello,

(Currently) Alt-Ergo does not consider that "int" is a subtype of 
"real". This is why it says "typing error: real and int cannot be 
unified ". This should evolve with our new (experimental) input language 
based on SMT2.

A workaround would be to introduce an explicit cast between int and real.

- Mohamed.

-- 
Senior R&D Engineer, OCamlPro
Research Associate, VALS team, LRI.
http://www.iguer.info

Le 19/06/2014 09:19, Frank Dordowsky a ?crit :
>
> 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
> _______________________________________________
> 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