Pre-Conditions, Post-Conditions, and Loop Invariants

Tom Kelliher, CS18

Apr. 12, 1996

Pre- and Post-Conditions

Two purposes:

• An aid in design verification
• Very good form of function documentation

A contract between caller (client) and callee (server)

Pre-condition states what must be true upon function entry

Post-condition states what will be true upon exit --- describing the transformation accomplished

Example:

/**********************************************************************

sort

pre-condition: the int array data contains integer values in its first
numElems locations

post-condition: the first numElems values of data are sorted into
ascending order

**********************************************************************/

void sort(int data[], int numElems)
{
   ...
}

What would the pre- and post-conditions be for:

int linkedListInsert(LinkedList& l, int position, ListItem item);

Loop Invariants

Four characteristics:

1. Must be true upon entry into the loop
2. Execution of the loop body must preserve the invariant
3. Invariant must capture the correctness and the meaning of the loop
4. Loop must terminate

Consider the code:

const int SIZE = 100;
int data[SIZE];
int i;
int sum;

// stuff to initialize data

sum = 0;
for (i = 0; i < SIZE; i++)
   sum += data[i];

cout << "Sum: " << sum << endl;

Three more examples:

fact = 1;
for (i = 2; i <= n; i++)
   fact *= n;             // careful!!

void SelectionSort(dataType A[], int N)
{
   for (int Last = N-1; Last >= 1; --Last)
   {
      // select largest item in A[0..Last]
      int L = IndexOfLargest(A, Last+1);

      // swap largest item A[L] with A[Last]
      Swap(A[L], A[Last]);
   }  // end for
}  // end SelectionSort

int IndexOfLargest(const dataType A[], int Size)
{
   int IndexSoFar = 0;  // index of largest item found so far

   for (int CurrentIndex = 1; CurrentIndex < Size;
                              ++CurrentIndex)
   {
      if (A[CurrentIndex] > A[IndexSoFar])
         IndexSoFar = CurrentIndex;
   }  // end for

   return IndexSoFar;  // index of largest item
}  // end IndexOfLargest

Exercises

Determine pre- and post- conditions and loop invariants for the following:

1. A function which computes the sum of the first n elements of the Fibonacci sequence

   int fibSum(int n)
   {
      int prev1 = 1;
      int prev2 = 1;
      int next;
      int sum = 2;
   
      if (n == 1)
         return 1;
      else if (n == 2)
         return 2;
   
      n -= 2;
   
      while (n > 0)
      {
         next = prev1 + prev2;
         sum += next;
         prev1 = prev2;
         prev2 = next;
         --n;
      }
   
      return sum;
   }
   

2. A function which finds the sum of the first five positive values in an integer array with n elements

   int firstFive(int data[], int n)
   {
      int found = 0;
      int sum = 0;
   
      for (i = 0; i < n && found < 5; ++i)
         if (data[i] > 0)
         {
            ++found;
            sum += data[i];
         }
   
      if (found != 5)
         return -1;
      else
         return sum;
   }
   

3. A function which iteratively performs binary search

   int binSearch(int data[], int n, int item)
   {
      int first = 0;
      int last = n - 1;
      int mid
   
      while (first < last)
      {
         mid = (first + last) / 2;
   
         if (data[mid] == item)
            return mid;
         else if (data[mid] < item)
            first = mid + 1;
         else
            last = mid - 1;
      }
   
      return -1;
   }