Testing As Proof
in [Java Programming]
|
From: Jim Janney on 12 Aug 2010 18:17 Alan Gutierrez <alan(a)blogometer.com> 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 */ x++; /* 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
From: jesbox on 13 Aug 2010 16:12 On Aug 13, 1:32 am, r...(a)zedat.fu-berlin.de (Stefan Ram) wrote: > Jim Janney <jjan...(a)shell.xmission.com> writes: > >while (x < 20) > >(...) > >/* postcondition: x >= 20 (from the condition of the while) */ > > I even read once that some people prefer »while( x != 21 )« > for such loops so as to get a more precise postcondition »x == 20«. > > From the point of view of »defensive programming« OTOH, »x < > 20« can avoid an endless loop (in case of bugs) better than > »x != 21«. > > Even in mathematics, proofs do not have to be »formal«. > They need to convey that an assertion is true beyond any > reasonable doubt to a sufficiently educated reader. Even in mathematics, formal proofs are sometimes proven wrong. In formal proofs on software, you prove that the code have implemented all the bugs of the specification.
From: jesbox on 13 Aug 2010 16:22
On Aug 2, 12:52 pm, Martin Gregorie <mar...(a)address-in-sig.invalid> wrote: > On Sun, 01 Aug 2010 23:08:05 +0100, Tom Anderson wrote: > > > This all sounds a bit mental to me. If this alleged designer is going to > > design to this level of detail, why don't they just write the code? > > The level I'm advocating is pretty much what you see in a good Javadoc or > a C standard library manpage. There's a good argument to be made that if > you don't document to that level before coding starts, then its pretty > much hit or miss whether the resulting code does what its intended to do > if the coding is done by somebody else. > > OK, it might stand a chance of doing its job if the designer wrote it, > but what are the chances of somebody else using it correctly without a > fair amount of coaching and hand-holding from the designer? > > The project I mentioned with the use-case system docs was like that: for > some packages running Javadocs showed absolutely nothing but the class > names and method interfaces - and the method names weren't particularly > meaningful. The result was that the Javadocs were meaningless for > determining how and when to use the classes - we had to prize example > code and argument descriptions out of the author before we could even > think about using them. You may think that's acceptable but I don't. > > Read the source? We didn't have it and couldn't get it. Besides, I expect > to use library objects without needing to see implementation detail. > Isn't that the while point of OO? > > -- > martin@ | Martin Gregorie > gregorie. | Essex, UK > org | I think all agree that documentation at the level of good javadoc or manpage is necessary. Some details takes very long time to figure out unless you build the code. The coder may be responsible for amending the documentation. Alternatively ask the designer to add the special cases to the design specification. |