--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on January 2009 ---
Hi, To illustrate my answer, I attach an instrumented version of your code. If you compile and run it you will get : loop1: 0 1 2 3 4 5 6 7 8 9 loop2: 0 1 2 3 4 5 6 7 8 9 loop3: 1 2 3 4 5 6 7 8 9 10 first loop: invariant 0 <= i < length is indeed true: no bug here second loop: although 0 <= i <= length is true, it is not an *inductive* invariant: imagine i=length before an iteration, then ++i != will be true and i will get value length+1. So no bug here. third loop: no problem. Beware that your "rewriting" of the loop has the effect that the invariant is now posed after incrementation of i. Which makes things different! No bug here. The key point is to understand where the invariant is supposed to hold, which is quite tricky if there are side effects in the loop condition. Please reread the loop invariant section of ACSL manual... By the way: if you think you find a bug, could you use the BTS instead? Today, it was fortunate that I was willing to answer quickly, but otherwise, a bug report only given in the mailing list might get lost... Regards, - Claude Christoph Weber wrote: > Hello, > > I think I discovered a bug: > Following function: > > /*@ > requires 0 < length; > */ > int loopinvariant(int length) > { > // loop 1: proof of false specification > int i = 0; > /*@ > loop invariant 0 <= i < length; > */ > while(++i != length) > {} > > // loop 2: proof failed for intended specification > i = 0; > /*@ > loop invariant 0 <= i <= length; > */ > while(++i != length) > {} > > // loop 3: proof of rewritten loop 2 > i = 0; > i++; > /*@ > loop invariant 0 <= i <= length; > */ > while(i != length) > { > i++; > } > return 0; > } > > As you can see from my comments, I expect loop 2 to be correct. > > It is courious, that a weaker loop invariant fails. > > But loop 1 is falsly specifyed but proven never the less. > > I think this is of interest and please tell me if I misinterpreted something > > Cheers > > Christoph > > > ------------------------------------------------------------------------ > > _______________________________________________ > 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 | -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: bug.c Type: text/x-csrc Taille: 656 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090123/b6edd1cd/attachment.c