Invariants

After writing an application, a programmer typically tests it thoroughly. Creating an exhaustive set of tests often is quite difficult, and it is always possible that a particular case remains untested. One technique that can help you test your programs thoroughly is to use invariants. An invariant is an assertion (see Section 13.13) that is true before and after the a portion of your code executes. Invariants are mathematical in nature and their concepts are more applicable to the theoretical side of computer science.

The most common type of invariant is a loop invariant. A loop invariant is an assertion that remains true

• before the execution of the loop,
• after every iteration of the loop body, and
• when the loop terminates.

A properly written loop invariant, can help you code a loop correctly. There are four steps to developing a loop from a loop invariant.

1. Set initial values for any loop control variables.
2. Determine the condition that causes the loop to terminate.
3. Modify the control variable(s) so the loop progresses toward termination.
4. Check that the invariant remains true at the end of each iteration.

As an example, we will examine method linearSearch from class LinearArray in Fig. 16.2. The invariant for the linear search algorithm is:

       for all k such that 0 <= k and k < index
            data[ k ] != searchKey

For example, suppose index equals 3. If we pick any non-negative number less than 3 such as 1 for the value of k, the element in data at location k in the array does not equal the searchKey. This invariant basically states that the portion of the array, called a subarray, from the start of the array up to but not including the element at index does not contain the searchKey. A subarray can have no elements, or it can encompass the entire array.

According to Step 1, we must first initialize control variable index. From the invariant, we see that if we set index to 0, then the subarray contains zero elements. Therefore, the invariant is true because a subarray with no elements cannot contain a value that matches the searchKey.

The second step is to determine the condition that causes the loop to terminate. The loop should end after searching the entire arraywhen index equals the length of the array. In this case, no element of array data matches the searchKey. Once the index reaches the end of the array, the invariant remains trueno elements in the subarray (which in this case is the entire array) equal the searchKey.

For the loop to proceed to the next element, we increment control variable index. The last step is to ensure the invariant remains true after each iteration. The if statement (lines 2627 of Fig. 16.2) determines whether data[ index ] equals the searchKey. If so, the method finishes and returns index. Because index is the first occurrence of searchKey in data, the invariant is still truethe subarray up to index does not contain the searchKey.