Loop Invariants

Invariant

A loop invariant is a boolean expression that is true each time the loop guard is evaluated. Typically the boolean expression is composed of variables used in the loop. The invariant is true every time the loop guard is evaluated. In particular, the initial establishment of the truth of the invariant helps determine the proper initial values of variables used in the loop guard and body. In the loop body, some statements make the invariant false, and other statements must then re-establish the invariant so that it is true before the loop guard is evaluated again.

Invariants can serve as both aids in recalling the details of an implementation of a particular algorithm and in the construction of an algorithm to meet a specification.

For example, the partition phase of Quicksort is a classic example where an invariant can help in developing the code and in reconstructing the code. An invariant is shown pictorially and as the postcondition of the function partition below. The initial value of pivot is left. This ensures that the invariant is true the first time the loop test is evaluated. When pivot is incremented in the loop, the invariant is false, but the swap re-establishes the invariant.

int partition(vector<string> & a, int left, int right) // precondition: left <= right // postcondition: rearranges entries in vector a // returns pivot such that // forall k, left <= k <= pivot, a[k] <= a[pivot] and // forall k, pivot < k <= right, a[pivot] < a[k] // { int k, pivot = left; string center = a[left]; for(k=left+1, k <= right; k++) { if (a[k] <= center) { pivot++; swap(a[k],a[pivot]); } } swap(a[left],a[pivot]); return piv; }

The invariant for this shode can be shown pictorially.


Owen L. Astrachan
Last modified: Fri May 15 15:32:35 EDT 1998