Many verification-oriented programming languages have built-in support for attaching loop invariants to loops. A loop invariant is a condition that holds in four different places:

- immediately before the loop,
- at the start of each iteration (before evaluating the test condition),
- at the end of each iteration, and
- immediately after the loop.

Usually, the invariants are written just after the test condition. For example, in Dafny you’d write this:

```
while i < n
invariant i <= n
{
i := i + 1;
}
```

and in VCC you’d write this:

```
while (i < n)
_(invariant i <= n)
{
i = i + 1;
}
```

and in Whiley you’d write this:

```
while i < n
where i <= n:
i = i + 1
```

But are these languages actually putting these loop invariants in the best place?

Well, perhaps not. The thing is, the loop invariants are required to hold at the beginning of every iteration, *before* the test condition is evaluated. (If the test condition holds, then the loop invariants must then be reestablished by the end of that iteration.) So writing the invariants *after* the test condition, as all of the languages above do, is really rather misleading. For instance, in the code above, it looks like we should know that `i < n`

holds by the time we evaluate the invariant. In fact we only know that `i <= n`

holds.

One alternative would be to write the invariants before the test condition, like this:

```
invariant i <= n
while i < n
{
i := i + 1;
}
```

```
_(invariant i <= n)
while (i < n)
{
i = i + 1;
}
```

```
where i <= n
while i < n:
i = i + 1
```

which I think is perfectly acceptable. Another alternative would be to write the invariants at the end of the loop body, like this:

```
while i < n
{
i := i + 1;
} invariant i <= n;
```

```
while (i < n)
{
i = i + 1;
}
_(invariant i <= n)
```

```
while i < n:
i = i + 1
where i <= n
```

which I also find inoffensive (though I think it works less well with the Python-style indentation rules that Whiley uses).

Ultimately, I think there’s no *single* place that is truly ideal for writing invariants. The thing is, as I mentioned above, loop invariants hold in four different places. So unless we write the same invariant in all four places, or we start writing programs as flowcharts rather than structured text, the user will need to do some mental gymnastics to remember exactly where they hold.

But perhaps these mental gymnastics can be made a little easier by moving the invariants to a slightly better position.

how about ?

while True {

//inv

if !(i < n) break;

i := i + 1

}

Enjoyed this old post. Note SPARK Ada allows placement of the invariant anywhere inside the loop body, I believe. Judging by the post, I’d imaginge this is just as offensive as placing it direclty after the loop condition.