Testing As Proof

[Stefan Ram]

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.

 

[Stefan Ram]

I even read once that some people prefer »while( x != 21 )«
for such loops so as to get a more precise postcondition »x == 20«.

Sorry, I meant »while( x != 20 )«.

I should have /proof/read my post ...

 

[jesbox]

  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.

 

[jesbox]

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?

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.