--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on November 2014 ---
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; > @ } > @*/