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:

1. holds on entry to the loop;
2. holds after the loop body is executed;
3. 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!