Xref: utzoo comp.ai:5463 comp.arch:13090 comp.databases:4583 comp.edu:2878 comp.object:712
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!brutus.cs.uiuc.edu!apple!mips!bridge2!jarthur!uci-ics!ucla-cs!frazier
From: frazier@oahu.cs.ucla.edu (Greg Frazier)
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: <30689@shemp.CS.UCLA.EDU>
Date: 10 Jan 90 20:07:09 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is>
Sender: news@CS.UCLA.EDU
Reply-To: frazier@cs.ucla.edu (Greg Frazier)
Organization: UCLA Computer Science Department
Lines: 30

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.
+
+I have not read this article and I must confess it is not obvious
+at all to me that verification is dead.  Perhaps automatic program
[delete]
+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.

Greg Frazier
...................................................................
"They thought to use and shame me but I win out by nature, because a true
freak cannot be made.  A true freak must be born." - Geek Love

Greg Frazier	frazier@CS.UCLA.EDU	!{ucbvax,rutgers}!ucla-cs!frazier