Path: utzoo!utgpu!news-server.csri.toronto.edu!mailrus!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <1424@oravax.UUCP>
Date: 16 Mar 90 00:36:25 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM> <18190@duke.cs.duke.edu>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 20

In article <18190@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes:
>In article <2480006@hpcuhc.HP.COM> runyan@hpcuhc.HP.COM (Mark Runyan) writes:
>>As an alternative, someone could post a non-trivial program and ask the
>>program provers to prove it either correct or incorrect...
>Um, it doesn't really work that way,
[...]
>What one needs to do in a proven program is construct the program with
>provability in mind.
[...]

Sure, sure, and if somebody posts something I think I have a chance of
getting through Ariel, I may modify it to make it easier to verify.  If
I do this, my intent will be to remain faithful to the original
program.  I'm willing to take the chance that many people may scream
that I changed the program beyond recognition.
-- 
------
Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Sans Peur