UNLV CS 477/677
University of Nevada Las Vegas
Howard R. Hughes College of Engineering
Department of Computer Science
My Home Page

Programming Invariants

Programming invariants are useful because they can help us to prove correctness, or complexity, of our code. They can also be useful to us before the code is written, helping guide us to write the code correctly. For example, I never got quicksort right until I decided to write a loop invariant for the partition phase before writing that code.

In most cases, programmers do not write loop invariants, because the code is "obvious." (There is nothing wrong with that, if the code is truly obvious.)

We now consider two of those invariants.

Loop Invariants

  1. A loop invariant of a given loop is a statement which satisfies the following conditions:


    • It is true before the first iteration of the loop.

    • If it is true at the beginning of a given iteration of the loop, it is true at the end of that iteration.


  2. We can transform a C++ for loop into a while loop in a few easy steps, and thus we can assume that all loops are while loops.

    • A for loop has three parameters, separated by semicolons. The first parameter is placed before the while loop, the second is the loop condition, and the third becomes the last statement in the body of the loop. Take a simple example of a for loop: 
      cin >> n;
int sum = 0;
for(int i = 1;i < n;i++)
  sum = sum + i;
cout << sum;
      We write an equivalent while loop: 
      cin >> n;
int i = 1;
while(i < n){
  sum = sum + i;
  i++;
  }
cout << sum;










    • Here is a more complex example, with nested for loops: 
      cin >> n;
for(int i = n; i > 1; i = i/2)
  for(int j = 1; j < i; j++)
    cout << "Hello world" << endl;
      We simply perform the same transformation twice: 
      cin >> n;
int i = n;
while (i > 1){
  int j = 1;
  while (j < i){
    cout << "Hello world" << endl;
    j++;
    }
  i = i/2;
  }
  3. Use of loop invariants in Selection Sort. Selection sort uses the following code to sort an array x of length n. We assume a procedure swap which exchanges the values of its parameters. The input condition is that there is an input array x[1] .. x[n], and the output condition is that the same variables will contain the sorted permutation of the values of the input array. 
    for (int i = 1; i < n; i++){
  int k = i;
  for (int j = i+1; j ≤ n; j++)
    if (x[j] < x[k]) k = j;
  if (k > i)
    swap(x[i],x[k]); 
  }
    We first transform the for loops into while loops. 
    int i = 1;
while (i < n){
  int k = i;
  int j = i+1;
  while (j ≤ n){
    if (x[j] < x[k]) k = j;
    j++;
    }
  if (k > i)
    swap(x[i],x[k]); 
  i++;
  }
    Since there are two loops, we need two loop invariants.

    The purpose of the outer loop is to swap ith smallest element into x[i], or to do nothing if it is already there. The purpose of the inner loop is to find the index of that smallest element, by linear search through the subarrary x[i] .. x[n].
    1. OLI = Outer loop invariant: All the items x[1] .. x[i-1] are in their correct positions.
      More formally, the array items are a permutation of the input array, and, for any 1 ≤ l < i, x[l] is the lth smallest element of the input array.

    2. ILI = Inner loop invariant:
      1. The outer loop invariant holds.
      2. x[k] is the smallest element in the subarray x[i] .. x[j-1].