how to write a suitable loop invariant?

Mar 28, 2011 at 1:14 AM

unsigned int ar[8];

void init_zero()
    ensures (forall(unsigned int i; i < 8 ==> ar[i] == i))
    writes (array_range(ar, 8))
{
    unsigned int i;
    for (i = 0; i < 8; i++)
        invariant (forall (unsigned int k; k < i ==> ar[k] == k))
        invariant (i <= 8)
    {
        ar[i] = i;
    }
    assert(ar[2] == 2);
}

The function "init_zero" will set all the elements in the array "ar" to be zero. But if I don't add the loop invariant "forall (unsigned int k; k < i ==> ar[k] == k)", VCC will report that the post-condition and the assert "ar[2] == 2" did not verify.

How to write a suitable loop invariant? Does the invariant need to present all the things the loop body does? If so, when the loop body is very complex, it will be very hard to find a suitable loop invariant. Are there some tools available to find a suitable loop invariant?

Coordinator
Mar 28, 2011 at 8:19 AM

Hi,

  indeed, in VCC loops need to be annotated by appropriate loop invariants, which must be strong enough to prove the remainder of the function. This may be hard. There is research on "invariant inference" to automate this process, but none of this is part of the VCC distribution. Also, I suspect, while they might help you with the loop invariants from your example, they will at this stage not help you with complex ones.

  Best, Mark

P.S.: you may want "ar[i] = 0;" in your code do really do zeroing :-)

Mar 28, 2011 at 8:27 AM

Thank you for your help! This is  just a toy I used to study VCC.