Article View: comp.ai
Article #1168Re: Reasons why you don't prove your programs are correct
From: Flame Bait
Date: Mon, 15 Jan 1990 19:17
Date: Mon, 15 Jan 1990 19:17
17 lines
1507 bytes
1507 bytes
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
Technical Details
Message-ID:
<16665@joshua.athertn.Atherton.COM>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!snorkelwacker!apple!oliveb!pyramid!athertn!joshuaReferences:
<16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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