Article View: comp.ai
Article #8745Re: Reasons why you don't prove your programs are correct
From: Peter Desnoyers
Date: Sat, 13 Jan 1990 01:03
Date: Sat, 13 Jan 1990 01:03
20 lines
1485 bytes
1485 bytes
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
Technical Details
Message-ID:
<6171@internal.Apple.COM>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!apple!apple.com!desnoyerReferences:
<6158@internal.Apple.COM> <9237@medusa.cs.purdue.edu>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!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: <6171@internal.Apple.COM> Date: 13 Jan 90 01:03:58 GMT Sender: usenet@Apple.COM Organization: Apple Computer, Inc. Lines: 20 References: <6158@internal.Apple.COM> <9237@medusa.cs.purdue.edu>