--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on February 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - loop invariant preserved



Le vendredi 08 f?vrier 2013 ? 16:35 -0200, Rovedy Aparecida Busquim e
Silva a ?crit :

> 1) Is my pos-condition written correctly?

It seems fine, as far as I can tell.

> 2) In this function, there is only a loop. So, the pos-condition is
> equal to loop invariant, is this right?

No, and that is where your main issue lies. Your loop invariant is just
plain wrong. A loop invariant has to hold at the start of each iteration
and at the end of the loop. Yours is true only at the end.

A better invariant (untested) would be

\forall integer j; 0<=j<i ==> G_E[j].G_Inst_Ativ <= Tempo ==>
G_E[j].G_Ativo == 1;

Notice how occurrences of i were replaced by j and how 0<=i<5 became
0<=j<i.

Best regards,

Guillaume