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
- Subject: [Frama-c-discuss] [Jessie] loop invariant
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Fri, 6 Sep 2013 13:32:25 +0200
- In-reply-to: <CAEtoXR3XiHDCd49mKyKh4GLL6ozO48u97AmeMc5qSCrhhgthow@mail.gmail.com>
- References: <CAEtoXR21n9RPnwGE_UQ7zDjqrNPjhhRMuG5kQdzM=SjH7z+9CA@mail.gmail.com> <52162B8A.4080703@inria.fr> <CAEtoXR2DsVLvtKZM9PiFNPxx-=w11eY0sr2WNQ4ymdv74P-h4A@mail.gmail.com> <5216629A.5080303@inria.fr> <CAEtoXR3XiHDCd49mKyKh4GLL6ozO48u97AmeMc5qSCrhhgthow@mail.gmail.com>
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
- Follow-Ups:
- [Frama-c-discuss] [Jessie] loop invariant
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] [Jessie] loop invariant
- References:
- [Frama-c-discuss] [Jessie] loop invariant
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] [Jessie] loop invariant
- Prev by Date: [Frama-c-discuss] How would one annotate a function in an external header?
- Next by Date: [Frama-c-discuss] Which version of Frama-C/Why to use PVS ? (Jessie or WP)
- Previous by thread: [Frama-c-discuss] [Jessie] loop invariant
- Next by thread: [Frama-c-discuss] [Jessie] loop invariant
- Index(es):