Loop Invariants

It is hard to keep track of what is happening with loops. Loops which don't terminate or terminate without achieving their goal behavior is a common problem in computer programming. Loop invariants help. A loop invariant is a formal statement about the relationship between variables in your program which holds true just before the loop is ever run (establishing the invariant) and is true again at the bottom of the loop, each time through the loop (maintaining the invariant).

Here is the general pattern of the use of Loop Invariants in your code: 

   ...
   // the Loop Invariant must be true here
   while ( TEST CONDITION ) {
      // top of the loop
      ...
      // bottom of the loop
      // the Loop Invariant must be true here
   }
   // Termination + Loop Invariant = Goal
   ...
Between the top and bottom of the loop, headway is presumably being made towards reaching the loop's goal. This might disturb (make false) the invariant. The point of Loop Invariants is the promise that the invariant will be restored before repeating the loop body each time.

There are two advantages to this:

  1. Work is not carried forward to the next pass in complicated, data dependent ways. Each pass through the loop in independent of all others, with the invariant serving to bind the passes together into a working whole.
  2. Reasoning that your loop works is reduced to reasoning that the loop invariant is restored with each pass through the loop. This breaks the complicated overall behavior of the loop into small simple steps, each which can be considered separately.

The test condition of the loop is not part of the invariant. It is what makes the loop terminate. You consider separately two things: why the loop should ever terminate, and why the loop achieves its goal when it terminates. The loop will terminate if each time through the loop you move closer to satisfying the termination condition. It is often easy to assure this: e.g. stepping a counter variable by one until it reaches a fixed upper limit. Sometimes the reasoning behind termination is more difficult.

The loop invariant should be created so that when the condition of termination is attained, and the invariant is true, then the goal is reached:

invariant + termination => goal It takes practice to create invariants which are simple and relate which capture all of goal attainment except for termination. It is best to use mathematical symbols to express loop invariants, but when this leads to over-complicated situations, we rely on clear prose and common-sense.

Example: Find the index of the minimum value in an array of integers.

Here is the general idea. Let us call the array A, which has n elements in it. We keep two variables, nextToCheck and smallestSoFar We initially set smallestSoFar to 0, and compare A[1], A[2], ..., A[n-1] against A[smallestSoFar] If the current comparision shows a smaller value, we update smallestSoFar.

Here is the Loop Invariant:

  1. smallestSoFar in [0,nextToCheck),
  2. and for all k in [0,nextToCheck), A[k] >= A[smallestSoFar].
Note that [a,b) means all integers from a to b, including a, but not including b.

We set the Loop Invariant true before the loop by setting: 

   nextToCheck = 1 ;
   smallestSoFar = 0 ;
Each time through the loop we increment nextToChekc by one, and fix smallestSoFar to keep the Loop Invariant true: 
   if ( a[smallestSoFar] > a[nextToCheck] ) {
      smallestSoFar = nextToCheck ;
   }
   nextToCheck ++ ;
The termination condition is nextToCheck==n, i.e., no more to check.

The combination of the loop invariant and the termination condition gives that smallestSoFar is the index of the smallest value in the array.

Review:

  1. Check that the Loop Invariant is setup true by the initialization of nextToCheck and smallestSoFar;
  2. Check that each time through the loop, assuming the Loop Invariant true going into the loop, it is true going out of the loop;
  3. Check that headway towards termination is being made (in this case, nextToCheck is always incremented in the loop body).
  4. Check that termination plus loop invariant equals goal attained.

Example: Selection Sort. Given an array A of n integers, sort them by repetitively selecting the smallest among the yet unselected integers. This is done using a single array by keeping the yet unselected integers at the front of the array, from location 0 to i-1, and the selected integers at the back of the array, from location i to n-1.

A trick is used to move the selected integer from the front part of the array to the back part of the array. The selected integer is swapped with the integer in location i-1.

We make use of the function FindMin( int A[], int n ) which returns the index of the minimum value in array A among array locations 0 through n-1. This function was presented in the previous example.

The loop invariant is in terms of numSorted, the number of elements already sorted from the array,

  1. The smallest numSorted values are sorted in descending order in locations [n-numSorted,n),
  2. and the rest are in locations [0,n-numSorted).
Setting 
   numSorted=0 ;
immidately makes the loop invariant true.

Each time through the loop increased numSorted by one. To do this, the smallest from the front of the array needs to be selected and swapped to the back of the array, 

   i = findMinumum(A,n-numSorted) ;
   numSorted++ ;
   swap( A, i, n-numSorted ) ;
Terminate when numSorted==n.

Review:

  1. Check that the Loop Invariant is setup true by the initialization of numSorted.
  2. Check that each time through the loop, assuming the Loop Invariant true going into the loop, it is true going out of the loop;
  3. Check that headway towards termination is being made. Here headway is obious: numSorted is incremented each time through the loop.
  4. Check that termination plus loop invariant equals goal attained.
The finished program is SelectionSort.C