# Understanding Loop Invariants in Whiley

In this article, I’ll look at a common problem one encounters when verifying programs: namely, *writing loop invariants*. In short, a loop invariant is a property of the loop which:

- holds on entry to the loop;
- holds after the loop body is executed;
- holds when the loop finishes.

Loop invariants can be tricky to get right but, without them, the verification will probably fail. Let’s consider a very simple example:

```
define nat as int where $ >= 0
nat counter(int count):
i = 0
while i < count:
i = i + 1
return i
```

This program does not verify. In order to get it to verify, we need to add a loop invariant. The need for loop invariants arises from Hoare's rule for `while`

-loops. The key issue is that the verifier *does not know anything about any variable modified within a loop, other than what the loop condition and/or invariant states*.

In our example above, the loop condition only tells us that `i < count`

during the loop, and that `i >= count`

after the loop (in fact, we can be more precise here but the verifier cannot). Knowing that `i >= count`

is not enough to prove the function’s post-condition (i.e. that `i >= 0`

). This is because `count`

is an arbitrary `int`

which, for example, may be *negative*.

Therefore, to get our example to verify, we need a loop invariant that explicitly states `i`

cannot be negative:

```
nat counter(int count):
i = 0
while i < count where i >= 0:
i = i + 1
return i
```

The loop invariant is specified on the `while`

loop with the `where`

keyword. In this case, it simply states that `i`

is always `>=0`

. Whilst this might seem obvious to us, it is unfortunately not so obvious to the verifier! In principle, we could employ a simple form of static analysis to infer this loop invariant (although, currently, Whiley does not do this). Unfortunately, in general, we will need to write loop invariants ourselves.

To explore a slightly more complex example, I’ve put together a short video which illustrates using Whiley to verify a program which sums a list of natural numbers:

Finally, if you’re interested in trying this out for yourself, the easiest way to run Whiley is through the whileylabs website. Have fun!