Path: utzoo!attcan!uunet!ns-mx!ceres!zaphod.mps.ohio-state.edu!tut.cis.ohio-state.edu!pt.cs.cmu.edu!rochester!spot!mayer
From: mayer@rocksanne.uucp (Jim Mayer)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <287@spot.wbst128.xerox.com>
Date: 12 Jan 90 01:43:52 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu>
Sender: news@spot.wbst128.xerox.com
Reply-To: mayer.wbst128@xerox.com (Jim Mayer)
Organization: Xerox Corporation, Webster Research Center
Lines: 28

Several messages have argued that automatic program verification is
impossible because it would require a solution to the halting problem.
While I am not a believer in automatic program verification, I do
belive that the halting problem argument does not apply here.  In
particular, an automatic verifier is not required to return a result at
all... that is it can return yes/no/unknown (one can always return SOME
result by computing for a given amount of time then punting).

Some consequences of this are:

	(1) If it says "YES", the program matches its specification
	    (but who verifies the spec?... I always felt this was the
	    real killer for automatic verification schemes).
	
	(2) If it says "NO", the program does NOT match the spec.

	(3) If it says "UNKNOWN", the program may or may not match
	    the spec.  I seem to recall (no references... so reach
	    for your salt shaker) that some mechanism for helping
	    out the verifier was usually provided (even if it was
	    no more than an "assert" that was taken as axiomatic by
	    the verifier program).

-- Jim Mayer
--
                                        Xerox Webster Research Center
Phone: (716) 422-9407  FAX: x2126       800 Phillips Road, 0128-29E
Internet: mayer.wbst128@xerox.com       Webster, New York 14580