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

[Frama-c-discuss] Loop invariants



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