gudeman@cs.arizona.edu (David Gudeman) (04/20/91)
In article <12297@dog.ee.lbl.gov> Chris Torek writes: ]>In article <1726@optima.cs.arizona.edu> gudeman@cs.arizona.edu ]>(David Gudeman) writes: ]>>Finally, consider the relationship of the proof to the real world ... ]>>you will have to deal with the philosophy of mathematical models. ] ](This goes well off the beam of comp.lang.misc. You must also deal ]with the question of objective reality, and whether, if it exists at ]all, it can be perceived. eek. I wasn't going that far out. ]Likewise---and perhaps this is what David Gudeman is talking about---we ]can use mathematical models of computer behaviour quite effectively, ]but we should keep in mind that they are only models. Exactly one of the points I wanted to make. Models are by their very nature abstractions, and abstractions by their very nature leave out some details. You have to remember that your theorems are only true if you stay within the limits of the abstraction. ]My own position on this is that both methods should be used in ]moderation, and in proportion to the importance of the problem. That is my position on the question of whether formal program verification is "useful" -- it certainly is. But I wanted to get at something about the nature of program verification, where I think people have mistaken ideas. Part of the mistake comes from the term "proof of correctness". What does such a proof really prove (assuming that the proof is correct in the first place)? First, I will point out what it does _not_ prove: it does not prove that the program actually behaves in the way that it is expected to. That is the point that I think a lot of people are missing. So what does it prove? Given a program P1 in programming language L1 with formal semantics M1; and a formal specification P2 in specification language L2, with formal semantics M2; a formal proof of correctness of L1 is just a proof that the meaning of P1 under the semantics M1 is the same as the meaning of P2 under the semantics M2 (where "is the same as" has some formal meaning that varies according to the proof technique). Now, what does such a proof tell us about the real-world question of whether the program P1 behaves as we want it to? Nothing. It tells us that P1 behaves as P2 says it will. How do we know that P2 specifies that P1 will behave as we want it to? We don't. We _can_ say that if our confidence in P2 was greater than our confidence in P1, then (assuming we have complete confidence in the proof itself) the result of the proof is that our confidence in P1 is now the same as our confidence in P2. But the problem is that there is no a priori reason that our confidence in P2 should have been higher than P1. But let us assume that such a reason exists. Possibly P2 is much shorter than P1 because it is in a higher-level language or because the paradigm of L2 is more suited to the problem than is the paradigm of L1. But if that is the case, then why not just write the program in L2 in the first place? One could answer by saying that L2 is too inefficient for a programming language. Fine. Then let's not pretend that our "proof of correctness" is a way to prove a program correct; it is just a way to prove that an efficiency hack preserves the semantics of the program (where the "efficiency hack" is to recode the inefficient program P2 in the more efficient language L1). Many people claim that we have more confidence in P2 than P1 just because L2 is a "mathematical" language. I don't think there is any basis for such a distinction unless P1 is designed to be a low-level implementaton language. In such a case I say that P2 should be the programming language and recoding in P1, again, is just an efficiency hack. Just because L1 uses the paradigm of imperative procedures and L2 uses the paradigm of predicate logic, is no reason to say that P2 is more reliable. I think people who argue that predicate logic is a "better" notation than imperative procedures are deceived in thinking that imperative procedures inherently have the messy, low-level semantic nature they have in many real programming languages. But is isn't fair to compare C to formal predicate calculus. A better comparison is Lisp to Prolog. Both are general-purpose programming languages at about the same "semantic level", and they are equally good (or bad) for formal purposes. So why do I still think formal verification is a good idea? Given two different programs P1 and P2 to solve the same problem, it seems reasonable to assume that the probability that the programs both have an identical error is small compared to the probability that each might have an arbitrary error. Given a proof that the two programs are "the same", we know that any errors that either one has, it has in common with the other one. We have already said that such a probability is smaller than the probability of individual errors, so we have increased our confidence. You could formalize this in probability theory to find out how much confidence we need in the proof and how much lower the probability of mutual errors has to be for the level of confidence to increase. Any takers? You can informally decrease the probability that two different program will have identical errors by writing them in different programming languages. You can further decrease the probability by using two languages with radically different paradigms (which is the usual verification technique). Even better would be to have different programmers do the work in different languages with radically different paradigms. Of course once this is all done, you still don't know if the thing runs until you test it. You can still run into compiler bugs. So the answer to my original question: "What do you know after a formal proof that you did not know before the proof?" is "You know that the program implements the formal specification. You don't formally 'know' anything more about the program's real behavior than you did before." -- David Gudeman gudeman@cs.arizona.edu noao!arizona!gudeman
cok@islsun.Kodak.COM (David Cok) (04/20/91)
In article <2202@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes: > >So the answer to my original question: "What do you know after a >formal proof that you did not know before the proof?" is "You know >that the program implements the formal specification. You don't >formally 'know' anything more about the program's real behavior than >you did before." >-- You know the same thing after a formal proof that you do after running a test suite: if there were errors (failed proof, failed tests) then you have some bugs to fix; if there were no errors (proof checked, all tests passed) then you know that the program behavior agrees with (a) the behavior specified by the specification, or (b) the behavior represented by the test suite. Both of the latter are subsets of the full behavior, and neither one necessarily represents what you really want. (Yes, I've seen tests that ran into bugs and no one had properly checked the result of the test.) If only as a way of finding more bugs sooner and if only as a way of "verifying" that an efficiency hack computes the same result as an "obviously correct" but inefficient alternate program, a program verifier would be useful. David R. Cok Eastman Kodak Complany -- Imaging Science Lab cok@Kodak.COM
gudeman@cs.arizona.edu (David Gudeman) (04/20/91)
Oops. The sentence above is true enough, but it isn't what I intended to say. I meant to say that "You don't know anything more about whether the program's behavior is correct by the real-world specification." ]You know the same thing after a formal proof that you do after running a test ]suite: if there were errors (failed proof, failed tests) then you have some ]bugs to fix; if there were no errors (proof checked, all tests passed) then ]you know that the program behavior agrees with (a) the behavior specified by ]the specification, or (b) the behavior represented by the test suite. You have missed the entire point of the article: the behavior specified by the specification may bear no relation to the correct behavior for the program. Thus knowing about the formally specified behavior does not tell you about the correctness of the behavior. I'm talking about what you _know_ in the sense of mathematical certainty. It has been said that mathematics gets its certainty by not actually saying what it is talking about. A proof of corrrectness is only a "proof" if it is applied to a formal specification with no relation to the real world. Once the specification is applied to the real world, you lose certainty. The reason I bring this up is because some people on this newsgroup have been talking like formal verification is some sort of magic that actually proves that a program does what it is supposed to do, and that testing is an unreliable hack. Quite the contrary, testing is now and always will be essential. Formal verification is now and always will be a special technique that is only useful in certain kinds of applications, and always in conjunction with testing. No, testing does not give mathematical certainty. There is no such thing in the real world. I can write a program that satisfies the following specification of a sort program: Forall 0 < i < N . Output[i-1] <= Output[i] and prove it correct even though it does not work correctly for any real world example. Since the specification is incorrect, the proof tells nothing about how the program is related to the real world. All a proof of correctness does is relate one formal specification to another. It doesn't tell you that either one is correct. Disclaimer: Nothing in the above should be taken as an assertion that program verification has no value. It is only intended to clarify exactly what is (and is not) mathematically proven by a formal proof of correctness. Furthermore, the author loves dogs and small children and is not a lunatic who just likes to drop bombs in comp.lang.misc and watch the fireworks. Really. No, I mean it. I didn't even want to talk about program verification, I was provoked. OK, I could have ignored it, but... never mind. -- David Gudeman gudeman@cs.arizona.edu noao!arizona!gudeman
cok@islsun.Kodak.COM (David Cok) (04/21/91)
In article <2216@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes: > ... > >In article <???> cok@Kodak.COM (David Cok) writes: >]You know the same thing after a formal proof that you do after running a test >]suite: if there were errors (failed proof, failed tests) then you have some >]bugs to fix; if there were no errors (proof checked, all tests passed) then >]you know that the program behavior agrees with (a) the behavior specified by >]the specification, or (b) the behavior represented by the test suite. > >You have missed the entire point of the article: the behavior >specified by the specification may bear no relation to the correct >behavior for the program. Thus knowing about the formally specified >behavior does not tell you about the correctness of the behavior. I'm >talking about what you _know_ in the sense of mathematical certainty. > I didn't miss your point. You stopped quoting my post too soon: Both of the latter are subsets of the full behavior, and neither one necessarily represents what you really want. I meant -- are at best subsets of the full behavior. In fact I mostly agree with you: formal proofs do not give certainty because specs may not match the desired behavior. However, I still think that a verifer could (the technology is nowhere near providing this yet) be a valuable complement to testing (for which we have some useful technology now), something people might run on programs as they might run lint on a C program. It does not give certainty but it can raise confidence. It only relates two formal specs, but if one is simpler and, to the human reader, more clearly correct, then there is good reason for some increased confidence. And if the verifier points out an error, you are one bug ahead. The confidence is misplaced if the spec is incomplete or inaccurate, but that is also true for an incomplete test suite. >Formal verification is now and >always will be a special technique that is only useful in certain >kinds of applications, and always in conjunction with testing. And everything useful was already invented by 1900. :-) > >Disclaimer: Nothing in the above should be taken as an assertion that >program verification has no value. It is only intended to clarify >exactly what is (and is not) mathematically proven by a formal proof >of correctness. OK. On those points we agree. David R. Cok Eastman Kodak Company -- Imaging Science Lab cok@Kodak.COM
stephen@estragon.uchicago.edu (Stephen P Spackman) (05/03/91)
One interesting thing that Hendrik Boom mentioned to me from using his (total correctness) verifier was that he typically found more bugs in his SPECIFICATIONS than he did in his PROGRAMMES (for example, a sort routine failed to typecheck because the specification failed to handle duplicates correctly). Now, you might think that this is a strike against verification (at very least it suggests that writing short, abstract, mathematical specs may NOT be easier than coding up a decent algorithm, and that checking such a spec by eye may not be so straightforward), but in fact it's precisely the spec (albeit in a less formal form) that is going to be the interface contract between the routine and the outside world. The effect of the verifier, then, is to make you look VERY hard at the properties of your interfaces. And my experience has been that interfaces are the things that HAVE to be right - the code you can always discard. ---------------------------------------------------------------------- stephen p spackman Center for Information and Language Studies systems analyst University of Chicago ----------------------------------------------------------------------