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