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

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).

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,
-- 
E tutto per oggi, a la prossima volta
Virgile