Xref: utzoo comp.ai:5562 comp.edu:2916 comp.object:747 Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uwm.edu!csd4.csd.uwm.edu!markh From: markh@csd4.csd.uwm.edu (Mark William Hopkins) Newsgroups: comp.ai,comp.edu,comp.object Subject: Re: Reasons why you don't prove your programs are correct Message-ID: <1906@uwm.edu> Date: 16 Jan 90 02:42:48 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <16479@joshua.athertn.Atherton.COM> <16664@joshua.athertn.Atherton.COM> Sender: news@uwm.edu Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins) Followup-To: comp.ai Organization: University of Wisconsin-Milwaukee Lines: 50 In article <16664@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes: >My last example points out a current problem with proving program correct. >They must only use libraries which have been proven correct, must run on >an operating system which has been proven correct, and must use hardware >which is proven correct. All of this is impossible right now. A program verification would look like this: "This program is guaranteed to operate consistently with the specifications outlined in the adjoining document on a CORRECT compiler and operating system. Any apparent bugs found are solely attributable to one or more of the utilities used to form the environment of the program." (the document could be short for all we care, just so long as it specifies all the details relevant to the user). Just because a program may be operating in a faulty environment does not mean that verification cannot be done with it. Verification is ALWAYS done conditionally on the assumption that everything being used to support the software is correct. In this context, it's only purpose is to eliminate the sources of possible bugs (it can't be the software, so it must be the firmware or even the hardware(!)). And by verification I DO mean mathematical verification. Of course, you will do some actual run-time testing whose purpose is to aid in the discovery of the mathematical properties of the software. That way you can significantly automate much of the discovery process. That's how I've been able to detect bugs in system utilities, such as a local Pascal compiler, an assembler, and even circuitry quite a few times. Never managed to find fault with a chip yet though... It's funny, because a student once came to me with a 200-300 line Pascal program, trying to figure out what was wrong with it. I looked at it in detail, and simply by inspection could tell her that there was nothing wrong with it. Some software you can tell will work simply by looking at it -- that easy they are to prove correct. So ... it was the compiler. The mentality was so ingrained in people (which was actually picked up from the course) that programs are creatures to be analysed behaviorally, instead of mathematical constructs, that it simply never occurred to this person that she might be able to prove that the fault did not lie with her program. >I often think of this branch of the "software proof" camp in the same way. >As long as they stick to mathmatical programs which do not have input, >output, or any other real life constraints, they can create interesting >examples. The irony...