Path: utzoo!attcan!uunet!husc6!rutgers!njin!princeton!phoenix!pucc!EGNILGES From: EGNILGES@pucc.Princeton.EDU (Ed Nilges) Newsgroups: comp.software-eng Subject: Re: Soft-Eng digest V5n23 Message-ID: <5835@pucc.Princeton.EDU> Date: 7 Aug 88 22:41:28 GMT References: <8808071435.AA05123@mitre.arpa> Reply-To: EGNILGES@pucc.Princeton.EDU Organization: Princeton University, NJ Lines: 102 Disclaimer: Author bears full responsibility for contents of this article In article <8808071435.AA05123@mitre.arpa>, soft-eng@MITRE.ARPA (Alok Nigam) writes: >Soft-Eng Digest Sun, 7 Aug 88 V: Issue 23 > >Today's Topics: > Proving software correct > >Date: Wed, 03 Aug 88 17:29:15 PDT >From: PAAAAAR%CALSTATE.BITNET >Subject: Proving software correct > > >>Assertions are only >>impossible to write when the software has not been designed in >>a structured and modular fashion. >>[definition of and examples of 'assert' in C] > >The poster confuses the 'assert' function of C's and the >"Invariant Assertions" I was writing about. >"Assert" functions should be used on any large project >to instrument the code. >Perhaps I should have been less cryptic... >I was not talking about any function or tool. >I ment the work done prior to C by Floyd, Hoare, Knuth, >Manna, Dijkstra and others, which still appears in elementary Comp Sci >Texts. These all present programs that are PROVEd to work using the >"invariant assertions" that where invented by Floyd way back in the 50's. No, there is a difference between invariant assertions and the assert() function (of course!). I am suggesting that we start using asserts in real code as a way of proving (but not PROVING) our software correct. I also feel that English-language arguments have a role in proving (but not PROVING) our software correct. > >>My assertions do not PROVE my software correct... > The people mentioned above have assertions that do! That's wonderful, Dick! But my concern in the real world is not PROVING software correct. It is proving software correct. The difference in case is meant to point up the intractability of the problem. Let me see if I can explain it better. I (or any competent programmer) can write a perfect Game of Life or even a perfect compiler for a toy language and PROVE it correct. Here, mathematics is tracking mathematics and, as such, perfection is attainable. I cannot write a PROVABLE battle management system or even a PROVABLE payroll program. This is because here, mathematics is trying to track something OUTSIDE of its realm. The problem is similar to that faced by Post and Turing in PROVING that Turing machines, or Post's system, captured our intuitive notion of computability. It is impossible in a formal sense, for you cannot formally map the mathematical onto the intuitive. However, and this is important, I can prove my payroll program correct (I don't know about battle management because, you see, I won't work on such projects). Not PROVE...prove. How? By using the techniques of program correctness proving, scaled-down and humbled so they work in the real world. I envision more and more formal techniques being used as software evolves! But I don't foresee a day when all software shall be PROVED correct. Another thing to keep in mind is that the viewpoint of as program as a static thing which is PROVED correct has produced a lot of maintenance nightmares, late hours, and plain old heartbreak. A program is more fruitfully viewed as a set or collection of programs evolving over time. Any applicable model of correctness proving must allow for maintenance of the correctness proof such that transforms which preserve correctness are encouraged and those that do not are dis- couraged, and the proof is updated along with the program. >>...any more than the designers >>of the Golden Gate Bridge (reference 2) could PROVE mathematically that >>the GG Bridge would stay up and be beautiful to boot. >Did they make drawings? > (using perspective & descriptive geometry) >Did they prove that the the bridge was long enough? > (using geometry, trigonometry, etc) >Did they calculate stresses and strains? > (using elementary mechanics/applied math) >Those engineers that I used to know used Math to PROVE that >the thing SHOULD work and then added a safety factor in case they >had left something out. >They also expected one or two bugs to turn up when the job was done... > But they didn't PROVE it, did they? >>I don't feel that it is possible to PROVE software correct. >Ed provides evidence of my key point... > REAL PROGRAMMERS FAIL TO PROVE THE CORRECTNESS OF THEIR PROGRAMS. Real programmers eat quiche! >I hope that somewhere in/on the networks someone is ready to disprove this... > I hope so to! But it shall be a long and winding road. The best advice is given by Robert L. Baber's The Spine of Software. Programmers today should learn these techniques so that they stand ready to use them when they are introduced.