Channels ▼

Andrew Koenig

Dr. Dobb's Bloggers

A Loop Invariant Can Be An Optimization Tool

September 29, 2014

Last week, I discussed how Dijkstra used a loop invariant to help understand the power function, which we expressed as

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;
}

This code is an example of a typical strategy: We start with an unsigned integer, here called n, that we reduce to zero while maintaining an invariant. The invariant is such that once n has become zero, we will know the result that our code intends to compute. In this particular case, that result will be in the variable r.

The most straightforward way to reduce n to zero in a loop is to decrease n by 1 as long as n is not zero. However, there are other ways to reduce n more quickly. In particular, Dijkstra observed that if n is even, we can divide it by 2 and get an exact integer result. Because xn is equal to x(n/2) * x(n/2), we can restore the invariant simply by squaring x. In other words, we can rewrite our code as

double power(double x, unsigned n)

 {

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


        // Invariant: Our desired result is r * xn

        while (n != 0) {

           while (n % 2 == 0) {
               x *= x;
// Break the invariant
               n /= 2; // Restore the invariant
           }
           r *= x; //
Break the invariant
          --n; // Restore the invariant
        }
    return r;
}

We now have two nested loops with the same invariant. Each loop assumes that the invariant is true at the beginning of each trip through the loop; each loop decreases n while maintaining the invariant. The difference between the two is that the inner loop reduces n by a factor of two each time through, whereas the outer loop decreases n by one each time. Accordingly, there is no guarantee that n will be zero when the inner loop terminates — but such a guarantee is unnecessary. All that is necessary is to ensure that n has not increased during the loop. Because the only operation that the inner loop performs on n is to divide it by 2, that condition is easily met.

To prove that the inner loop terminates, we can add a second invariant to the inner loop: n != 0. We know that this invariant is true when we enter the inner loop for the first time because the condition of the outer loop ensures it. We also know that each time through the inner loop, n is even, because the condition of the inner loop ensures it. Therefore, when we divide n by 2, the result is exact; and dividing a nonzero value by 2 to yield an exact result cannot ever yield zero.

Using this inner invariant to prove that n is never zero in the inner loop helps us in two ways. First, it means that the inner loop must terminate. If it were possible for n to be zero, we might get in trouble; the loop might run forever with n being zero each time through. But if we start with an integer greater than zero, and we divide it by two enough times, we will eventually reach an odd value and the loop will stop.

The second way in which the inner invariant helps us is to ensure that when the loop terminates, n is still not zero, because zero is an even number. As a result, when we decrement n at the end of the outer loop, we know that the result cannot be negative.

Each of our loops decreases n while maintaining the invariant. The inner loop decreases it quickly, but in a way that might not cause it to reach zero. The outer loop does so more slowly, but in a way that guarantees that n will eventually become zero. As a result, we are still assured that the program will yield the right result, and we have good reason to believe that in many cases, the program will run more quickly than the original.

What I find remarkable about this program is that the invariant makes it unnecessary to answer what one might think is an obvious question: What is the value of r at each point in the code? We don't need to know the exact value of r; we need only to know that r has whatever value will ensure that our eventual result is r * xn. In other words, we care not about the value of r but about its properties. In effect, an invariant is an abstraction that allows us to ignore the exact value of a variable while still reasoning about the program.

Next week, I intend to talk about how invariants can help us test our programs, after which I shall apply invariants to a trickier problem than this one.

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.
 


Video