From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,699cc914522aa7c4
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news3.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!wns14feed!worldnet.att.net!attbi_s71.POSTED!53ab2750!not-for-mail
From: Jeffrey Carter <spam.jrcarter.not@spam.acm.not.org>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US;
 rv:1.8.0.1) Gecko/20060130 SeaMonkey/1.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Structured exception information
References: <eog0g5$2bn$1@cernne03.cern.ch>
 <wcczm8k8aj5.fsf@shell01.TheWorld.com> <1168885771.30643.20.camel@localhost>
 <th0jaznlzs72$.uirljzpoeskd.dlg@40tude.net>
 <1168891576.30643.39.camel@localhost>
 <5NKdnTv2UZfVZTbYnZ2dnUVZ_vipnZ2d@megapath.net>
 <38z8yk9z1uxn$.1r6qpevwu2i7c.dlg@40tude.net>
 <Wf8rh.1144532$084.1006940@attbi_s22>
 <s0prxwrhxfj1.1r5zzccgpzy2.dlg@40tude.net>
 <SbWdnW-QRpBqyzDYnZ2dnUVZ_qKknZ2d@megapath.net>
 <1lpy2h06scx34.1i2k4dlbg0nfy.dlg@40tude.net>
In-Reply-To: <1lpy2h06scx34.1i2k4dlbg0nfy.dlg@40tude.net>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <x2urh.309672$FQ1.158886@attbi_s71>
NNTP-Posting-Host: 12.201.97.213
X-Complaints-To: abuse@mchsi.com
X-Trace: attbi_s71 1169059101 12.201.97.213 (Wed, 17 Jan 2007 18:38:21 GMT)
NNTP-Posting-Date: Wed, 17 Jan 2007 18:38:21 GMT
Organization: AT&T ASP.att.net
Date: Wed, 17 Jan 2007 18:38:21 GMT
Xref: g2news2.google.com comp.lang.ada:8229
Date: 2007-01-17T18:38:21+00:00
List-Id: <comp.lang.ada>

Dmitry A. Kazakov wrote:
> 
> I doubt that others could or should be called preconditions.

> The point is that violated preconditions are non-states and cannot be
> handled at all. Provided, that one understands precondition as a method of
> proving program correctness. Otherwise, it is something else.

It's clear that you're locked into the concept of a precondition as part 
of correctness proofs. In that context, yes, you statically prove that 
preconditions are met, and do not need to dynamically test them. This is 
the case with SPARK, for example.

In general, though, preconditions are a useful tool for documenting SW, 
especially SW that will be used by people other than the developer. It's 
a useful way of communicating to the client what he needs to ensure in 
order for the SW to function normally (this condition must be true), and 
the consequences of failing to do so (this exception is raised).

Ideally, you'd use the same syntax for both uses of preconditions. Then 
SW that's written for general use could be used in SW that does 
correctness proofs without changes; without correctness proofs the 
compiler would automatically generate the tests, and with proofs, the 
tests would not be generated.

In retrospect, the syntax I thought up on the spur of the moment in my 
previous post is not very good, since, for a precondition P, what you 
write is not P. That would not be very useful for correctness proofs.