Path: utzoo!attcan!uunet!snorkelwacker!bu.edu!bu-cs!xylogics!world!bzs
From: bzs@world.std.com (Barry Shein)
Newsgroups: comp.ai
Subject: Re: Re^2: Reasons why you don't prove your programs are correct
Message-ID: <1990Jan12.030424.1397@world.std.com>
Date: 12 Jan 90 03:04:24 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <548@tci.bell-atl.com>
Followup-To: comp.ai
Organization: The World @ Software Tool & Die
Lines: 28
In-Reply-To: kempf@tci.bell-atl.com's message of 11 Jan 90 15:23:12 GMT


>I should think that the idea would be silly on the face of it... after
>all, wouldn't it need to have a subroutine that could solve the
>halting problem?  Last time I looked, it was still considered
>impossible.  Maybe on the new Cray IV??*
>
>+C

The halting problem states (very roughly) "There exists at least one
program who's halting conditions cannot be determined".

People don't often write that program*, the fact that there was one
(or a few) theoretically possible counter-example would hardly be
sufficient to invalidate the concept of automatic program
verification.

Computer science education makes far too much of this interesting
observation and seems to leave people forever without hope that any
automatic examination of a loop can be fruitful (e.g. in a debugging
compiler.)

* People do write infinite loops frequently, but those are usually
easy to detect automatically with some inequality manipulations.
-- 
        -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!bzs