psc@lznv.ATT.COM (Paul S. R. Chisholm) (01/28/88)
< 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.
UH2@PSUVM.BITNET (Lee Sailer) (01/29/88)
In article <1273@lznv.ATT.COM>, psc@lznv.ATT.COM (Paul S. R. Chisholm) says: > >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 I agree. The semester I spent on Proving Correctness improved my programming skills tremendously, even though I don't ever actually "prove" my code. lee
csm@garnet.berkeley.edu (01/29/88)
In article <1958@svax.cs.cornell.edu> siegel@svax.cs.cornell.edu (Alexander Siegel) writes: >In article <1273@lznv.ATT.COM> psc@lznv.ATT.COM (Paul S. R. Chisholm) writes: >>In article <30176UH2@PSUVM>, UH2@PSUVM.BITNET (Lee Sailer) writes: >>>... >>> PROGRAM CORRECTNESS PROOFS: All the work on this seems to require the >>>... >>It's quite impossible to prove most software "correct", either because >>it's not correct (no smiley)... >>... >.... The biggest efforts are being made in automatic progarm verification... > In five years ... >-- It will take more than five years to prove the automatic program verifier software is "correct" (also no smiley). However, using "assertive" comments is a lot of help to you and to other savvy programmers who might want to muck around with your code. -- Brad Sherman P.S. If employers could imagine longer time spans than "until the next shareholders' meeting" they might understand that by giving programmers (sorry, Software Engineers) offices instead of cubicles, they will eventually INCREASE profits. P.P.S Has anyone seen a study of the effect on productivity of (gasp) increasing vacation time.