# 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;
```
What is the invariant?

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;
}
```

Thomas P. Kelliher
Thu Apr 11 12:43:29 EDT 1996
Tom Kelliher