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!newsfeed2.dallas1.level3.net!news.level3.com!newsfeed-00.mathworks.com!nntp.TheWorld.com!not-for-mail
From: Robert A Duff <bobduff@shell01.TheWorld.com>
Newsgroups: comp.lang.ada
Subject: Re: Structured exception information
Date: Fri, 19 Jan 2007 14:57:58 -0500
Organization: The World Public Access UNIX, Brookline, MA
Message-ID: <wcchcumlrg9.fsf@shell01.TheWorld.com>
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>
 <ELudndXclMc6MzPYnZ2dnUVZ_umlnZ2d@megapath.net>
 <%xErh.228837$aJ.94458@attbi_s21>
 <uJqdnZHQg-zJ6S3YnZ2dnUVZ_sWdnZ2d@megapath.net>
 <n9nxrrwse2m5.19v4em7xkygda.dlg@40tude.net> <Kw8sh.230908$aJ.29262@attbi_s21>
NNTP-Posting-Host: shell01.theworld.com
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: pcls6.std.com 1169236678 1780 192.74.137.71 (19 Jan 2007 19:57:58
 GMT)
X-Complaints-To: abuse@TheWorld.com
NNTP-Posting-Date: Fri, 19 Jan 2007 19:57:58 +0000 (UTC)
User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix)
Cancel-Lock: sha1:i/vm/tXTUzB4zBMQG8rQ9gbNvvw=
Xref: g2news2.google.com comp.lang.ada:8343
Date: 2007-01-19T14:57:58-05:00
List-Id: <comp.lang.ada>

Jeffrey Carter <spam.jrcarter.not@spam.acm.not.org> writes:

> This is a good point. Ada's subtypes have always been a form of dynamic
> precondition.

And postcondition.  I.e. an invariant.

>... I've always thought it better to write
>
> Length : in Natural
>
> than
>
> Length : in Integer
>
> --#pre Length >= 0

Agreed.

> So it would be nice if this concept could be extended to essentially
> handle dynamic preconditions. Any suggestions how to apply this to, say
>
> (DS : in out Data_Structure; Index : in Positive)
>
> --#pre Index in 1 .. Size (DS);

Well I suppose one could come up with rules that make sense of:

(DS : in out Data_Structure; Index : in Positive range 1..Size(DS))

but that's a huge change to Ada.

- Bob