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