To give an explanation of this requires a problem in which to frame the discussion. I propose the Dutch National Flag problem, likely first proposed by Dijkstra, but I'm not positive.
I'll pose the problem first and discuss the solution using invariants.
The Problem Taken from The Science of Programming.
You have an array of n elements. Each element is a color, red, white, or blue. You want to "sort" the array so that all of the low index cells are red, all of the high index sells are blue, with the white cells between them.
The number of tests should be kept to a minimum. Cells may be permuted with swap (only). The algorithm you develop should require only a single pass over the array and be linear time.
This answer is in process and will be updated. If you want to try to solve it in the interim, the precondition is that the colors are randomly arranged and the postcondition is as described above: [red*, white*, blue*]
Discussion: There are many ways to develop a loop invariant, as discussed in Gries. One way is to weaken the postcondition. I will use [red*, white*, any*, blue*] as the weakened condition and the loop invariant. Such an array configuration can be described with three variables:
The definition of these is as follows: Every cell from
lastRed is RED. Every cell from
lastRed + 1 through
index - 1 is WHITE. Every cell from
lastBlue through the end is BLUE
To establish the invariant prior to the loop:
lastRed = -1;
index = 0;
firstBlue = flag.length; // flag is the array variable, initially random.
With these definitions, the invariant is true with the array in state [ any* ].
Solution: The solution is to run a loop that takes the any* section from "all" to "empty". You can do that either by (a) increasing
index, which breaks the invariant, and then re-establishing the invariant, or (b) by decreasing
firstBlue and re-establishing. Looking at $flag[index]$ will tell you what to do. Swap two cells as needed. A three case "switch" or equivalent is the body of the loop.
The invariant along with
index == firstBlue is the postcondition. Therefore the while loop test condition is
index < firstBlue QED
Note that it is a linear pass over the array, but with two variables moving toward each other from the end. Cool as a moose.
Note 1: The Science of Programming book has many other ideas for coming up with an invariant. This was just one possibility. The book is well organized around that idea. In general, though, the invariant of a loop emerges somehow from the pre and/or postconditions.
Note 2: It shouldn't take much, after doing this exercise, to convince a student that with four values instead of three it is only a bit harder to "sort" in linear time. Actually, any list/array of values from a finite set can be sorted in linear time. Radix sort works, of course, but so does this.