Xref: utzoo comp.ai:5535 comp.edu:2911 comp.object:741
Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!mcsun!hafro!isgate!krafla!snorri
From: snorri@rhi.hi.is (Snorri Agnarsson)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1455@krafla.rhi.hi.is>
Date: 13 Jan 90 18:04:33 GMT
References: <16479@joshua.athertn.Atherton.COM>
Organization: University of Iceland
Lines: 23

From article <16479@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait):
> "Proving your programs are correct" seems to mean different things
> to different people:
> 
> One group thinks it means that your program does exactly what your
> spec says it should.
> 
> Another group thinks it means that you can put complex assertions
> in your code and have the checker makes sure that these assertions
> are always true.

And a third group (including myself) thinks it means you can put
assertions in your code and in your interfaces and carefully
try to see to it that those assertions are true at each time point.

This is not very hard at all for good programmers (in fact I would
claim that those who cannot do this cannot be good programmers),
and has the extra advantage that the assertions act as documentation
for future maintenance.
-- 
Snorri Agnarsson		|  Internet:	snorri@rhi.hi.is
Taeknigardur, Dunhaga 5		|  UUCP:	..!mcvax!hafro!rhi!snorri
IS-107 Reykjavik, ICELAND