--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on May 2012 ---
On Thu, May 17, 2012 at 6:02 PM, dams <damien.balima at free.fr> wrote: > ? ?/*@ > ? ? ?@ loop invariant max_id > i; > ? ? ?@ loop variant max_id-i; > ? ? ?@*/ > ? ?while(i<max_id){ Another issue is that the invariant you have written, which is supposed holds at each iteration by definition, implies that the loop condition is always true, which would mean that the loop does not terminate. The correct invariant for i of your loop is i <= max_id. This invariant is true up to the last iteration, when the loop exits. When the loop is exited, Jessie knows that the loop invariant holds (i <= max_id) and that the condition (i < max_id) is false. It can then infer that i == max_id for the rest of the program, in case the program uses i after the loop. In summary, a loop invariant that implies the loop condition is a wrong loop invariant, unless the loop is an infinite loop. Pascal