Channels ▼

Andrew Koenig

Dr. Dobb's Bloggers

Using a Loop Invariant to Help Think About a Program

September 19, 2014


The problem is to raise a floating-point number to an integer power. Because C++, unlike the language that Dijkstra used in his book, supports unsigned integers, we shall think about the problem as defining the function declared as

double power(double, unsigned);

Because the second argument is unsigned, we do not need to think about what to do if the exponent is negative.

We might define this function as

double power(double x, unsigned n)      
     if (n == 0)     
              return 1; 
     return x * power(x, n-1);

This is a reasonable definition except for one problem, which I shall describe in a little while. First, let's use an induction proof to convince ourselves that the code is correct. Interested readers may wish to construct this proof for themselves before reading on.

We wish to prove that this function yields xn for all values of n, assuming that the computer is capable of evaluating this function at all. To do so by induction, we observe first that n is a natural number, so proof by induction is relevant. Next, we note that the function is clearly correct if n is 0, except in the specific case in which x is also 0. In that case, the result is undefined, so for the moment we shall accept that the function returns 1 in that case. In effect, we have defined "correct" so that our function works correctly if n is 0.

Our next job is to assume that the function works correctly for all n<k and prove that the function works correctly when n=k. In that case, we return x * power(x, n-1). Therefore,

x * power(x, n-1) 
= x * power(x, k-1)
[because n=k]
= x * xk-1 [because of our assumption that power works correctly for n<k]
= xk [by the nature of exponentiation]

We have just proved that the function works correctly for n=k; by mathematical induction, it works correctly for all values of n.

This function has two problems. First, in order to be able to prove that it works, we had to define it in a way that we might not want. Suppose, for example, we wanted to detect the undefined case in which x and n are both zero. We cannot simply write

double power(double x, unsigned n)      
            assert(n != 0 || x != 0);
           if (n == 0)      
                   return 1; 
           return x * power(x, n-1);

because now our base case is incomplete. For example, to compute 01, our function relies on being able to compute 00. Indeed, we kind of glossed over that reliance in our proof.

The second problem is that in general, recursive functions use an amount of memory proportional to the number of levels of recursion. Even though most computers have lots of memory these days, it would still be nice to avoid the waste. Accordingly, we shall write this function as a loop.

We have a kind of vague idea that we should solve this problem by defining a variable to contain an intermediate result. We might name that variable r for result, and write code that looks like this:

 double power(double x, unsigned n)      
           double r = 1; 
           // We need to do something here  
          return r;

Now we have to figure out how to get r to have the right value before we return. The way to do this is to write down a relationship between x, n, and r that might serve as a loop invariant. In effect, Dijkstra used

// Invariant: Our desired result is r * xn

In other words, r starts out at 1, and when we multiply r by xn, we therefore get our desired result. Our job is now to write a loop that does two things:

  • Each trip through the loop, it brings n closer to zero.
  • It assumes that the invariant is true at the beginning of the loop body, and ensures that it is still true at the end.

If n is zero when the loop terminates, then in order for xn to be our desired result (as the invariant claims), r must be equal to that result because x0 is 1.

If we express the requirements on the loop this way, the loop itself becomes almost trivial to write:

double power(double x, unsigned n) 
    double r = 1;  

    // Invariant: Our desired result is r * xn
    while (n != 0) { 
        r *= x; 
    return r;

To see that the invariant holds through at the end of each trip through the loop, we will use oldr, newr, oldn, and newn to denote the values at the beginning and end of the loop. Then:

Our desired result 
= oldr * xoldn [because of the loop invariant]
= oldr * xnewn+1 [because the loop decreases n by 1] 
= oldr * (x * xnewn) [because of the definition of exponentiation] 
= (oldr * x) * xnewn[because multiplication is associative] 
= newr * xnewn [because newr is oldr * x]

As a result, the invariant is true at the end of each trip through the loop. Because the loop terminates only when n is zero, and because the invariant still holds at that point, r must contain our desired result.

So far, we have used our invariant both to help us write our code and to demonstrate that the code works properly. However, Dijkstra went further than that: He took advantage of the fact that you can do anything inside the loop that meets our two conditions (bringing n closer to zero and maintaining the invariant) to devise a way of making the code dramatically faster. We shall explore that technique next week.

Related Reading

More Insights

Currently we allow the following HTML tags in comments:

Single tags


<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags


<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

