Path: utzoo!utgpu!water!watmath!clyde!cbosgd!ihnp4!homxb!mtuxo!mtune!lzaz!lznv!psc
From: psc@lznv.ATT.COM (Paul S. R. Chisholm)
Newsgroups: comp.software-eng
Subject: correctness proofs (was Re: Complexity Measures)
Message-ID: <1273@lznv.ATT.COM>
Date: 27 Jan 88 22:25:22 GMT
References: <5874@sol.ARPA> <30176UH2@PSUVM>
Organization: AT&T
Lines: 33

< If you lined all the news readers up end-to-end, they'd be easier to shoot. >

In article <30176UH2@PSUVM>, UH2@PSUVM.BITNET (Lee Sailer) writes:
>...
> PROGRAM CORRECTNESS PROOFS:  All the work on this seems to require the
> addition of "assertions" to the code, that is, logical statements of
> all the assumptions that must hold before, after, and even during the
> execution of a piece of program.  (See Gries, the Science of Programming)

Um, sort of, but the other way 'round would be closer to the truth.

It's quite impossible to prove most software "correct", either because
it's not correct (no smiley), or the structure of the program doesn't
resemble the structure of the definition of "correct".  Not long after
playing with correctness proofs, folks such as Dijkstra and Gries found
that it was far easier to write the correctness proof and add the code
than vice versa.  Even so, the proof of a trivial code segment is
longer than the code, and the length of proofs grow much faster than
the code they can prove.  Gries' THE SCIENCE OF PROGRAMMING is an
excellent introduction to this subject.

In my personal experience, it's impractically difficult to "prove" any
non-trivial program correct.  On the other hand, the skills you need
for correctness proofs are very useful.  My programming environment
(writing UNIX applications in C) can't "understand" proofs and compile
time assertions, but it lets me add run time assertions.  I've done
this often, and found them a great aid in testing and debugging code.
The assertions I add are the same ones I used to develop the
code/proof.

-Paul S. R. Chisholm, {ihnp4,cbosgd,allegra,rutgers}!mtune!lznv!psc
AT&T Mail !psrchisholm, Internet psc@lznv.att.com
I'm not speaking for my employer, I'm just speaking my mind.