Deriving loop invariants

Unit 3.3 Deriving loop invariants

In Unit 3.2, we derived a correct program after we were given a loop invariant. This leaves us with the question of how to systematically determine one or more loop invariants, from which one or more programs can then be derived.

The goal of our operation is given by the postcondition

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

As a loop progresses, inherently some computation has completed and some has yet to be performed. To express this, we introduce an index, \(k \text{,}\) and split the range of the summation using this index:

\begin{equation} y = \sum_{i=0}^{k-1} a_i x^i + \sum_{i=k}^{n-1} a_i x^i ~\wedge ~ 0 \leq k \leq n. \label{PME}\tag{3.2} \end{equation}

While the loop is executing, only part of the final result has been computed, leading us to a proposed loop invariant, Invariant 1:

\begin{equation} y = \sum_{i=0}^{k-1} a_i x^i \phantom{+ \sum_{i=k}^{n-1} a_i x^i } ~\wedge ~ 0 \leq k \leq n .\label{LoopInvariant1}\tag{3.3} \end{equation}

Given this loop invariant, an algorithm can be systematically derived as described in Unit 3.2.

Exercise 3.1.

Consider (3.2) and suggest another loop invariant. Derive the corresponding algorithm, using the outline

Hint

Remove the first partial summation.

Solution

An alternative loop invariant is given by Invariant 2;

\begin{equation} y = \phantom{\sum_{i=0}^{k-1} a_i x^i + }\sum_{i=k}^{n-1} a_i x^i ~\wedge ~ 0 \leq k \leq n . \label{AlternativeSimpleInvariant}\tag{3.4} \end{equation}

Mimicking the derivation in Unit 3.2 yields the filled-out worksheet