--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on January 2009 ---
Hello again, I would like to clarify something: Given, that while(++i != length) {} is equivalent to the following: and the loop invariant requires that i < length, /*@ loop invariant 0 <= i < length; */ while(true) { i++; if (i == length) break; } Why is i allowed to become equal to length? I remember the ACSL document state, that abnormal termination with a "break" it is not required that the loop invariant holds. That leaves only one question, are both loops truly equivalent. Again, Thank you for your help. Cheers Christoph