Re: Testing As Proof

Alan Gutierrez <alan@xxxxxxxxxxxxxx> writes:

I'm working on implementing a B+tree and I'd like to be a little more
rigorous with testing than I have in the past. What I'd like to do is
write tests that prove the validity of the algorithm.

The algorithm works, mind you, but I don't feel like I can prove it. I
want than a bug stomping test suite. I want tests that capture the
reasoning behind the algorithm. Ideally I could point you to these
tests and you could see a proof. You could find fault in the reasoning
or else gain confidence in the implementation.

Nuts for me that I never got past geometry in high-school. I'll need
to weave a study of this sort of testing practice in with a study of
proofs. I need to learn how one might reasonably convince oneself of
something without deceiving oneself, which is a human tendency.

I'm getting good at identifying fallacies as a discussion survival
tool for more the raucous forms. I've used the resources on the
Internet that help you identify fallacies. I'm not yet confident in my
ability to draw new conclusions, only to spot misdirection. I imagine
there might be similar resources that help a person structure their
own arguments, rather than simply poke holes in the fallacious
arguments of others.

Does this make sense to you? It may sound as if I'm asking for
something too basic, but there must be other programmers who learned
the trade but then later wanted to circle back and learn the
formalities. It seems like someone must have taken the testing as
proof approach already.

It's possible to reason formally about code. This typically involves
pre- and post-conditions, things that are known to be true before the
execution of a piece of code and things that can be derived from the
code and its preconditions. A simple, probably not very good example
would be:

int x;
/* no precondition */
x = 10;
/* postcondition: x == 10 */

/* precondition: x == 10 */
while (x < 20) {
/* precondition: x < 20 */
/* postcondition: x <= 20 */

/* postcondition: x >= 20 (from the condition of the while) */

It gets more complicated than this, but I hope you get the general
idea. In principle it's possible, but usually not easy, to prove the
correctness of entire classes or even whole programs this way. As Lew
has already pointed out, this kind of reasoning converts fairly
directly into assert statements embedded in the code.

BUT -- and this is a big but -- this is not unit testing, because it
depends on a line-by-line knowledge of the code and the assertions
have to be embedded directly in the code. All that unit testing can
do is to call the publically accessible methods of a class and check
the results. And normally you *don't* want a unit test to care how a
method works inside, only that it behaves in the required manner.

Sorry for the late response, I'm catching up after a vacation.

Jim Janney