Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uwm.edu!ogicse!decwrl!megatest!djones
From: djones@megatest.UUCP (Dave Jones)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <12326@goofy.megatest.UUCP>
Date: 15 Mar 90 01:53:14 GMT
Organization: Megatest Corporation, San Jose, Ca
Lines: 45


   [ I suppose that you program-provers, once you have proved you program,
     are going to prove that the proof is correct, yes? No? ]


Anecdote 1:

I often think about "invariant relations" and such when I'm programming, but
only once in the eleven years that I've been doing software engineering full
time have I written out a formal proof of a piece of production code. (Stop me
if you've heard this one.) The thing was made-to-order for a formal proof.
It was a tricky hash-table algorithm. It was so tricky, that I figured I
better prove it, so I did. A fellow worker had checked over my proof with me,
verifying that it was correct. A couple of months later a bug manifested
itself. No, it wasn't due to a typo in the coding -- and not a compiler-bug,
either. The proof contained a mistake corresponding to a mistake in the code.

Anecdote 2:

I did my master's thesis on an arcane bit of topology called "Dehn's Lemma".
(It concerns itself with necessary criteria in order that a loop be knotted
within a three or higher dimensional manifold.) Herr Dehn proved it in 1917
in _Annalen Mathematica_. It got rave reviews.  I may not have all these
dates exactly right, but I think it was sometime around 1929 when somebody
finally noticed that the proof had a whopping whole in it. In 1935, a fellow
discovered that the proof could be patched up and saved if a certain other
proposition was true. In 1957, a third man proved the second proposition, and
everybody was happy again. In 1978, I undertook to put it all together, but I
found a flaw in the proof of the second proposition!  After a few weeks of
sixteen-hours-a-day head-scratching, I was able to replace the faulty section
with a completely different, and much shorter, argument. Again, _das lemma_
appeared to be truly proved. The others had published their stuff in big math
journals, but I just wanted out of school so I could buy some food, so I never
submitted mine to a journal. Of course, my advisor checked it carefully, as
supposedly did the jury, but I guess there is some possibility that I too
overlooked something. It is a very knotty bit of business, that.

Now consider that both of those faulty proofs underwent much closer scrutiny
than my little program-proof of anecdote-1 did -- years of scrutiny --
more than ANY program-proof is ever likely to undergo, yet each was incorrect.

The point is, if you think that doing a formal proof is a good way to budget
your system test time, by all means go ahead. Just don't think it proves
anything conclusively. You better run lots of carefully selected test-cases
too.