4.3: Loop Invariant

Mathematical induction is a foundation for the logic we use when we are using a looping statement in a program. In our programming class, we are frequently asked to use a looping statement in a program, most of times, we code the program with a looping statement, and then test it with a few sample data. If the looping statement produces correct results with those testing data, we simply accept the correctness of the looping statement we use and assume it will work for all cases.

Example

Write a function that receives a positive integer (a natural number), and then produces the sum of squares of all the numbers from 0 to the number the function receives. For example, if the function receives 5, then the function should produce 0²+1²+2²+3²+4²+5² which is 55

This is a simple programming assignment; the code is shown as following:

We normally check the correctness of this function by entering a few of testing data, such as 5, 6, and 7 in the main(). If the results are all correct, then we assume this function will work for any positive integers we may enter. For some simple calculation, like this one, it will be fine. However, for some complicated calculation, the correctness may not be obvious. Especially, if the result of a function is related to a life and death situation, then we can't just accept the correctness of the function by the results that come from a few of sample data. We will need a solid proof.

In this example, even we don't have to, we would like to introduce the way of proving the correctness of the looping statement we used in the function sumSquares().

First, we explain what is a "Loop Invariant"

Definition

A loop invariant is a predicate that is true before the loop begins and it is also true after each iteration of the loop.

For the looping statement we use in the function sumSquares(), consider the predicate "s = 0²+1²+2²+3², ..., + i², where i is the value of the looping variable after each iteration", if we can prove it is a loop invariant, then it will be true before the looping statement begins and it also true after each iteration. In particular, it will be true after the last iteration. That means s = 0²+1²+2²+3², ..., + n² is true and this proves the looping statement produces the result we expect.

However, the process of proving is not always simple, but we want to get it a try.

Proof

To prove the predicate "s = 0²+1²+2²+3², ..., + i²" is a loop invariant, we need to prove it is true before the loop begins and it is also true after each iteration.

Before the loop begins, s = 0 and i = 0, so the predicate "s = 0²" is true.

Now, we need to prove the predicate is also true after each iteration of the loop. We will use mathematical induction for the proof.

It is not too difficult to see that, after the first iteration, the value of the looping variable i is 1, and, since s=s+i*i, s=1. Thus s = 0²+1², so the predicate is true

Assume that the predicate is true after the i iterations, that means, after i iterations, s = 0²+1²+2²+3², ..., + i². Now we need to prove that, after i+1 iterations, we have s = 0²+1²+2²+3², ..., + (i+1)²

In the ith iteration, the value of the looping variable is i and in the (i+1)th iteration, the value of the looping variable will be i+1, thus, after i+1 iterations, s = s + (i+1)(i+1). On the right side of equal sign, the value of s is 0²+1²+2²+3², ..., + i², thus, after the i+1 iterations, s = 0²+1²+2²+3², ..., + i²+ (i+1)(i+1) = 0²+1²+2²+3², ..., + (i+1)². The proof is completed.

With such strict proof, we can make sure the loop we use produces correct result for any given positive integer.

It may seem difficult for you to grasp the logic we use in this proof. No worries, we can't become an expert after one logic class. As you become mathematically mature, you will have much more strength to handle such task.

What we do need to know here is we can't prove the correctness of a looping statement just by testing it with sample data. Sometimes, even with a large set of sample data, we still can't make sure a looping statement will produce the correct result.

Example

Following program contains a user-defined function getLargest() which receives an integer array along with its length, and then returns the largest number in the array it receives

In the main(), we test this function with an array, it works fine. The function produces correct result for this sample data. We can test the function with over hundreds of sample data. Even the results are all correct, we still can't say the function will work for all integer arrays. We can easily find an integer array, such as y[5] = {-5, -2, -10, -4, -7}, which the function will produce an incorrect result.

Prove the correctness of programs is a big topic and mathematical induction is only one of the tools we can use in this area.