--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on January 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] bug with loop invariant, wrong loop invariant gets proven



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