3.9. Invariants#

Recursion is closely linked to iteration. In fact, a while loop can be written as a recursive subroutine (and this how the programming language Prolog achieves ‘iteration’: see this section). In computer science we would like to prove correctness and other properties about algorithms. Proofs about algorithms can be more difficult than the proofs about simple properties of the integers that we often use as examples this book.

A tool that helps us to prove properties about algorithms is an invariant. For example, a loop invariant is a property \(P\) of a loop such that:

  1. \(P\) is true before the loop is executed, and

  2. \(P\) remains true after each execution of the body of the loop (but not necessarily in-between the steps within the body).

So to prove that an algorithm \(A\) has the property \(Q\) (the post-condition), we can find an invariant \(P\) of \(A\) such that \(Q\) follows from \(P\), together with the fact that \(A\) has terminated. This last fact that \(A\) has terminated means that the loop condition (the guard of the loop) has become false.

In more detail, we need to find an invariant and show four things about it:

  1. Initialization or basis property. The invariant holds before the first iteration of the loop.

  2. Maintenance or inductive property. If the invariant holds before an iteration, then it also holds before the next iteration.

  3. Termination and falsity of guard. After a finite number of iterations the guard becomes false and the loop terminates.

  4. Correctness of the post-condition. The invariant together with the negation of the guard imply that the post-condition holds, in which case the program is correct.

Video

In one of the pencasts of this course, we prove the correctness of an algorithm using an invariant. You can find that pencast here: youtu.be/GSvqF48TVM4.

As an example, consider the simple loop:

while (x < 10)
    x = x+1;

What does this loop achieve? What is an invariant that helps us to prove the loop correctly achieves this? The invariant is \(x \leq 10\)—check that it does satisfy the above four properties!

While invariants can be useful, a suitable invariant can be difficult to find.

For a more complex example, consider the following. Note that you should call this bit of code with an integer \(n \geq 0\) and \(a > 0\).

r = 0
b = n
while (b >= a)
    b -= a
    r += 1

Try to convince yourself that this code computes: \(\lfloor n/a \rfloor\). Don’t believe us? We will prove it to you:

Proof. Invariant: \(r\cdot a + b = n\)

  1. Initialization or basis property. Before the loop runs, \(b=n\) and \(r=0\). Thus \(r\cdot a + b = b = n\).

  2. Maintenance or inductive property. Assume the invariant holds before iteration \(k\), thus: \(r_\text{old} \cdot a + b_\text{old} = n\).

Now we prove that it holds after iteration \(k\), that is: \(r_\text{new} \cdot a + b_\text{new} = n\).

From line 4 we derive that: \(b_\text{new} = b_\text{old} - a\) and \(r_\text{new} = r_\text{old}+1\). Thus \(r_\text{new} \cdot a + b_\text{new} = (r_\text{old} + 1) \cdot a + b_\text{old} - a = r_\text{old} \cdot a + a + b_\text{old} -a = r_\text{old} \cdot a + b_\text{old} \stackrel{ IH}{=} n\).

  1. Termination and falsity of guard. Every iteration \(b\) decreases by \(a\). Since \(a > 0\), this means that eventually \(b < a\) will hold.

  2. Correctness of the post-condition. Since \(0 \leq b < a\) and \(r \cdot a + b = n\), we know that: \(r \cdot a \leq n\) and \(n = r \cdot a + b < r \cdot a + a < (r +1) \cdot a\). So we get: \(r \leq n /a\) and \(n/a < r+1\), thus \(n/a - 1 < r \leq n/a\). Since \(r\) is integer, this means: \(f = \lfloor n/a \rfloor\).

□

Note

There is a form of logic, Floyd–Hoare logic, in which we can express invariants and can formally prove the (partial) correctness of a program. Read about it on wikipedia: en.wikipedia.org/wiki/Loop_invariant.