Loop Invariants

We write loops to accomplish some task, for example, given an array of integers, to find the largest element in the array. The (loop) invariant states what is true at each iteration of the loop (before the test is made). The invariant should be strong enough to allow us to show that the loop accomplishes its intended task.
One can get very formal about (loop) invariants and, in general, about how to show that a program is correct. Our goals here are very modest: just to learn to better understand what we do when we write a loop. We will proceed by examples. I write the invariants in precise english and I give arguments to try convince you that they are valid and useful invariants. If you find the arguments difficult or boring, then skip them, but try at least to understand what each invariant tries to say. And try to think of your programs more in terms of ideas expressed in english than in terms of details of programming statements. We need to become able to reason about what our programs do.

Example 1: Find Largest element in an array

/* return largest value in array a with n elements.*/
int findmax(const int a[], int n)
{
	int who = a[0]; // Represents the largest value found
			// up to now in a.
	for (int k = 0; k < n; ++k) {
	// INVARIANT: for all positions j from 0 to k-1
	// a[j] <= who, thus who is the largest element in the range 0..k-1
	    if (a[k] > who)
		who = a[k];
	}
	return who;
}

1. Is the statement true at each iteration? This involves two things:

   Is the statement true the first time we get to the loop?

   In our case yes, since when we get first to the loop k is equal to 1, thus j can only have the value 0, and we know that who = a[0], thus who >= a[0], thus who >= a[j] for all j from 0 to k-1.

   If the statement is true when k is equal, say, to h, will it be true in the next iteration, when it has value h+1?

   You should agree to this because during an iteration we compare who to the next element of a and, if necessary, update who, which thus remains the largest of the elements seen up to now in a.
   [Notice that we have gone thru what people call "an argument/proof by induction".]

2. Does the invariant allow us to prove that the code accomplishes its intended task?
   In our case we need to show that at the end of the loop who contains the largest value in a. But from the invariant we know that who >= a[j] for j=0,1, ..k-1. When the loop terminates k has value n, thus who >= a[j] for j=0,1,..,n-1. Thus who contains the largest value in a.

Example 2: Looking for an element in an unsorted array

int linearSearch(const int a[], int n, int who)
{
	for (int k = 0; k < n; ++k) {
	// INVARIANT: for all positions j from 0 to k-1, who != a[j]
	    if (a[k] == who) return (k);
	}
	return (-1);
}

Example 3: Looking for an element in a sorted array

int binarySearch(const int a[], int n, int who)
{
	int low = 0;
	int high = n-1;
	while (low <= high) {
	// INVARIANT: if who is in the array a, it is in the range low..high.
	   int mid = (low+high)/2;
	   if (who < a[mid])
		high = mid-1;
	   else if (who > a[mid])
		low = mid+1;
	   else
		return (who);		
	}
	return (-1);
}

Example 4: Sorting an array using selectionSort

/* Given array a with n elements, sort it in non decreasing order,
   using the selection method
 */
void selectionSort(int a[], int n)
{
	for (int limit=n; limit>1; limit--) {
	// INVARIANT1: All elements in range limit..n-1 are in their final
	// sorted position.
	    int w = 0; 
	    for (int k=1; k < limit; ++k) 
	    // INVARIANT2: a[w]>=a[j] for all j in range 0..k-1
		if (a[w] < a[k])
		   w = k;
	    int temp = a[w];
	    a[w] = a[limit-1];
	    a[limit-1] = temp;
	}
}