--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on June 2014 ---
On Thu, Jun 19, 2014 at 9:19 AM, Frank Dordowsky <frank at dordowsky.de> wrote: > > /*@ axiomatic Rounding { > @ logic integer lround(real x); > @ axiom rounded_value: > @ \forall real x ; -0.5 <= (x - lround(x)) < 0.5; > @ } > @*/ ... > int roundit(float x) > { > return (int)(x+0.5); > } > If you want to actually prove that the function roundit computing with IEEE 754 arithmetic (as opposed to the function implemented on an imaginary computer where + is real addition), you will need: 1- to weaken the specification slightly to -0.5 <= (x - lround(x)) <= 0.5 2- to find a better implementation, because (int)(x+0.5) does not have even the weaker property. See the series of posts that starts at http://blog.frama-c.com/index.php?post/2013/05/02/nearbyintf1 . -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140619/dd9bb7b6/attachment.html>