--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on January 2009 ---
Thank you very much, I think I understand. I confused the requirements of annotation-writing with the execution. That was a valuable information Cheers Christoph ----- Original Message ----- From: "Claude March?" <Claude.Marche at inria.fr> To: "Frama-C public discussion" <frama-c-discuss at lists.gforge.inria.fr> Sent: Friday, January 23, 2009 11:01 AM Subject: Re: [Frama-c-discuss] bug with loop invariant, wrong loop invariant gets proven Christoph Weber wrote: > 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. But the semantics of loop invariant in ACSL does not imply that. Generally speaking, in //@ invariant I; while (true) { s1; if (c) break; s2; } I is asked to be true when entering the loop, and being preserved by the sequence s1; if (c) break; s2; When the sequence s1; if (c) break; exits the loop, I may be made wrong if there are side-effects in s1 (or in c!) In other words: loop invariant hold right after termination of a loop only if there are no side-effects between the loop start and the exit. But otherwise not necessarily... This is why in textbooks you usually prefer to assume side-effect free loop conditions... > 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. Sure, but the program points where I put my printf are exactly where the invariant should hold. It is not the case for your additional printf, as said above. > > >> 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" The VC for preservation of an inductive invariant is like this: { 0<=i<=length } i++; if (i == length) break; { 0<=i<=length } which is not true when i==length at the beginning! Hence: the right invariant is 0 <= i < length ! -- 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 | _______________________________________________ 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