Loops can be annotated with loop invariants. A loop invariant is a condition that you expect to hold every time control reaches the top of the loop. A loop invariant is an annotation of the format _(invariant e) just after the header of the loop.

In while- and for-loops, the exit condition is checked right after assuming the invariant, thus, the invariant must contain the exit condition. In do-while-loops, however, the exit condition is checked before assuming the invariant again, so the invariant must not contain the exit condition. For example:

#include <vcc.h>

void foo() {

  int i;

  for (i = 0; i < 10; i++) 
    _(invariant 0 <= i && i <= 10)
  { }
  _(assert i == 10);
 
  i = 0;
  while (i < 10) 
    _(invariant 0 <= i && i <= 10)
  { 
    i++;
  }
  _(assert i == 10);

  i = 0;  
  do
    _(invariant 0 <= i && i < 10) 
  {
    i++;
  } while (i < 10);
  _(assert i == 10);
}


A more interesting example is a function computing the Fibonacci function, specified using the recursive definition and implemented iteratively:

#include "vcc.h"

ispure int fib(int n)
_(ensures n <= 1 ==> \result == 1)
_(ensures n > 1 ==> \result == _(unchecked) (fib(n - 1) + fib(n - 2)))
{
    int a = 1, b = 1;
    int i;

    if (n <= 1) return 1;

    for (i = 1; i < n; ++i)
        _(invariant 1 <= i && i <= n)
        _(invariant b ==_(unchecked) fib(i))
        _(invariant a == _(unchecked) fib(i - 1))
    {
        int cur = _(unchecked) (a + b);
        a = b;
        b = cur;
    }

    return b;
}

Last edited Jan 19, 2012 at 4:53 PM by MarkHillebrand, version 8

Comments

erniecohen Sep 5, 2010 at 5:55 PM 
Before. The translation of a while loop is to assert the invariant, havoc the modified part of the state, assume the invariant, compute the test, jump past the loop if the test says to exit the loop, do the loop, assert the invariant anywhere where you do a continue and at the end of the loop, and finally assume false. So if the failing test has a side effect that invalidates the invariant, the invariant will no longer hold after you leave the loop (but VCC knows that the invariant held before the test failed, so it can use ordinary sequential reasoning to deduce what holds after the loop). Similarly, when checking the body, any effects of the passing test form part of the loop body.

dcrocker Sep 4, 2010 at 3:38 PM 
If the while-part of a for- or while-loop has side-effects, is the invariant assumed/required to hold before the side-effects occur, or after they occur?