# 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 & 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