--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on September 2013 ---
On 09/12/2013 08:06 PM, Rovedy Aparecida Busquim e Silva wrote: > Hi, > > We have run the example as suggested by Claude > (http://proval.lri.fr/gallery/ScalarProduct.en.html). > > We used the example annotations in our code (attached) and the all VCs > were proved. > > However, we have some doubts: > > 1. We have used the lemma bound_int_to_real but we did not understand > how it works. > Why the define NMAXR is used? the lemma says the if some integer n is less or equal 3, then when converting it to a rel number the result is less or equal 3.0. Seems stupid but needed to help provers... > 2. The variable j used in the loop was global in the legacy source > code. However, the loop invariant was not proved (loop invariant > \abs(p - sum(x,j)) <= j * BOUND). > We changed the variable j to local and the loop invariant was proved. > Does not the loop invariant work with global variable? It should not make any major difference. However since the context of the VC would be a bit different (e.g. not the same order of hypotheses), you may need to increase a little the time limit given to the prover. I tried your example and I've been abble to prove it, both in case j is global and when it is local. Although, I needed to modify a bit the annotations: removing the "loop assigns p,j" that disturbs Jessie, and replacing "sum(x,...)" by "sum(x+0,...)" because it is refused by Frama-C kernel. I'm using Frama-C Fluorine 20130601 + Why 2.33 + Why3 + provers Alt-Ergo, CVC3 and Gappa. Hope this helps, - Claude > Best regards, > Nanci, Luciana e Rovedy > > > > > 2013/9/7 Claude Marche <Claude.Marche at inria.fr> >> >> >> >> On 09/07/2013 10:56 AM, Claude Marche wrote: >>>> >>>> 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 >> >> >> A very bad idea indeed. >> >> - claude >> >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss