--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on January 2009 ---
Hello and thank you very much for your quick answer. I reviewed the ACSL section on loop invariants as well as the wikipedia entry on loop invariants: http://en.wikipedia.org/wiki/Loop_invariant My Interpretation is, that a loop invariant must hold right after termination of a loop. I also ran the a function in a debug mode. Which showed me, that "i" will reach length in each loop. On my opinion, the index should also be printed right after termination. Therefore, I added a printf() after each loop. Doing this, "i" will reach 10. > 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. I do not understand, I required "i" to be less then "length" Please tell me if I havn't understood "loop invariants" because I am a little confused. Cheers Christoph -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: bug.c Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090123/f02af8b3/attachment.txt