--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] loop invariant




On 09/06/2013 01:32 PM, Virgile Prevosto wrote:
> Hello,
>
> 2013/9/5 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
>
>> We modified the example, the int t[] was replaced to float t[] (in the
>> function and in the axiomatic).
>
>> However, we would like to work without the pragma (with floating point
>> arithmetic).
>> The problem is that the loop invariant below was not proved:
>> loop invariant s == sum(t,0,i);
>>
>> The screen shot (Without_Pragma.png) shows the comparison between a Real
>> variable and float. We think that the loop invariant was not proved because
>> of that.
>>
>> Is this the problem? How can we to solve this problem?
>
> Yes, this is the problem: in your predicate sum, all computations are
> made over real, so that it is in general not true that the partial sum
> as computed on floats in the code is equal to sum(t,0,i). You have to
> express your properties in terms of rounding errors between the
> mathematical result and the floating point computation. You can find
> examples of such specifications on Toccata's gallery of verified
> programs (http://toccata.lri.fr/gallery/fp.en.html).

Indeed, you may have a look at the example 
http://proval.lri.fr/gallery/ScalarProduct.en.html which is very close 
to yours. I guess you could prove on your code a post-condition of the form

ensures \abs(\result - sum(t,0,n)) <= n * C;

for some well chosen constant C. Follow the example above to proceed.

In other words, your original code is wrong with respect to your 
specification: this code does not compute exactly the sum of the 
elements of the array, but it computes a number that is close, the 
rounding error being given by the post-condition above.

Notice that technically, the post-condition above needs to give a fixed 
bound for the elements of the array. The constant C depends on that 
bound. You may also try to find a bound on the *relative* error:

ensures \abs(\result - sum(t,0,n)) <= C * n * sum(t,0,n);

but it would require significantly more work, I do not recommend to 
start with that.

Good luck, do not hesitate to report your successes !

- Claude


> Alternatively, you can force the computation into float in sum
> by modifying your axiom:
>    @   axiom sum2{L} :
>    @     \forall float *t, integer i, j;
>    @       sum(t,i,j+1) == (float)(sum(t,i,j) + t[j]);
> But this is not a very good idea IMHO: as floating point addition is
> not associative, this definition of sum is very fragile. In
> particular, I guess that sum2(t,i,j) != sum(t,i,j) where sum2 is
> axiomatically defined by
>    @   axiom sum2_2{L} :
>    @     \forall float *t, integer i, j;
>    @       sum(t,i,j) == (float)(t[i]+sum(t,i+1,j));
> (i.e. sum(t,i,j) = ((t[i]+t[i+1])+t[i+2])+... and sum2(t,i,j) =
> t[i]+(t[i+1]+(t[i+2]+(...))))
>
> Best regards,
>