Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!ucbvax!decwrl!megatest!djones
From: djones@megatest.UUCP (Dave Jones)
Newsgroups: comp.software-eng
Subject: comments and correctness proofs ( Re: comments on comments )
Message-ID: <1859@goofy.megatest.UUCP>
Date: 13 Feb 89 22:21:46 GMT
References: <20233@agate.BERKELEY.EDU>
Organization: Megatest Corporation, San Jose, Ca
Lines: 62

From article <20233@agate.BERKELEY.EDU>, by hughes@math.Berkeley.EDU (eric hughes):
[...]
> 
>>					       If you do that, and
>>if the code is well structured, documenting an algorithm is usually
>>(but not always) unnecessary. Usually it is obvious how the algorithm
>>will go about the process of reestablishing a broken invariant.
> 
> I always document an algorithm, not matter how silly.  This has
> helped me avoid what I term "typo bugs," things I meant to do
> but forgot.
> 

Go ahead and write all the comments you want while you are developing
the code, to help you avoid those "typo bugs".  But my personal
preference is that you remove the comments of those "silly" algorithms
before you release the software into the great beyond.

>>		  If the algorithm is not tricky, the WHAT
>>will make the HOW clear enough.   
> 
> Yes, a good statement of the preconditions and postconditions to a
> function can eliminate most procedural comments.

Now you're talking!
 
> Now I would like some engineering tools with which I could check my
> correctness proofs, but since none exist (to my knowledge), I have
> found that conscientious commenting is acceptable.
> 

This is off the subject, but it's something I have been thinking about
a little, so allow me to ramble on for a bit, (or hit 'q').

Take the following for what it's worth, which may not be too much...

Seems to me there's a chicken and egg problem with computer aided
correctness proofs.

The universe of discourse about computer programs which computer programs
may get involved in concerns state and computable values. That's not too
profound, when one considers that a computer is basicly a memory
with an ALU.  But the universe of discourse of the proofs is couched in
terms of the problem -- the thing the program is modeling.

So one has a choice: write the invariants in terms of the computer
model, in which case you have tacitly agreed that the model is correct --
or write the invariants in terms of the problem, and somehow "teach"
the computer about those terms, in which case you tacitly agreee on
a model.  Hmmm...

And there's another problem: The assertions often have universal 
quantifiers and such that can not reasonably be calculated at runtime.

One can perhaps program around some of this by programming a basic
understanding of mathematical induction into the machine.  But when you 
start to attempt to do proofs about all possible histories of events and
such, things seem to get a little sticky.

On the other hand.  Sometimes I think *I* do correctness proofs.
So if one computer (like me) can do it, seems like another (like my
sun 3/60) should be able to do it.  Or maybe I'm just fooling myself.