Deriving a loop from its loop invariant

Unit 3.2 Deriving a loop from its loop invariant

In the spirit of the quote from Dijkstra in Unit 3.1, given the precondition, postcondition, and loop invariant, it is the proof outline that these create that should guide the development of the program. Let us illustrate this for \({\bf Algorithm~1}\text{.}\) (In Unit 3.3, we will go a step further and systematically derive the loop invariant.)

Let us pretend that we don't know about \({\bf Algorithm~1} \) but we do have some means for determining the loop invariant that allows it to be proven correct, together with the precondition and the postcondition. We can place this information into our outline for a proof of correctness, which we will refer to as the worksheet since we will systematically fill it with assertions and commands.

Now, if we can derive commands that make make the loop invariant true at the indicated points in the algorithm and we can reason that the loop eventually terminates in a state where the loop invariant together with the loop guard being false implies the postcondition holds, then we will have derived a correct program.

The condition under which the \({\bf while} \) loop continues to execute, \(G \text{,}\) is called the loop guard. If the loop correctly maintains the loop invariant and the execution exits the loop, then after that loop the condition

\begin{equation} y = \sum_{i=0}^{k-1} a_i x^i ~\wedge ~ 0 \leq k \leq n ~\wedge~ \neg G \label{eqn-after-loop}\tag{3.1} \end{equation}

is true. We must choose \(G \) so that (3.1) implies the postcondition

\begin{equation*} y = \sum_{i=0}^{n-1} a_i x^i . \end{equation*}

Clearly, choosing \(G \) equal to \(k \neq n \) meets the desired criteria. This can then be substituted for \(G \) in the worksheet, which yields

Note that the loop invariant and the postcondition have guided us to a correct loop guard.

Next, we need to initialize variables \(y \) and \(k\) so that the loop invariant is true before the loop:

\begin{equation*} \begin{array}{l} \left\{ 0 \leq n \right\} \\ y := \mbox{?} \\ k := \mbox{?} \\ \left\{ y = \sum_{i=0}^{k-1} a_i x^i ~\wedge ~ 0 \leq k \leq n \right\} \end{array} \end{equation*}

Initializing \(y := 0 \) and \(k := 0 \) has the desired effect, since the Hoare triple

\begin{equation*} \begin{array}{l} \left\{ 0 \leq n \right\} \\ y := 0 \\ k := 0 \\ \left\{ y = \sum_{i=0}^{k-1} a_i x^i ~\wedge ~ 0 \leq k \leq n \right\} \end{array} \end{equation*}

evaluates to true. This initializiation is added to the worksheet:

Note that the precondition and the loop invariant postcondition have guided us towards a correct initialization of \(y \) and \(k \text{.}\)

This leaves us to determine the commands that make the body of the loop correct. In other words, commands such that the loop invariant is maintained. Notice that performing no computation in the body of the loop has the desired result. However, that would mean that \(k \) is never incremented and hence the loop never completes for \(k \neq 0 \text{.}\) This leads us to increment (rather than decrement) \(k \text{:}\)

Note that the initialization of \(k \) to zero together with the loop guard \(k \neq m \) have led us to increment \(k\) in the loop body.

We can now reason about what the state of the variables must be before \(k \) is incremented: If \(k:=k+1 \) leaves us in a state where

\begin{equation*} y = \sum_{i=0}^{k-1} a_i x^i ~\wedge ~ 0 \leq k \leq n \end{equation*}

is true, then before incrementing \(k \) the variables must be in a state where

\begin{equation*} y = \sum_{i=0}^{(k+1)-1} a_i x^i ~\wedge ~ 0 \leq (k+1) \leq n \end{equation*}

is true. This yields

How an assignment and a postcondition dictates the state that the variables must be in before that assignment requires a textual substitution of the expression being assigned into every occurance of the variable in the postcondition. Details go beyond this note.

Finally, we must determine how \(y \) must be updated in order to make the Hoare triple

\begin{equation*} \begin{array}{l} \left\{ y = \sum_{i=0}^{k-1} a_i x^i ~\wedge ~ 0 \leq k \leq n ~\wedge ~ k \neq n \right\} \\ y := ? \\ \left\{ y = \sum_{i=0}^{(k+1)-1} a_i x^i ~\wedge ~ 0 \leq (k+1) \leq n \right\} \end{array} \end{equation*}

true. We can manipulate the postcondition for this Haore triple to find it is equivalent to

\begin{equation*} \begin{array}{l} \left\{ y = \sum_{i=0}^{k-1} a_i x^i ~\wedge ~ 0 \leq k \leq n ~\wedge ~ k \neq n \right\} \\ y := ? \\ \left\{ y = \sum_{i=0}^{k-1} a_i x^i + a_k x^k ~\wedge ~ 0 \leq (k+1) \leq n \right\} \end{array} \end{equation*}

which then suggests the update

\begin{equation*} y := y + a_k x^k \end{equation*}

with which we complete the worksheet:

If desired, the assertions can now be removed, leaving us with the correct algorithm.

It is important to note that at every step the proof of correctness of the program guided the insertion of assertions (in form of predicates) and commands in the worksheet. Thus, we have (almost) achieved what Dijkstra advocated: We have let correctness proof and program grow hand in hand.