--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on September 2013 ---
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, >