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



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>