
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 postcondition 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?



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 :)



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

