steve@hubcap.clemson.edu ("Steve" Stevenson) (01/06/90)
I'm trying to discover the real reason why people do not prove their programs
are correct. I would like to collect those reasons --- even those snappy
one liners that we all use as excuses.
Please forward your comments ( short flames ok) to me by E-mail. I'll post
the replies if there is sufficient interest. Thanks.
--
Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu
Department of Computer Science, (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906
--
Send compilers articles to compilers@esegue.segue.boston.ma.us
{spdcc | ima | lotus}!esegue. Meta-mail to compilers-request@esegue.
Please send responses to the author of the message, not the poster.mmm@cup.portal.com (Mark Robert Thorson) (01/08/90)
There was an excellent article about 10 years ago in CACM on this. I believe the title was "The Social Process and Proofs of Program Correctness". This article marked the death of program verification; feelings which had echoed in the halls of academia and industry for more than a decade were expressed in a clear form in print, and from that point on the "conventional wisdom" was that program verification was a dead-end for research. In retrospect, it's hard hard to see why this wasn't obvious from the very beginning.
snorri@rhi.hi.is (Snorri Agnarsson) (01/10/90)
From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson): > There was an excellent article about 10 years ago in CACM on this. > I believe the title was "The Social Process and Proofs of Program > Correctness". This article marked the death of program verification; > feelings which had echoed in the halls of academia and industry > for more than a decade were expressed in a clear form in print, > and from that point on the "conventional wisdom" was that program > verification was a dead-end for research. In retrospect, it's hard > hard to see why this wasn't obvious from the very beginning. I have not read this article and I must confess it is not obvious at all to me that verification is dead. Perhaps automatic program verification is dead, that would not surprise me, but I still believe all programmers should prove their programs while they write them, even if the proofs are only for their own consumption. I believe this is especially important for large projects with many procedures. To be able to maintain a large program you need to know the following for each procedure: 1) Under what circumstances is it allowed to call the procedure? (those are the procedures preconditions) 2) Assuming it is allowed to call the procedure, what will it's effect be? (postconditions) It is astonishing how often large projects are done without documenting the above information. -- Snorri Agnarsson | Internet: snorri@rhi.hi.is Taeknigardur, Dunhaga 5 | UUCP: ..!mcvax!hafro!rhi!snorri IS-107 Reykjavik, ICELAND
frazier@oahu.cs.ucla.edu (Greg Frazier) (01/11/90)
In article <1449@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes:
+From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson):
[delete]
+> verification was a dead-end for research. In retrospect, it's hard
+> hard to see why this wasn't obvious from the very beginning.
+
+I have not read this article and I must confess it is not obvious
+at all to me that verification is dead. Perhaps automatic program
[delete]
+To be able to maintain a large program you need to know the following
+for each procedure:
+
+ 1) Under what circumstances is it allowed to call the
+ procedure? (those are the procedures preconditions)
+
+ 2) Assuming it is allowed to call the procedure, what
+ will it's effect be? (postconditions)
Different versions of verification going on here. THe
first poster meant proof when he said verification. The second
poster confidence in correctness when he said verify. Being
confident a program will work is a far cry from proving that
it will work.
Greg Frazier
...................................................................
"They thought to use and shame me but I win out by nature, because a true
freak cannot be made. A true freak must be born." - Geek Love
Greg Frazier frazier@CS.UCLA.EDU !{ucbvax,rutgers}!ucla-cs!frazierbzs@world.std.com (Barry Shein) (01/11/90)
Yes, the flap in the early 80's was over automatic program
verification. It seemed that DOD was considering putting $150M into
this so the debate became quite bloody.
The automatic program verification proponents lost. Perlis gave a good
talk on why, it went something like:
In order to determine if a program is correct another
program would have to build some sort of model to
compare it against. This would be, presumably, from
some sort of abstract specification of what the program
is supposed to do.
If the verifier could build that model it could translate
the specifications into the program. So why bother to
write a program to be verified at all? Why not just write
a high-level specifications compiler (why indeed, no one
knows how, but verification was being passed off as something
palpable to work on, like just a big math proof generator.)
There were some corrollary observations, like what exactly would such
a verifier be able to tell us? Presumably either "yes this program is
correct" or "no, this program is not correct". That's of questionable
value. If it could tell us useful detail about why it was correct or
not then, again, we are led to the conclusion that it could write the
program.
Also some amusing concerns about verifying the verifier.
--
-Barry Shein
Software Tool & Die, Purveyors to the Trade | bzs@world.std.com
1330 Beacon St, Brookline, MA 02146, (617) 739-0202 | {xylogics,uunet}world!bzsbls@cs.purdue.EDU (Brian L. Stuart) (01/12/90)
In article <1990Jan11.015531.20996@world.std.com> bzs@world.std.com (Barry Shein) writes: > >The automatic program verification proponents lost. Perlis gave a good >talk on why, it went something like: > His arguments are significant and important practical considerations, but there is a more fundamental theoretical issue here. 1) No program can be verfied to be correct unless it is verified that it produces the correct output. 2) In verifying the correctness of the output, one verifies the existence of the output. 3) Assume that a program exists that can verify the existence of output. Now create a pre-processor that takes as input a program and produces as output the same program except that it halts after every output. (The construction of such a program is left as a excercize for the reader :-) Now the combination of this pre-processor with the assumed verifier is a program which will detect whether or not a program halts. Hopefully, everyone recognizes that this is impossible according to the halting theorem, so our assumption of a program that can verify the existence of output must be false and by 1) and 2) we cannot have a program that verifies the correctness of programs in general. The upshot of this is that for any language or programming methodology which is verifiable, there will be some programs that can be expressed on a Turing Machine which cannot be expressed in this language or methodology. When you ask for verifibility, you ask to sacrifice Turing-compatability. Be careful what you ask for, you may get it. Brian L. Stuart Department of Computer Science Purdue University
snorri@rhi.hi.is (Snorri Agnarsson) (01/12/90)
From article <30689@shemp.CS.UCLA.EDU>, by frazier@oahu.cs.ucla.edu (Greg Frazier): > In article <1449@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes: > +From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson): > [delete] > +> verification was a dead-end for research. In retrospect, it's hard > +> hard to see why this wasn't obvious from the very beginning. > +... > +To be able to maintain a large program you need to know the following > +for each procedure: > + > + 1) Under what circumstances is it allowed to call the > + procedure? (those are the procedures preconditions) > + > + 2) Assuming it is allowed to call the procedure, what > + will it's effect be? (postconditions) > > Different versions of verification going on here. THe > first poster meant proof when he said verification. The second > poster confidence in correctness when he said verify. Being > confident a program will work is a far cry from proving that > it will work. No, I meant PROOF. Not automatic proof, just the usual garden variety kind of proof. Of course proofs can be wrong, so all they can do is increase our confidence. While I don't believe automatic verification is ever going to be directly useful I do believe research on those lines is useful because it increases our understanding on how to program. You can use a lot of the same techniques manually, and it is not necessary to do them formally to increase your confidence in your programs. I think every programmer should know about loop invariants, pre- and postconditions, and their use. Every programmer should know the difference between weak and strong correctness, and should know how to prove weak correctness and termination independently. Every programmer should know how to prove weak correctness of mutually recursive procedures, and why the method works. Every programmer should be able to state and prove data invariants for their data types. I find it very hard to understand why some people claim we should not use these techniques just because they do not give us 100% confidence in our programs. Similar reasoning should tell us to abandon testing, and should tell mathematicians to stop writing theorems. -- Snorri Agnarsson | Internet: snorri@rhi.hi.is Taeknigardur, Dunhaga 5 | UUCP: ..!mcvax!hafro!rhi!snorri IS-107 Reykjavik, ICELAND
desnoyer@apple.com (Peter Desnoyers) (01/13/90)
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) writes: >[flawed proof that program verification is impossible.] Try this one instead. Given a program V that will verify whether or not program P run on input I will produce output O. We can transform P by deleting all output statements and having it output a single value O' before it halts. [ie. transform P() to P'(),print(O') where P'() is P() with all print statements deleted.] V(P',I,O') will then determine whether or not the output of P'(I) is O', which is equivalent to determining whether P(I) halts. Therefore V cannot exist. However, this result isn't as useful as it seems. First, there are important classes of programs where V is computable, even if it is not computable on all programs. Second, program verification often means proving whether or not P (the program) is equivalent to P' (the specification), which is a different problem entirely. (although probably not computable in the general case.) Peter Desnoyers Apple ATG (408) 974-4469
bls@cs.purdue.EDU (Brian L. Stuart) (01/13/90)
In article <6158@internal.Apple.COM> desnoyer@apple.com (Peter Desnoyers) writes: >In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) >writes: >>[flawed proof that program verification is impossible.] > >Try this one instead. Given a program V that will verify whether or not >program P run on input I will produce output O. We can transform P by >deleting all output statements and having it output a single value O' >before it halts. [ie. transform P() to P'(),print(O') where P'() is P() >with all print statements deleted.] V(P',I,O') will then determine whether >or not the output of P'(I) is O', which is equivalent to determining >whether P(I) halts. > >Therefore V cannot exist. This appears to me to also be a valid proof from the case of verifiers with the specified form. >However, this result isn't as useful as it >seems. First, there are important classes of programs where V is >computable, even if it is not computable on all programs. Second, program >verification often means proving whether or not P (the program) is >equivalent to P' (the specification), which is a different problem >entirely. (although probably not computable in the general case.) Not entirely. Anytime a program is verified, the correctness of its output is verified either implicitly or explicitly. That is why I was careful to phrase my proof in a form that did not say that verification took place by verifying output, but instead took the general case of a verifier. I said that a by-product of the verification process was the verification of output and used that. Why do you feel that my proof was flawed? I know its not as rigorous as it could be, but I don't thing its wrong. Brian L. Stuart Department of Computer Science Purdue University
desnoyer@apple.com (Peter Desnoyers) (01/13/90)
In article <9237@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) writes: > Why do you feel that my proof was flawed? I know its not as rigorous > as it could be, but I don't thing its wrong. Your proof was of the form "take program P and transform it into program P'. Verifying that P produces any output is the equivalent of solving the Halting Problem for P'". In other words, you showed that you could use a program that decides the Halting Problem to decide the verification problem. That isn't a particularly interesting result (since halting problem deciders can compute just about anything :-) - what we need to prove that the verifier cannot exist is to show that you can use the verifier to solve the halting problem. Don't feel bad - I think I made the identical mistake on the net a year or two ago. Peter Desnoyers Apple ATG (408) 974-4469