Xref: utzoo comp.ai:5508 comp.arch:13145 comp.databases:4615 comp.edu:2901 comp.object:734
Path: utzoo!attcan!uunet!aplcen!haven!purdue!bls
From: bls@cs.purdue.EDU (Brian L. Stuart)
Newsgroups: comp.ai,comp.arch,comp.databases,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <9237@medusa.cs.purdue.edu>
Date: 12 Jan 90 21:32:05 GMT
References: <6158@internal.Apple.COM>
Reply-To: bls@cs.purdue.edu (Brian L. Stuart)
Followup-To: comp.ai
Organization: Department of Computer Science, Purdue University
Lines: 38

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