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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.stack.nl!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Shouldn't there be a paragraph like 7.3.2(5/3) in 3.2.4?
Date: Mon, 12 May 2014 17:26:28 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <lkrhqk$een$1@loke.gir.dk>
References: <87bnv3nomb.fsf@adaheads.sparre-andersen.dk>
 <dd27f835-8295-4cb2-aa28-2ff3f351b0e0@googlegroups.com>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: loke.gir.dk 1399933589 14807 69.95.181.76 (12 May 2014 22:26:29 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Mon, 12 May 2014 22:26:29 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Xref: news.eternal-september.org comp.lang.ada:19792
Date: 2014-05-12T17:26:28-05:00
List-Id: <comp.lang.ada>

"Adam Beneschan" <adambeneschan@gmail.com> wrote in message 
news:dd27f835-8295-4cb2-aa28-2ff3f351b0e0@googlegroups.com...
>On Monday, May 12, 2014 5:54:52 AM UTC-7, Jacob Sparre Andersen wrote:
>> Reading the fine print on subtype predicates and type invariants, I
>> noticed that section 3.2.4 (on subtype predicates) doesn't have a
>> paragraph matching 7.3.2(5/3) (on type invariants).
>>
>> 7.3.2(5/3): Within an invariant expression, the identifier of the first
>>             subtype of the associated type denotes the current instance
>>             of the type. Within an invariant expression associated with
>>             type T, the type of the current instance is T for the
>>             Type_Invariant aspect and T'Class for the
>>             Type_Invariant'Class aspect.
>
>FYI, the first sentence is true for both subtype predicates and type 
>invariants.  It's actually redundant in 7.3.2(5/3), >and the AARM shows it 
>as such (http://www.ada-auth.org/standards/12aarm/html/AA-7-3-2.html); 
>13.1.1(12/3) >applies to all aspect clauses on type and subtype 
>declarations.  I'd guess that the authors felt that in 7.3.2(5/3), they 
> >needed to repeat the rule in the first sentence in order to provide some 
>context to help readers understand the >second sentence.

Right; this is the consequence of other rules and does not need to be 
mentioned in 3.2.4 (or 7.3.2, for that matter). There was an issue that the 
properties of the current instance of a subtype aren't well-defined; that's 
the issue of AI12-0068-1. We expect this will end up as conservative as 
possible (the current instance is a value, not an object), but it hasn't be 
resolved yet. (It's on Tucker's homework list, but he didn't get to it 
before the last meeting.)

                                        Randy.