It is hard to keep track of what is happening with loops. A Loop invariant is a formal statement about the relationship between variables in program which holds true just before the loop is ever run (establishing the invariant) and is true again at the bottom of the loop, each time through the loop (maintaining the invariant). It state that a desired property is maintained in loop. General pattern of the use of Loop Invariants is shown below:
...
// Loop Invariant must be true here
while ( TEST CONDITION ) {
// Top of the loop
...
// Bottom of the loop
// the Loop Invariant must be true here
}
// Termination + Loop Invariant = Goal
...
Between the top and bottom of the loop, headway is presumably being made towards reaching the loop’s goal. This might disturb (make false) the invariant. The point of Loop Invariants is the promise that the invariant will be restored before repeating the loop body each time.
The test condition of the loop is not part of the invariant. It is what makes the loop terminate. You consider separately two things: why the loop should ever terminate, and why the loop achieves its goal when it terminates. The loop will terminate if each time through the loop you move closer to satisfying the termination condition. It is often easy to assure this: e.g. stepping a counter variable by one until it reaches a fixed upper limit. Sometimes the reasoning behind termination is more difficult.
In short Loop invariant proof is broken down into the following parts
- Initialization: It is true (in a limited sense) before the loop runs.
- Maintenance: If it’s true before an iteration of a loop, it remains true before the next iteration.
- Termination: It will terminate in a useful way once it is finished.
For example, in Java, a while loop has the following form, where B is a boolean expression (that we shall call the guard of the loop) and S is a sequence of commands/instructions (that we shall call the body of the loop).
while (B)
{ S }
A flow chart that indicates the steps taken in executing such a loop is as follows:
+-------+
| start |
+-------+
|
| <--- Q (the precondition)
| holds here (assumption)
|
+-------------------------> | <--- P (the invariant)
| holds here (every time)
| |
| |
| / \
| / \
| true / B \ false
| +<------ \ / -------->+
| P & B ---->| \ / |
| holds | \ / | <---- P & !B holds here
| here v |
| +---+ | <---- R (postcondition)
| | S | v is to hold here
| +---+ +------+
| | | stop |
| | +------+
+<--------------+
The flow chart is annotated to indicate the “locations” at which
- we assume that the precondition Q holds,
- we want the postcondition R to hold, and
- we want the loop invariant P to hold.
Finding a Maximum Element in an Array
Suppose we have an array a[0..n-1] (where n>0) of, say, integers, and we want to determine the maximum among the values in a[]. Using maxVal as the output variable, the desired postcondition is
For brevity, henceforth we shall abbreviate the array segment <a[0], a[1], ..., a[k]> by a[0..k].). Using the approach described above, we replace “constant” n in the postcondition by variable k in order to obtain P: maxVal == Max(a[0..k-1]) as a candidate for a loop invariant. This leads us to propose the following program skeleton:
// {precondition: a.length > 0}
k = 1;
< code to establish P(k:=1): maxVal == Max(a[0..0]) >
// {loop invariant P: maxVal == Max(a[0..k-1])}
while ( k != n ) {
< code to establish P(k:=k+1): maxVal == Max(a[0..k]) >
k = k+1; // re-establishes P
}
// { maxVal == Max(a[0..k-1]) & k == n }
// {postcondition R: maxVal == Max(a[0..n-1]) follows from above}
Having set k to 1, to establish P(k:=1) requires simply that maxVal be initialized to the maximum of a[0..0], which is obviously a[0] itself. As for establishing P(k:=k+1) inside the loop before incrementing k, consider that, at this point, we have P (i.e., maxVal == Max(a[0..k-1])) and that we want to change maxVal to establish maxVal == Max(a[0..k]).
How are Max(a[0..k-1]) and Max(a[0..k]) related? Given that a[0..k-1] and a[0..k] are the same, except for the latter containing one extra element, —namely, a[k]— clearly the only difference is this: if a[k] is bigger than the maximum element in a[0..k-1], it is the maximum of a[0..k]; otherwise, the maximum of the two array segments is the same. So we refine our program to get
k = 1;
maxVal = a[0]; // {P(k:=1): maxVal == Max(a[0..0])}
// {loop invariant P: maxVal == Max(a[0..k-1])}
while (k != n) {
if ( a[k] > Max(a[0..k-1]) )
{ maxVal = a[k]; }
else
{ maxVal = Max(a[0..k-1]); }
// {P(k:=k+1): maxVal == Max(a[0..k])}
k = k+1; // {P: maxVal == Max(a[0..k-1])}
}
// { maxVal == Max(a[0..k-1]) & k == n }
// {postcondition: maxVal == Max(a[0..n-1])}
By the fact that maxVal == Max(a[0..k-1]) holds at the time that the “if” statement is executed, the two instances of Max(a[0..k-1]) appearing there can be replaced by maxVal. We get
k = 1;
maxVal = a[0];
// {loop invariant P: maxVal == Max(a[0..k-1]) }
while (k != n) {
if ( a[k] > maxVal )
{ maxVal = a[k]; }
else
{ maxVal = maxVal; }
// {P(k:=k+1): maxVal == Max(a[0..k])}
k = k+1; // re-establishes P
}
// {maxVal == Max(a[0..k-1]) & k == n}
// {postcondition: maxVal == Max(a[0..n-1]) (follows from above)}
Because the body of the else part has no net effect, we can omit it (or replace it by a statement that has no effect, such as { } in Java), giving us as the final program:
k = 1;
maxVal = a[0];
// {loop invariant P: maxVal == Max(a[0..k-1])}
while (k != n) {
if (a[k] > maxVal)
{ maxVal = a[k]; }
// {P(k:=k+1): maxVal == Max(a[0..k])}
k = k+1; // re-establishes P
}
// { maxVal == Max(a[0..k-1]) & k == n }
// {postcondition: maxVal == Max(a[0..n-1]) }