Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!umich!samsung!caesar.cs.montana.edu!ogicse!ucsd!ucsdhub!hp-sdd!ncr-sd!ncrcae!hubcap!cooper
From: cooper@nunki.crd.ge.com (Clark Cooper)
Newsgroups: comp.parallel
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <7669@hubcap.clemson.edu>
Date: 16 Jan 90 18:01:42 GMT
Sender: fpst@hubcap.clemson.edu
Lines: 32
Approved: parallel@hubcap.clemson.edu


	You can prove your program correct with respect to a formal
specification, but not with respect to an ill-defined and fuzzy world
with which the desired system must deal. The source of most profound
bugs is a conceptual model that fails to fit the real world. Proving
a program correct with respect to a specification with a faulty model
is not only wasted effort, but leads to a very false sense of security.

	In my view, specification writing is just programming at a higher
level. If the language of the specification is truly formal and complete,
then (in theory) no further programming is necessary and a suitable compiler
could deliver the program.

	In that case, proving the program correct is like proving that
my current compiler transforms my source program into an equivalent
program in machine language. The people who worked on the compiler
should take reasonable measures to assure that this happens for all
valid source programs (and that invalid source programs raise exceptions).
If a proof is possible and reasonable for this, then it is a GOOD THING.
In any case, it is not the duty of every programmer that uses the
compiler.

	Thus, unless the application domain is purely formal (like program
compilation), program correctness proofs are no more than additional
evidence that our systems are reliable. This makes them no more valuable
than program testing techniques, which are anathema to the program
correctness proof school.
--
===================================================================
Clark Cooper	 GE Corporate R&D	  cooper@nunki.crd.ge.com
(518) 387-5887	 P.O. Box 8 / K-1 4C31	  coopercc@crdgw1.ge.com
		 Schenectady, NY  12301	  ...!uunet!crdgw1!coopercc