Loop invariants help us to see that an algorithm is correct. Three things should be true about loop invariants. (See Introduction to Algorithms1, pages 18-20.)
- Initialization: the loop invariant is true before the first iteration of the loop.
- Maintenance: the loop invariant is true after each iteration of the loop. (Note that the loop invariant may become temporarily false during the loop, but by the end of the loop, it must be true.)
- Termination: when the loop ends, the invariant gives us a useful property that helps show that the algorithm is correct.
As an example, let’s consider the loop invariants for insertion sort. The loop invariant for insertion sort are the following: first, for each iteration through the outer loop, where j
is an index of the loop from 1
to len(slice)-1
, the subslice slice[0:j-1]
contains the elements from slice[0:j-1]
, but in sorted order; second, the inner loop only adds items to xs[i:j]
if those elements are less than or equal to key
. (I think that there should be a better way to describe the second invariant.)
- Initialization: initially the subslice
xs[0:1]
contains one item; therefore, it is trivially in order. - Maintenance: informally, the point of the inner loop is to move
key
down as far as possible; therefore, at the end of the inner loop, everything inxs[i:j]
is greater than or equal to key. More formally, we explicitly test whetherxs[i] > key
before doing anything. Ifxs[i]
is not greater thankey
, theni
remains unchanged and when we runxs[i+1] = key
, we are placingkey
back where it started sincei
was defined asj-1
. Therefore,i+1
is j whenever i has not changed. On the other hand, ifxs[i]
is greater thankey
, then we do two things. First, we slidexs[i]
rightward. Second, we decreasei
. Thus, when we assign key toxs[i+1]
,xs[i+1]
has becomej-1
. Since the key was previouslyxs[j]
, we have thus movedkey
down one and the larger number up one. Thus,xs[0:j-1]
maintains the first invariant. - Termination: when the outer loop finishes,
j
islen(xs)
. Thus, we can say that the entire slice (xs[0:len(xs)]
) is in order when the outer loop finishes.
- Initialization: before the loop begins, nothing has been added to
xs[i:j]
, so the invariant is true in a trivial way. - Maintenance: the inner loop has a test that insures that anything larger than
key
is moved upwards. Thus, anything larger than key will end up somewhere inxs[j:]
, and the invariant remains true. - Termination: the inner loop ends in one of two ways. First, the loop ends if reach a value of
i
wherexs[i]
is less than or equal tokey
. (Any such items are kept inxs[i:j]
.) Thus, if the loop ends in this way, the invariant survives termination. Second, the loop explicitly tests for wheni
becomes less than zero. (This test protects us from attempting to index outside the bounds of a slice.) The lower bound ofxs[i:j]
is therefore zero, and based on initialization and maintenance, we know thatxs[0:j]
will have nothing added to it that isn’t smaller than or equal tokey
.
Footnotes
-
Introduction to Algorithms, 3rd edition, Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Clifford Stein. The MIT Press (Cambridge, MA), 2009. ↩