--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on May 2009 ---
Hollas Boris (CR/AEY1) wrote: > Hello, > > consider the following while loop: > > > // loop invariant i <= n; > while(some condition) { > P > i++; > } > > > Assume that > - the loop invariant holds and > - P is a block of code that does not modify i. > Hence, i < n holds in P. > >Does Jessie know that when analysing this kind of loop? Ie, is Jessie able to conclude i <= n \land (some condition) ==> i < n ? Sure if condition is (i < n) or anything that implies (i < n), but otherwise no. But if you are able to prove that the invariant holds, then certainly you should be able to prove //@ assert i<n; either before or after P, no ? What is your condition exactly ? > - Boris > > _______________________________________________ > 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 -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |