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_s21.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>
 <x2urh.309672$FQ1.158886@attbi_s71>
 <vqdjmgk3akqr.1mkjxu3kj9k6.dlg@40tude.net>
In-Reply-To: <vqdjmgk3akqr.1mkjxu3kj9k6.dlg@40tude.net>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <e%Orh.229467$aJ.120266@attbi_s21>
NNTP-Posting-Host: 12.201.97.213
X-Complaints-To: abuse@mchsi.com
X-Trace: attbi_s21 1169144906 12.201.97.213 (Thu, 18 Jan 2007 18:28:26 GMT)
NNTP-Posting-Date: Thu, 18 Jan 2007 18:28:26 GMT
Organization: AT&T ASP.att.net
Date: Thu, 18 Jan 2007 18:28:26 GMT
Xref: g2news2.google.com comp.lang.ada:8271
Date: 2007-01-18T18:28:26+00:00
List-Id: <comp.lang.ada>

Dmitry A. Kazakov wrote:
> 
> To me this is a contract: x/y yields a mathematically correct result or
> else it propagates an exception when, for example, y=0. I.e. it is legal to
> write 1/0 and the precondition is True.
> 
> If the precondition were y/=0, then 1/0 would be illegal and nothing could
> be done about it.

I think what many of us (Brukardt and I, at least) are calling (dynamic) 
preconditions, you're calling exceptional states. I can see that, but 
these are undesirable exceptional states that the developer cannot 
ensure will not happen (consider reusable components). Neither the 
client nor the service provider want an exceptional state. The idea is, 
in the contract, to assist the caller in knowing what the exceptional 
states are and how to avoid them. That's similar to a precondition in 
the correctness-proof sense: something which prevents the program from 
functioning. In the case of correctness proofs, the program doesn't 
function at all; in the case of dynamic preconditions or exceptional 
states, the program doesn't function as desired.