Xref: utzoo comp.ai:5553 comp.edu:2915 comp.object:746
Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!snorkelwacker!apple!oliveb!pyramid!athertn!joshua
From: joshua@athertn.Atherton.COM (Flame Bait)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <16665@joshua.athertn.Atherton.COM>
Date: 15 Jan 90 19:17:35 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is>
Reply-To: joshua@Atherton.COM (Flame Bait)
Organization: Atherton Technology, Sunnyvale, CA
Lines: 17

In article <1455@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes:
>From article <16479@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait):
>> 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.

I would group you into my second group.  The assertions are checked
both statically and dynamically.  By the way, I agree that this is
good programming practice and I do it myself, but it is not "proving
a program correct".  I consider it part of defence in depth.

Joshua Levy                          joshua@atherton.com  home:(415)968-3718
                        {decwrl|sun|hpda}!athertn!joshua  work:(408)734-9822