--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using floating-point + in spec



I was about to answer to this question but Virgile did it just before me.

A few additional remarks

On 01/12/2011 09:04, Virgile Prevosto wrote:
> Hello,
>
> On 30/11/2011 23:22, Stephen Siegel wrote:
>> What is the right way to use floating-point addition in a
>> specification? For example, I want to say
>>
>> ensures x == y + z;
>>
>> where x, y, and z are variables in the program, and I want the "+" to
>> mean "floating-point addition" (i.e., whatever the "+" means inside
>> the program), not "real (mathematical) addition".
>>
>
> If I'm not mistaken, addition on floating-point values is defined by
> IEEE754 as rounding the result of the addition on the corresponding real
> number. Thus, your ensures clause could be expressed (assuming x,y and z
> are double and rounding mode is nearest even. The various other
> possibilities are described in ACSL manual, section 2.2.5) as
>
> //@ ensures x == \round_double(\NearestEven,y+z);


Yes. And of course you should be aware that this assumes that the 
rounding mode is nearestEven. I think it is good that it is has to be 
made explicit.

> NB: the \eq_double function is unimplemented in the current version of
> Frama-C.

Yes and no. The function \eq_float is implemented, and I think it 
applies to apply both on type float and double. The ACSL document may be 
unaccurate on this point.

Anyway, for me it is not related to the original question, since the 
purpose of \eq_float is to support special values (infinities and NaN)

- Claude