Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.ai
Subject: Re: Re^2: Reasons why you don't prove your programs are correct
Message-ID: <1244@oravax.UUCP>
Date: 12 Jan 90 20:51:55 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <548@tci.bell-atl.com>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 26

bzs@world.std.com (Barry Shein) writes:

>Yes, the flap in the early 80's was over automatic program
>verification. It seemed that DOD was considering putting $150M into
>this so the debate became quite bloody.

In this discussion, does the term "automatic program verification"
mean "FULLY automatic", that is, you just hand it the program and the
specification and it says "yes" or "no", or are we talking about
USER-GUIDED verification?

>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?

It depends on whether your specification language allows you to state
that the program halts, and it depends on whether your verifier is (in
the above sense) fully automatic.  If it does, and it is
(respectively) then there will be some programs that it gives an
incorrect answer for.  If the verifier is also allowed to answer "I
don't know", then it can always answer correctly but if so, must
sometimes answer "I don't know".
-- 
Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Sans Peur