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

[Frama-c-discuss] Floor problem



The axiom is of course true, but would be better as

axiom floor: \forall real a; floor(a) <= a < floor(a)+1;

On 11/18/2014 4:42 AM, Claude Marche wrote:
> /*@ axiomatic Floor {
>   @   logic integer floor(real a);
>   @   axiom floor: \forall real a; floor(a) <= a <= floor(a)+1;
>   @ }
>   @*/