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 install Whiley is through the Eclipse Plugin. Have fun!