Lower Bound (via testing) vs. Upper Bound (via proof) for Correctness

296 views Asked by At

Chris Smith's article "What to know before debating type systems" contains the following unexplained statement:

Testing: establishes upper bounds on correctness
Proof: establishes lower bounds on correctness

The context is comparing the benefits of proving program correctness (e.g. with a type-checker) vs. testing program behaviour (e.g. with TDD in a dynamically typed language).

What are the "upper" and "lower" bounds on correctness in this context?

1

There are 1 answers

4
templatetypedef On BEST ANSWER

Imagine you have a program and you know basically nothing about how it works. It's supposed to have a bunch of properties (say, X, Y, and Z), but you're not really sure whether it does. What can you do to figure this out?

One option would be to try to use a program verification tool to formally prove that the program has properties X, Y, and Z. Unfortunately, in general, it's impossible to automatically verify that a program has any interesting properties (thanks, halting problem!), so even if the program actually has these properties, you may never be certain of this. However, if the program checker reports that the program does indeed have property X, you can say that at the very least, the program does X. In that sense, you're "lower-bounding" the correctness of the program: it definitely has property X, and possibly has some more properties.

Another option would be to run the program and see what happens. Suppose during testing you find a test case that causes the program to misbehave and, therefore, definitely not have property Z. Your test cases didn't expose any other errors, though. In that case, because you saw the program misbehave, you know for certain that it doesn't have property Z. Therefore, you've "upper-bounded" how correct the program is - it definitely doesn't have property Z, but you can't rule anything else out.

If you put the two of these together, you've got a proof that your program has property X and you have direct evidence that it doesn't have property Z. You don't know whether it has property Y or not, since that wasn't settled either way.

Hope this helps!