Article View: comp.ai
Article #8730Re: Reasons why you don't prove your programs are correct
From: victor yodaiken
Date: Fri, 12 Jan 1990 13:41
Date: Fri, 12 Jan 1990 13:41
12 lines
1418 bytes
1418 bytes
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) explains that program verification is impossible because it would violate the halting problem theorem of Turing. This is true in a very narrow and uninteresting sense. The problem of program verification is for programs on actual computing devices, not programs on turing machines. If someone produced a system which would test to see whether or not a program could compute its intended result within the estimated life-span of the Solar system on a computing device 100trillion times the speed of a CRAY, the system would , by most accounts be a solution to the program verification problem. There is nothing in unsolvability theory that precludes such a system. Obviously, a far more modest system would be of great practical use and theoretical interest.
Technical Details
Message-ID:
<8421@dime.cs.umass.edu>Path:
arc1-ca.pugleaf.net!utzoo!attcan!uunet!aplcen!samsung!think!husc6!m2c!umvlsi!dime!yodaikenReferences:
<25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!attcan!uunet!aplcen!samsung!think!husc6!m2c!umvlsi!dime!yodaiken From: yodaiken@freal.cs.umass.edu (victor yodaiken) Newsgroups: comp.ai Subject: Re: Reasons why you don't prove your programs are correct Message-ID: <8421@dime.cs.umass.edu> Date: 12 Jan 90 13:41:42 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu> Sender: news@dime.cs.umass.edu Reply-To: yodaiken@freal.cs.umass.edu (victor yodaiken) Organization: University of Massachusetts, Amherst Lines: 12