hughes@tempest.Berkeley.EDU (Eric Hughes) (03/20/90)
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
skrbec@cell.mot.COM (Brad Skrbec) (03/20/90)
hughes@tempest.Berkeley.EDU (Eric Hughes) writes: ><...> >Misperception 1: A program by itself is either correct or incorrect. ><...> I agree that the preconditions and postconditions are what determine whether a program or subroutine is correct or incorrect for the problem domain. However, if the results of a subroutine don't apply to the pre- and postconditions, is the subroutine incorrect, or is it being incorrectly used? If I use a Sine subroutine where I need a Cosine result, the Sine routine isn't incorrect, only inapplicable. >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." The proof development can and often should accompany the development of the code, but it probably shouldn't guide the goal of the code. If the proof contains misconceptions, then they are automatically carried over to the code, and now you have not one source of false information, but two. We use an independent testing group, and they are kept apart from the code designers and writers, so that they have an unbiased view of what the code should do. If the coders start to work too closely with the testers, they tend toward similar false assumptions, and errors go undetected until too late. ><...> >Misperception 3: Writing a compiler which only compiles correct >programs is impossible. This may be a false perception, but I doubt that you'll disprove it any time soon. Again, this all depends on what you consider "correct". Semantically, I think that current technology won't allow this (We have tried AI verification programs that take a week to do what one could do manually in a couple of hours). Syntactically, I believe this is already done by strongly typed compilers such as Ada and some others.
hughes@locusts.Berkeley.EDU (Eric Hughes) (03/21/90)
In article <1751@teal4.UUCP> skrbec@cell.mot.COM (Brad Skrbec) writes: >hughes@tempest.Berkeley.EDU (Eric Hughes) writes: >However, if the results of a subroutine don't apply to the >pre- and postconditions, is the subroutine incorrect, or is it being >incorrectly used? If I use a Sine subroutine where I need a Cosine >result, the Sine routine isn't incorrect, only inapplicable. It is incorrect, because no proof can be exhibited (since none exists) which asserts that the answer is a cosine if the calculated value is a sine. For example, the following program is incorrect, because one cannot demonstrate that y is in fact the cosine of x after execution of the program. This does not mean that the code statements don't do anything, simply that they have not been demonstrated (with a proof or proof sketch) that they do in fact do something. You can, however, compile the program (with a regular C compiler) and exhibit (with a program execution) behavior. { true } y = sin( x ) { y == cos( x ) } >The proof development can and often should accompany the development >of the code, but it probably shouldn't guide the goal of the code. I disagree. It is my own coding experience, that if you do let the proof guide the code, it is much easier to construct programs that work, let alone be correct. More below. >If the proof contains misconceptions, then they are automatically >carried over to the code, and now you have not one source of false >information, but two. If the proof contains a logic flaw, then this does in fact happen; I cannot deny this, and in a hand checked proof system, this will always be a problem, that one can only be sure about the correctness of the program to the extent that you are sure about your abilities at logical manipulation. However, in a machine checked system (assuming, for the sake of argument, that the machine checker is correct and bug-free) the only possible misconceptions are those in the preconditions and postconditions, exactly those predicates which are supplied by the programmer. You will get a correct program, but you may not do what you think it should do or want it to do. This is what Dijkstra refers to as "the pleasantness problem." However, the virtue of good design, per Hoare, whom I quoted earlier, is that a complicated specification should be simple enough that there are "_obviously_ no deficiences." Here is a small example to illustrate the pleasantness problem. {{ true }} switch( a ) { case 1 : if ( doremi( x ) ) break ; case 2 : } {{ true }} The postcondition is true, so the program is correct, because every program that halts satisfies the true postcondition. But does this program do anything useful? No. > If the coders start >to work too closely with the testers, they tend toward similar false >assumptions, and errors go undetected until too late. No argument here. Making sure that others think a formal spec means the same thing to them as it means to you is definitely a good idea. This is one part of a solution to the pleasantness problem. >>Misperception 3: Writing a compiler which only compiles correct >>programs is impossible. >This may be a false perception, but I doubt that you'll disprove >it any time soon. Again, this all depends on what you consider >"correct". I alluded to this earlier. One of the very hardest things to prove a compiler correct is to write down just exactly what it really does. One could, for example, construct the "strongest postcondition", from a true precondition, of, say GCC, but I doubt that it would be readable or understandable. (The strongest postcondition is technical term, which means loosely in this context "a formal specification of what the program really does.") I would love to see it as a goal of the computer science community to be able to state in both simple and elegant language the right kinds of formal specifications for complex programs such as compilers, operating systems, and editors. (Such language may be large, but that by itself doesn't prevent it from being simple.) > Semantically, I think that current technology won't >allow this (We have tried AI verification programs that take >a week to do what one could do manually in a couple of hours). When you mention AI in this context, it makes me wonder what type of verification system you were using. An AI system that tries to come up with, say, loop invariants is bound to fail at its goal, because the general problem is equivalent to the halting problem. (That is, by the way, the reason for a bound function; one _must_ prove that every loop halts.) What such a compiler really needs is a way to verify that the invariants supplied by the programmer are valid. What we need is a proof checker, not a proof constructor. Now I don't know what kind of verification system you were using, so this argument may not apply to you. It is, however, of vital importance in using correctness as a useful tool. In the proof I posted earlier, one of the invariants was something like "n' = s' + n * b^u." Only people can come up with those kinds of invariants effectively. The problem with automatic generation is fundamental. True sentences are recursively enumerable, but not decidable. In other words, if you have a postcondition to a program, and that postcondition is provable from the program and precondition, then you eventually can automatically generate a proof of that postcondition. But if that postcondition is not provable, then you may never find a disproof, i.e. the constructor may never halt. >Syntactically, I believe this is already done by strongly typed >compilers such as Ada and some others. Strong typing (or, more correctly, robust handling of the interpretation and representation of concrete and abstract types) is one necessary element of a correct compiler. But it does a fairly small amount of the real work of proving a program correct, even if in practice strong typing is extremely useful. Abstractly, strong typing verifies that all the terms of the program and proof are well-formed, that is, that the arguments are of the proper domain with respect to the functions. However, it is also a manifestation _only_ of well-formedness, but since one can only speak of correctness with respect to well-formed formulas, it is a necessary aspect. Eric Hughes hughes@ocf.berkeley.edu