--- layout: fc_discuss_archives title: Message 16 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



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>