--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on May 2009 ---
Hello, consider the following while loop: // loop invariant i <= n; while(some condition) { P i++; } Assume that - the loop invariant holds and - P is a block of code that does not modify i. Hence, i < n holds in P. Does Jessie know that when analysing this kind of loop? Ie, is Jessie able to conclude i <= n \land (some condition) ==> i < n ? - Boris