in reply to Re^2: Theorem proving and Unit testing
in thread Theorem proving and Unit testing

It does say something about the implementation of the algorithm. It doesn't actually say a darn thing about the algorithm itself.

Here's another way to look at it. You're trying to say "If the algorithm passes test X, then the implementation should pass test X." Absolutely true. However, you can throw every test like this that you can think of against a given implementation, but the implementation actually doesn't implement the algorithm! It just happens to pass all your tests.

You can still look at the proof of an algorithm, though, and glean a number of tests which will have the largest confidence increase per test. For example, if you threw hundreds of randomly-constructed trees at that test, you might gain a confidence of 90% in the algorithm for a cost of 300 tests. You can gain that same 90% confidence by looking at the edge cases of trees and constructing, say, 10 tests. So, each test in the second series is worth 30 tests from the first series.

For example, I would look at testing:

At that point, you can probably look at the tests and develop an inductive proof that says "I don't need to test linear six generations because linear three generations would break in the same way, if linear six generations would break." Most people intuitively develop tests like this, but most don't actually go through the effort of proving that their tests will work.

Another way to look at this is if you're testing something with 30 binary properties, you don't actually need to test all 2**30 possible situations. You only need to run the 32 basic tests (1 all off, 30 for turning each one on, 1 all on), then turning certain ones on together, based on the specification and a little knowledge of how the code works. Now, you and I would both love to have the 2**30 tests to make sure that unintended interactions don't creep in. But, I know I don't have the CPU time to run a billion+ tests. So, I don't have 100% confidence in my code, but I do have 99% confidence, based on the 32+ tests I ran. And, I can run those tests every time I make a tiny change. I might actually run the billion+ tests (or a random subset of a million tests) if I were building out to production and could let it run overnight, but that wouldn't be a standard part of my test suite.

------
We are the carpenters and bricklayers of the Information Age.

Then there are Damian modules.... *sigh* ... that's not about being less-lazy -- that's about being on some really good drugs -- you know, there is no spoon. - flyingmoose

I shouldn't have to say this, but any code, unless otherwise stated, is untested