Path: utzoo!attcan!uunet!snorkelwacker!apple!agate!agate!hughes From: hughes@tempest.Berkeley.EDU (Eric Hughes) Newsgroups: comp.software-eng Subject: Some misperceptions about program proof Message-ID: Date: 19 Mar 90 17:57:08 GMT Sender: usenet@agate.berkeley.edu (USENET Administrator;;;;ZU44) Organization: ucb Lines: 101 It seems that there has been a lot of discussion about program proving without a general understanding of what the whole process involves. I do not claim that any individual misunderstands any individual point; rather I offer this as clarification to the end of a useful discussion. Here then, are four misperceptions that whose explication would be of benefit. Misperception 1: A program by itself is either correct or incorrect. In my previous posting where I supplied a proof sketch to the posted subroutine, I made this same point. Correctness applies to a program insofar as it has preconditions and postconditions attached to it. The issue here is one of semantics. A program, by itself, is just syntax (at least, mostly syntax). A statement of that the program (and here I mean subroutine, loop, statement, etc.) does is not contained as such within the statements of the program. A signifer of the intended semantics is often included in the name of the subroutine/variable/program, as sqrt(), to implement a square root function, or insert_node_with_rebalancing(). But the name cannot fully describe the semantics. The semantics, at best, are contained in the statement of the preconditions and postconditions. Misperception 2: The proof is developed after the code is written. This can, of course, be done. The method works best, however, if the proof is written at the same time as the code. Furthermore, it works best when the proof guides the construction of the code. It is often said "a program and its proof"; I have begun to think of "a proof and its program." As Gries says in _The Science of Programming_, "Programming is a goal- oriented activity." In other words, you should have the postcondition in mind before you start. What the idea is (and it works; I do it) is to state first what you want to do, and then to work backwards from the postcondition, changing it as you go, working back to the precondition all the time. This assumes you know what you want to do, of course, which is a much harder thing than most people imagine. One's mindset changes, as typified by the question "What do I do next?" changing to "How do I make this true?" Misperception 3: Writing a compiler which only compiles correct programs is impossible. This misperception requires both the preceding two. Such a compiler would require that statements be alternated with assertions and that all preconditions and postconditions be stated. Furthermore, it would require that all loop invariants be stated together with their bound functions and guards. It would also likely require the explicit assertion of intermediate steps in the proof. But I do think that such a compiler could be written. It would not be easy for any current language I know of, because none of them are simple and elegant enough, including C, or, possibly, especially C. In any case, only the program statements would be retained; there would be entirely new syntax for describing the assertions and predicates. As Hoare said: "I conclude that there are two ways of constructing a software design: One way is to make it so simple that there are _obviously_ no deficiences and the other way is to make it so complicated that there are no _obvious_ deficiencies." A further hurdle to such a compiler would be that it would itself have to be proved correct in order for it to have any credibility. This would require that for those sections of the code that are automatically generated, the proof, as well, should be automatically generated. This is, I suspect, the least of the hurdles. Misperception 4: Writing a program and proof takes forever. Forever is an awfully long time. :-) Currently, I admit, it does take a long time to write a correct program. A large part of that, though, is that common constructions must be thought about over and over again. There simply has not been enough practice in writing correct programs that the common, repeated features are well understood and embedded in language design. All the books on program correctness (that I know of) deal with writing correct algorithms, not with writing implementations of correct algorithms by writing correct programs. (This is, at least, basically true. Gries does have a small section about "Writing Programs in Other Languages", but it is not a treatise on how to write whole software packages which are correct.) As common constructions are identified and named, it will be much easier to think about program proofs, making it much faster to write correct software. Another hindrance is the lack of software tools. A first step would be a lint-like processor which takes a program whose proof is entirely within comments (meaning no alteration to existing compilers) and prints out a list of assertions which it cannot justify from the program text. Such a tool would not verify that a program was correct, but it would allow correct programs to be written. This tool would also be able to check that the pre/post-conditions of a subroutines definition match those used in its reference. Misperception 5. Program correctness will solve all your problems. Oops, that's a dead horse. :-) Eric Hughes hughes@ocf.berkeley.edu