Channels ▼

Andrew Koenig

Dr. Dobb's Bloggers

Sanity Checking By Extrapolation

August 27, 2014

Last week, I started discussing this code fragment, which purported to compute the sum of a sequence of floating-point numbers:

doublesum(double* begin, double* end)
{
      doubleresult = 0;
      double* p = begin;
      while(p != end) {
           result += *p;
           ++p;
      }
      returnresult;
}

I observed that by stepping manually through the code, it was easy to see that the code worked correctly if the sequence had no elements at all, or had one element; but that it was less obvious how to deal with the general case in which the sequence might have any number of elements.

It is tempting to dismiss this problem as trivial, and argue that one should simply be able to construct a bunch of test cases and be done with it. However, it may not be easy to determine what the correct results are from this function.

For example, consider a C++ implementation that is capable of recognizing that the variable result is used only within a loop. Such an implementation might decide to put result in a hardware register rather than storing it in memory. What if that hardware register has more precision than a normal double variable? In that case, this function might return a result that is more accurate than the test cases that a naïve test-case generator might produce. When you are inspecting test results, how can you distinguish between such an optimization and an outright bug?

Of course you might try test cases with a variety of values in the input, and verify that changing a single input value changes the result by approximately the same amount. However, in a case such as this one, in which there is not always guaranteed to be a single correct answer, it can often be useful to supplement your testing by trying to verify that the code is doing what you think it is doing.

Last week, I showed that the code works correctly when begin is equal to end or when begin+1 is equal to end. What if we generalize this notion by saying that begin+n is equal to end for various values of n? Then we have shown that the code works correctly for n=0 or n=1; our task is to remove that limitation.

We can approach this task in several ways. The most informal, which nevertheless is often surprisingly effective, is to verify that our code works for several values of n, and then wave our hands around and say something like: "Well, we know it works for n=0 and n=1, and we've also tested it for n=42. Nothing in the code depends on the specific value of n, so we have every reason to believe that it works for all n."

Described in this way, the mental process seems absurdly sloppy. Nevertheless, there is an important truth behind it: If the code works for n=0, and increasing the value of n doesn't do anything to break the code, then the code works for all n. We can make this argument slightly less informal by assuming that the code works for n=0 and n=1, but doesn't work for n=k. If there is more than one value of n for which the code fails, let's assume that k is the smallest such value. In other words, for all n such that 0<=n<k, the code works; but with n=k, it fails.

In order for this state of affairs to be possible, there must be something special about k. In particular, increasing the value of n by one doesn't break the code for any n<k-1, but when n=k-1, something about that particular value causes the code to break. In order for that to happen, the code has to contain some kind of knowledge, perhaps implicitly, about the value of k, and the location of that knowledge in the code ought to show up in a careful inspection.

Here is a still less informal way of describing this way of thinking:

Suppose that we know that our function works when begin+n is equal to end for some specific value of n. If the code truly does not depend on the value of n, then we ought to be able to use the fact that it works when begin+n is equal to end to prove that it also works when begin+n+1 is equal to end. In other words, we should be able to extrapolate from our knowledge of the code's correctness when begin+n is equal to end to other values of n. If we can do that, then we should be able to prove that the code works in all cases.

There are two important techniques that can help verify the correctness of programs of this sort. The first one is an induction proof, which many readers probably studied in high school or college and then promptly forgot. We shall discuss induction proofs next week. After that, we will finally be in a position to understand loop invariants, which we shall discuss the week after next.

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