Something to Ponder

Moral of the story: take your time to write really good software.

Loop Invariant

The word, “invariant”, means "no change". An invariant is an assertion that is always true. In particular, there are three points in a program where a loop invariant is required to be true:

Method for developing with loop invariant:

Here is a loop-invariant based proof and associated program to find the largest element of an array, A, where the array's dimenions are declared,

int A[0..n];

At the end of our loop's execution we want j to be the index of a largest element. This idea is captured with the following boolean expression,

POST: forall x in 0..n, A[j]>=A[x]

If you don't like the forall expression, let's rewrite the above expression into it's longhand equivalent,

A[j]>=A[0] and A[j]>=A[1] and ... and A[j]>=A[n]

INV: forall x in i..n, A[j]>=A[x]

INV &&  not (guard) ==> POST

( i != 0 )

i = i - 1;

if A[i] > A[j] then j = i

assert(INV);
i = i - 1;
if A[i] > A[j] then j = i
assert(INV);

i = n;

wp("i = n"; INV)

wp("i = n"; forall x in i..n, A[j]>=A[x])

forall x in n..n, A[j]>=A[x]

A[n]>=A[n]

true

assert(true);      // true means can we start the program in any state
i = n;
assert(INV);

The invariant is specified formally as,

INV: (forall u=1:i-1 forall v=i:n  A[u] <= A[v]) and sorted(A[i:n])

An another, less formal way to express is through pictures,

          1                                      i    i+1               n
        +-------------------------------------------+---------------------+
INV:	|        all A[1:i] <= all A[i+1:n]         |       sorted        |
        +-------------------------------------------+---------------------+

Even less formal is,

          1                                      i    i+1               n
        +-------------------------------------------+---------------------+
INV:	|               <= A[i+1:n]                 |       sorted        |
        +-------------------------------------------+---------------------+

Now we can almost write the guard. But the most important part is that we well author the guard code (the expression inside the while loop test) by reasoning statically.

The guard is obtained by envisioning the postcondition, shown here, and asking what value of i will achieve this?

          1                                                             n
        +-----------------------------------------------------------------+
POST:	|                              sorted                             |
        +-----------------------------------------------------------------+

Clearly,

INV && (i==0)

will do this. So the guard is written using the boolean test,

i != 0

which is the negation of (i==0).

The program, developed this far, looks like this.

// some init code goes here
while (i != 0) {
  // some loop body code goes here
}

Annotated with asserts, the program looks like this.

assert (TRUE);
// some init code goes here
assert (INV);
while (i != 0) {
  assert (INV);
  // some loop body code goes here
  assert (INV);
}
assert (INV && i==0);   /* same as */   assert (POST);

There are two important things to point out. First, we have been reasoning about the loop termination condition, by reasoning statically. This way we avoid the immature programmer's iterative or repetive thinking. The second point is that we have reasoned about this program by authoring the proof first; and the development of the prove drive the code. Finally, we have reduced or eliminated off-by-one error!

The loop initialization establishes (i.e., makes true) the invariant. So we want a peice of code at the beginning that does this:

assert(true);

//some code goes here

assert(INV);

Or the same written in the traditional Djiktsta notation, where curly braces are used to denote comment syntax in the tradition of Pascal programming.

{ true }

//some code goes here

{ INV }

Intuitively, an approach is to use some initialization code that makes INV true by "moving" i so far to the left that the sorted part is empty. Thus the initialization is just doing easy work of setting i's value, and doesn't require any "hard" sorting work.

	Note
	This is a good time to make some general comments on invariant design. Good invariants are designed to be: Easy to establish. Requiring little or no initialization code. Parameterizable (in this example by the variable, i) Obviously convertable into a postcondition. Logically anding INV with a simple expression should yeild the postcondition.

assert( PRE: true )

  i := n +1;                    // establishes INV

{ INV: (forall u=1:i-1 forall v=i:n  A[u] <= A[v]) and sorted(A[i:n]) 


assert( i==n+1 and INV )

  while ( i != 1 ) {
    ...                         // INV must be true at each iteration...
  }

assert( POST: i==1 and INV )          // negate while loop test condition

NOTE: we can simplify and rewrite as the equivalent,

assert( POST: sorted(A[1:n]) )

Intuitively know the loop body needs to move i to the left, which breaks (makes false) the invariant, so we code this:

i := i - 1;

Picture of broken invariant, i.e., what can be asserted just after this assignment statement,

          1                                i   i+1    i+2               n
        +-------------------------------------------+---------------------+
        |                                           |       sorted        |
        +-------------------------------------------+---------------------+

Now the job is to re-establish the invariant, INV, and note, we could re-establish the invariant with:

  i := i + 1;

But this does so so trivially as to make no progress towards the post condition and the ultimate goal of sorting. Better, instead to reestablish the invariant by scanning for the largest element in A[1:i+1], say it's A[m], and swapping the largest element A[m] into the right place, i.e., swapping with A[i+1]

This scanning business needs to be done with an inner loop - we can also design using another invariant, INV2 (two pictures).

          1                                     i+1   i+2               n
        +-------------------------------------------+---------------------+
INV2:	|           all <= all A[i:n]               |       sorted        |
        +-------------------------------------------+---------------------+

        AND

          1             j            m          i+1   
        +-------------+------------+---+------------+--...
	|             |   <= A[m]  |   |   <= A[m]  |  
        +-------------+------------+---+------------+--...

	Design Strategy
	Note, we design the inner loop by formulating its invariant, first. Code will come later.

{ INV: (forall u=1:i-1 forall v=i:n  A[u] <= A[v]) and sorted(A[i:n]) 

{ PRE: true }

  i := n +1;                    // establishes INV

{ i==n+1 and INV }

  while ( i != n ) {
                                // INV at each start of iteration...
       i := i - 1;              // INV broken

     { INV2: (forall u=1:i forall v=i+1:n  A[u] <= A[v]) and sorted(A[i+1:n]) 
            and
            A[m] == max(A[j:i]) }

       j := i; m := i;		// establishes INV2

     { j==i==m  and INV2 }

       while (j != 1) {
         .
         .
         .
       }

     { POST: INV2 and j==1 }
  }

{ POST: sorted(A[1:n]) }

Important Subtilty

The predicate, sorted(), here is different than the other sort algorithms, e.g., insertion sort. Here, the meaning is that all the sorted elements are indeed in their final positions w.r.t. the whole array. Formally, sorted() is defined as, forall X in [i..n], forall Y in [1..X], A[X] <= A[Y] Whereas in the insertion sort's algorithm, Y ranges from i..X Must be very careful about these "informalisms". Note in bubble sort, sorted() can just mean relative to the array slice without consideration for the array elements not in that slice, but selection sort, sorted() has a stronger meaning: the sorted array elements are in their final positions w.r.t. the whole array. This has a subtle implication when establishing the initial invariant, the sorted slice must be empty, because sorted() might not be true for A[n]. Then again, even this definition for the predicate sorted() does not capture the notion of a permutation of the initial array elements. Which demonstrates an incompleteness in the notation, since we do not have a notation for initial values. Also we should have introduced the function, perm( A, B ), which is true when A contains all the same elements as B possibly in a rearranged permutation.