Note: this is not working on IE. Please use Firefox while I work out the problems.
We demonstrate the use of Loop Invariants on the problem of finding the minimum value in an array. The idea is to sweep the array left to right, keeping track of the minimum value seen. At each pass through the loop we include into consideration one more element. We update the minium or not, according to the size of the new value admitted.
In the illustration, the array begins blue and turns red as we sweep. The smallest element so far is indicated by coloring the number yellow. The very rough pseudo code is shown, and the simulation highlights the currently active line of code.
Our Loop Invariant is that we have identified the smallest element so far. That is, the Loop Invariant is: the smallest value among the red cells is colored yellow. The L.I. should be a true. An assertion, or to assert the L.I., is to insist that at that point in the code, the L.I. mus be true. If the L.I. is not true at the point of assertion, then our code is wrong.
A difficult things about L.I.'s is they are best stated mathematically. Note that the statement of the L.I. using colors is more amenable to a mathematical statement that saying "smallest element so far", because the concept of "so far" is hard to explain mathematically. It is always best to make assertions about the relationships in your data at a moment in time, and avoid notions of before or after in time.
The mathematical rendition of our L.I. is:
A pass through the loop involves two actions: first we expand the red region; then we restore the L.I. if it is necessary to do so. Because the L.I. was true before extending the red region by one cell, it is either still true, or if not it is because the element in the newly admitted array cell is smaller than the previously smallest element. In that case we can re-establish the L.I. by making the new smallest element be the newly admitted value.
The first step, extending the red region, is our drive towards termination. The second step is our maintenance of correctness. When both are fulfilled, that is, we are terminated and correct, then our goal is reached.
The L.I. is established (made a true statement) before entering the loop, and is guaranteed to be true when we reach the bottom of the loop. It is therefore also guaranteed to be true when we exit the loop. There is always preamble code before the loop whose role is to establish the L.I. before entry to the loop. This is usually done by creating a very simple situation for which it is easy to establish the L.I. In this case, we initially establish the L.I. by considering the one element array, and its only element to be the element of smallest value.
I hope you have enjoyed this animation of Loop Invariants. Loop Invariants are a great tool helping programmers write correct code. They belong to a family of techniques involving Assertions. Other ways to use Assertions include pre-conditions, post-conditions and data structure invariants.