--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with loop invariant



Now, the code verifies. However, there are two points that I can't
explain:

- The loop invariant can be proved, but not the assertion at the end of
the loop body. But the latter should follow from the loop invariant
because

  wp(internal.msgnum++,
     \forall integer x;  0 <= x < internal.msgnum * BUFFSIZE 
                   ==>  tosend->data[x] == received->data[x];)  =

     \forall integer x;  0 <= x < (internal.msgnum+1) * BUFFSIZE
                   ==>  tosend->data[x] == received->data[x];

where wp(S,P) is the weakest precondition of S wrt P.

- If the assertion is omitted, the loop invariant can't be proved. Does
it nonetheless cause the prover to find the right goals?



/*@
loop variant MSGCOUNT - internal.msgnum;
loop invariant 0 <= internal.msgnum &&
  \forall integer x;  0 <= x < internal.msgnum * BUFFSIZE 
                   ==>  tosend->data[x] == received->data[x];
*/
for (internal.msgnum = 0;internal.msgnum < MSGCOUNT; internal.msgnum++)
{
  sreadi(msg_send,tosend,internal.msgnum);
  abpRound(msg_send,msg_receive,&channel,&internal);
  swritei(received,msg_receive,internal.msgnum);
  //@ assert \forall integer x;  0 <= x < (internal.msgnum+1) * BUFFSIZE
                   ==>  tosend->data[x] == received->data[x];
}

-- 
Regards,
Boris