Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>