# 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.

### More Insights

 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.