--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on February 2013 ---
Dear Guillaume, Thanks a lot. The loop invariant has worked very well. I have noticed my error. Best regards, Rovedy 2013/2/8 Guillaume Melquiond <guillaume.melquiond at inria.fr> > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130208/8cfe8e32/attachment.html>