Xref: utzoo comp.ai:5505 comp.arch:13139 comp.databases:4611 comp.edu:2899 comp.object:731
Path: utzoo!attcan!uunet!mcsun!hafro!isgate!krafla!snorri
From: snorri@rhi.hi.is (Snorri Agnarsson)
Newsgroups: comp.ai,comp.arch,comp.databases,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1454@krafla.rhi.hi.is>
Date: 12 Jan 90 15:43:34 GMT
References: <30689@shemp.CS.UCLA.EDU>
Organization: University of Iceland
Lines: 51

From article <30689@shemp.CS.UCLA.EDU>, by frazier@oahu.cs.ucla.edu (Greg Frazier):
> In article <1449@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes:
> +From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson):
> [delete]
> +> verification was a dead-end for research.  In retrospect, it's hard
> +> hard to see why this wasn't obvious from the very beginning.
> +...
> +To be able to maintain a large program you need to know the following
> +for each procedure:
> +
> +	1)	Under what circumstances is it allowed to call the
> +		procedure? (those are the procedures preconditions)
> +
> +	2)	Assuming it is allowed to call the procedure, what
> +		will it's effect be?  (postconditions)
> 
> Different versions of verification going on here.  THe
> first poster meant proof when he said verification.  The second
> poster confidence in correctness when he said verify.  Being
> confident a program will work is a far cry from proving that
> it will work.

No, I meant PROOF.  Not automatic proof, just the usual garden
variety kind of proof.
Of course proofs can be wrong, so all they can do is increase
our confidence.
While I don't believe automatic verification is ever going to
be directly useful I do believe research on those lines is
useful because it increases our understanding on how to
program.
You can use a lot of the same techniques manually, and it
is not necessary to do them formally to increase your
confidence in your programs.
I think every programmer should know about loop invariants,
pre- and postconditions, and their use.
Every programmer should know the difference between weak
and strong correctness, and should know how to prove
weak correctness and termination independently.
Every programmer should know how to prove weak correctness
of mutually recursive procedures, and why the method works.
Every programmer should be able to state and prove data
invariants for their data types.
I find it very hard to understand why some people claim
we should not use these techniques just because they do
not give us 100% confidence in our programs.
Similar reasoning should tell us to abandon testing,
and should tell mathematicians to stop writing theorems.
-- 
Snorri Agnarsson		|  Internet:	snorri@rhi.hi.is
Taeknigardur, Dunhaga 5		|  UUCP:	..!mcvax!hafro!rhi!snorri
IS-107 Reykjavik, ICELAND