Skip to main content

Unit 2.4 Proving the loop correct

Link to Logic 2.4.

Let \(P( k ) \) be a predicate that is a function of a nonnegative integer \(k \text{.}\) If it can be shown that

  • Base case: \(P( 0 ) \) is true and

  • Inductive Step: Assuming the Inductive Hypothesis (I.H.) that \(P( k ) \) is true for arbitrary \(k \geq 0 \text{,}\) we can prove that \(P( k+1 ) \) is true.

Then we can conclude that \(P( n ) \) is true for all \(n \geq 0 \text{.}\)

This is known as the Principle of Mathematical Induction (PMI).

(The Principle of Mathematical Induction can take a number of different forms, of which this is one that works well in our setting.)

In reasoning about the correctness of a loop, one asks the question "What is true about the variables before and after each iteration?" The predicate that captures this is called the loop invariant. For our algorthm, the answer to this question is that \(y\) contains the sum of the terms of the polynomial "so far." In words: The sum of the first \(k \) terms, where \(k \) is between \(0 \) and \(n \) (inclusive \(0 \) and \(n \)). This translates to

\begin{equation} y = \sum_{i=0}^{k-1} a_i x^i ~\wedge~ 0 \leq k \leq n. \label{eqn-loop-invariant}\tag{2.1} \end{equation}

Here, \(\wedge \) indicates the logical "AND" operator.

Link to Logic 2.5.

The following truth table defines the \(\wedge \) (logical AND) operator:

\begin{equation*} \begin{array}{| c c | c |} \hline p \amp q \amp p \wedge q \\ \hline T \amp T \amp T \\ T \amp F \amp F \\ F \amp T \amp F \\ F \amp F \amp F \\ \hline \end{array} \end{equation*}

Let us annotate our algorithm with the loop invariant in (2.1).

Here is how we reason that the loop is correct.

  • The predicate \(P( k ) \) in Link to Logic 2.4 is the loop invariant

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

  • Base case:. If we start in a state where \(0 \leq n \) and initialize \(y := 0; k := 0 \text{,}\) then we end up in a state where \(P(0) \text{,}\) the loop invariant, is true since \(P( 0 ) \) (the state of the variables just before the loop) evaluates to true:

    \begin{equation*} 0 = \begin{array}[t]{c} \underbrace{ \sum_{i=0}^{0-1} a_i x^i } \\ \mbox{sum over} \\ \mbox{empty range} \end{array} ~\wedge~ 0 \leq 0 \leq n \end{equation*}

    implifies to

    \begin{equation*} 0 \leq n \end{equation*}

    This establishes that the loop invariant holds before the first iteration of the \({\bf while} \) loop.

  • Inductive step: Assuming that \(P( k ) \text{,}\) the loop invariant, is true at the top of the loop (and hence \(k \neq n \)), it can be reasoned that the loop invariant is again true at the bottom of the loop. In other words, it can be shown that 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 := y + a_k \times x^k \\ k := k+1 \\ \left\{ y = \sum_{i=0}^{k-1} a_i x^ i ~\wedge~ 0 \leq k \leq n \right\} \end{array} \end{equation*}

    is true. One way to see this is to add one more assertion in the program:

    This lets us reason "by examination" that if the loop invariant is true at the top of the loop body, then it is again true at the bottom of the loop body. (There are more formal ways of proving this that go beyond the scope of this note.)

  • By the PMI, the loop invariant holds before and after every iteration of the loop.

It is easy to see that eventually the loop terminates:

  • Initially \(k = 0 \text{,}\)

  • each iteration increments \(k \text{,}\) and

  • the condition that keeps execution in the loop is \(k \neq n \text{,}\) where we know that \(0 \leq n \text{.}\)

When the loop is exited, we know that

\begin{equation} y = \sum_{i=0}^{k-1} a_i x^ i ~\wedge~ 0 \leq k \leq n ~\wedge~ \neg( k \neq n ). \label{eq-afterloop}\tag{2.2} \end{equation}

Since \(\neg( k \neq n ) \) is equivalent to \(k = n \text{,}\) the condition in (2.2) implies that the desired result has been computed:

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

We conclude that this program correctly evaluates the polynomial.

Link to Logic 2.6.

The following truth table defines the \(\neg \) (logical NOT) operator:

\begin{equation*} \begin{array}{| c | c |} \hline p \amp \neg p \\ \hline T \amp F \\ F \amp T \\ \hline \end{array} \end{equation*}