Testing As Proof
in [Java Programming]
|
From: Alan Gutierrez on 29 Jul 2010 00:39 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. -- Alan Gutierrez - alan(a)blogometer.com - http://twitter.com/bigeasy
From: Lew on 29 Jul 2010 01:10 On 07/29/2010 12:39 AM, Alan Gutierrez wrote: > 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. Tests don't give a formal proof. They just show that certain cases produce expected results. An algorithm is either proven or not proven. You can use a proven algorithm, and use published material to verify that the algorithm is valid. You can look up the proof that the algorithm is valid. That leaves the question of whether your implementation actually expresses that proven algorithm. You can and should establish that by salting the code with 'assert' statements to prove that the implementation adheres to the algorithmic invariants. -- Lew
From: Tom Anderson on 29 Jul 2010 07:06 On Thu, 29 Jul 2010, Lew wrote: > On 07/29/2010 12:39 AM, Alan Gutierrez wrote: > >> 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. > > Tests don't give a formal proof. They just show that certain cases produce > expected results. True. I think what Alan is getting at is more 'testing as argument' than 'testing as proof'. For instance, if i was going to write such tests for an implementation of quicksort, i might write tests like: // i have an isTrivialCase to weed out arrays that don't need sorting isTrivialCaseReturnsTrueForLengthZeroArray isTrivialCaseReturnsTrueForLengthOneArray isTrivialCaseReturnsFalseForLongerArrays // test 2, 3, 100 // and i'm going to deal with two-element arrays specially to save some headache isTwosortCaseReturnsTrueForLengthTwoArray isTwosortCaseReturnsFalseForLengthThreeArray twosortSortsALengthTwoArray // maybe try a few examples // i use median-of-three partitioning to choose the pivot choosePivotFindsAnElementOfTheArray choosePivotFindsAnElementOfTheArrayWithAtLeastOneSmallerElement choosePivotFindsAnElementOfTheArrayWithAtLeastOneLargerElement // i partition around the pivot partitionLeavesTheArrayPartitionedAroundThePivot // perhaps the crucial test // might have several variations on the above, for pathological cases and so on partitionAppliedToASubarrayDoesNotAffectTheRestOfTheArray // we need some kind of test of the fact that the two halves left after // partitioning are always smaller than the starting array // final test quicksortLeavesTheArraySorted At each step, i test one of the invariants which are the building blocks of the proof of correctness. The tests aren't a proof, but they help illustrate the proof - and check that my implementation conforms to the it. tom -- Scheme is simple and elegant *if you're a computer*.
From: Lew on 29 Jul 2010 09:06 Tom Anderson wrote: > At each step, i test one of the invariants which are the building blocks > of the proof of correctness. The tests aren't a proof, but they help > illustrate the proof - and check that my implementation conforms to the it. Tests are good things. There are three legs on the stool of implementation correctness here: assertions, conditional/exception blocks and unit tests. -- Lew
From: Joshua Cranmer on 29 Jul 2010 18:58
On 07/29/2010 12:39 AM, Alan Gutierrez wrote: > 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. To quote Dijkstra, "Testing cannot prove the absence of bugs, they can only prove the presence of bugs." Instead, the simplest thing to do is to write enough tests such that all execution paths can be covered. Basically, find a few examples of common cases and use every corner case you can think of--null parameters, 0-length arrays, etc. If you're making a datatype, you probably need to have your tests ensure that the internal structure never gets out of sync. In addition, you'd need to ensure that the tree looks like how it's supposed to look after each operation. You can also (if the license is appropriate) reuse others' examples as test cases. -- Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald E. Knuth |