Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!elroy.jpl.nasa.gov!hacgate!ashtate!atsun!dwiggins From: dwiggins@atsun.a-t.com (Don Dwiggins) Newsgroups: comp.theory Subject: Re: Reasons why you don't prove your programs are correct Message-ID: Date: 16 Jan 90 00:14:11 GMT References: <1891@uwm.edu> <1788@bruce.OZ> Sender: dwiggins@ashtate.UUCP Organization: Ashton-Tate, Inc. Lines: 15 In-reply-to: cjs@bruce.OZ's message of 14 Jan 90 07:08:28 GMT I've read a few of the messages in this thread, and it triggered a question in my mind. Generally, in a mathematical theory, one doesn't construct proofs starting with the axioms if a reasonable set of useful theorems is available. In fact, when working in a new theory, the first order of business is to "build some tools" in the form of generally applicable theorems. Is there any work along those lines going on in the program verification field (e.g. something of the form "if the code of a loop matches pattern X, then it will satisfy invariants of the form Y"). Such theorems could be built into an automatic verifier and might cut the search space considerably. -- Don Dwiggins "Solvitur Ambulando" Ashton-Tate, Inc. dwiggins@ashtate.a-t.com