--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on February 2013 ---
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