5.3. Computer Program Verification

We saw in Section 5.2.3 that recursive algorithms could be proved to be true using induction. This is an extremely powerful tool to reason about the correctness of algorithms.

Here, we examine an important application of induction to computer science in the form of loop invariants.

Definition (loop invariant)

A loop invariant is a property of a program that is true before and after each iteration of a loop.

Let’s begin with a simple example. Consider the following Python program which computes the maximum element in a list of integers.

def max(L) :
    m = L[0];
    i = 1;
    while (i < len(L)) :
        if (L[i] > m) :
            m = L[i]
        i = i + 1

    return m

print(max([4,12,5,1,56,1,4,7]))

56

A loop invariant for this program would be that m is always the maximum element of L between the index 0 and i-1, inclusive.

Before the loop m = L[0] and i=1. Hence, surely m is the maximum element of the sub-list L[0:i]. After the first iteration of the loop, we have i=2. Does the loop invariant hold? That is, is m equal to the maximum element in L[0:2]? Surely so, we check if L[1] > m and, if so, assign m to be L[1].

To prove the overall correctness of the function max(L) we must apply induction.

Loop invariant induction

We prove that max(L) returns the maximum element of L using induction and loop invariants.

For the basis step, before the first iteration of the loop, we have m = L[0] and i=1. Thus, surely m is the maximum element in L[0:1].

For the inductive step, assume that after the \(k\)th iteration of the loop we have that m is the maximum element of L[0:i]. We will prove that, after the \(k+1\)th iteration of the loop, that m is still the maximum element of L[0:i].

At the end of the \(k\)th iteration of the loop we have i = k+1. Hence, by inductive hypothesis, m is the maximum element of L[0:k+1].

After the end of the \(k+1\)th iteration of the loop we have i = k+2. We will show that m is the maximum element of L[0:k+2]. Proceed by cases: either L[k+1] is is the maximum element of L[0:k+2] or it is not.

If L[k+1] is not the maximum element of L[0:k+2], then m, as the maximum element of L[0:k+1], is also the maximum element of L[0:k+2]. In the loop, since m > L[k+1], then m retains its value from the previous loop and is the maximum element of L[0:k+2].

It L[k+1] is the maximum element of L[0:k+2], then surely it is also greater than any element in L[0:k+1]. Hence, m < L[k+1]. In the body of the loop, the if condition will then re-assign m to be L[k+1]. Thus, at the end of the loop, m = L[k+1] and m is the maximum element of L[0:k+2].

Therefore, by induction, the loop invariant holds for all iterations of the loop and thus max(L) correctly computes the maximum element of L.

Proving that a loop invariant holds for every loop in a program is one step toward proving or verifying that the entire program is correct.

Generally, formal program verification is a very difficult task. For more information, consider reading the articles Loop Invariant and Formal Verification.

Later in your studies in computer science, you will see loop invariants a program verification again. When that time comes, remember induction!