Path: utzoo!attcan!uunet!tut.cis.ohio-state.edu!ucbvax!pasteur!agate!agate!hughes
From: hughes@locusts.Berkeley.EDU (Eric Hughes)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <HUGHES.90Mar20090717@locusts.Berkeley.EDU>
Date: 20 Mar 90 17:07:17 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM>
	<18190@duke.cs.duke.edu> <1424@oravax.UUCP>
	<19988@joshua.athertn.Atherton.COM>
Sender: usenet@agate.berkeley.edu (USENET Administrator;;;;ZU44)
Organization: ucb
Lines: 22
In-reply-to: joshua@athertn.Atherton.COM's message of 19 Mar 90 17:23:35 GMT

In article <19988@joshua.athertn.Atherton.COM> joshua@athertn.Atherton.COM (Flame Bait) writes:
   I would like to see any of the following four programs verified:
   GnuTar, GCC, GAWK, or G++.

OK, I accept.  I pick GAWK.  If you will stipulate that the program
halts on all inputs, then my proof is finished, because I have
picked the true postcondition.

Now if you write a formal spec of the behavior of GAWK, I will
have another, and different, task at hand.  But I think it will
take you longer to write a formal spec than for me to write a 
proof.

Maxim:  A program is only correct with respect to a precondition
and postcondition.

Furthermore, utilities like GAWK, which are meant to be general
purpose, public utilities, should always have the true precondition,
since the should not hang up on arbitrary input.

Eric Hughes
hughes@ocf.berkeley.edu