Xref: utzoo comp.ai:5504 comp.arch:13138 comp.databases:4610 comp.edu:2898 comp.object:730
Path: utzoo!attcan!uunet!aplcen!samsung!brutus.cs.uiuc.edu!apple!apple.com!desnoyer
From: desnoyer@apple.com (Peter Desnoyers)
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: <6158@internal.Apple.COM>
Date: 12 Jan 90 18:48:44 GMT
Sender: usenet@Apple.COM
Organization: Apple Computer, Inc.
Lines: 22
References:<25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu>

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