Channels ▼

Andrew Koenig

Dr. Dobb's Bloggers

Using a Loop Invariant to Help Think About a Program

September 19, 2014

Last week, I talked about how to write a loop invariant. I would like to continue this discussion by paraphrasing a beautifully elegant example that Dijkstra used in A Discipline of Programming.

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)
     
{

           assert(n != 0 || x != 0);
           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)

{

    assert(n != 0 || x != 0);
    double r = 1;



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

        r *= x;

        --n;

    }
    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

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<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

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

 
Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.