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: 
 border1.nntp.dca.giganews.com!nntp.giganews.com!goblin3!goblin.stu.neva.ru!gegeweb.org!news.ecp.fr!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: Declaration of function in precondition
Date: Thu, 24 Apr 2014 20:45:48 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <ljceoc$r11$1@loke.gir.dk>
References: <lyzjjbt4rc.fsf@pushface.org>
 <5a38852c-512e-43c4-9c02-cdcf105f0397@googlegroups.com>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: loke.gir.dk 1398390348 27681 69.95.181.76 (25 Apr 2014 01:45:48 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Fri, 25 Apr 2014 01:45:48 +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: number.nntp.dca.giganews.com comp.lang.ada:186079
Date: 2014-04-24T20:45:48-05:00
List-Id: <comp.lang.ada>

"Adam Beneschan" <adambeneschan@gmail.com> wrote in message 
news:5a38852c-512e-43c4-9c02-cdcf105f0397@googlegroups.com...
> On Thursday, April 24, 2014 3:12:55 AM UTC-7, Simon Wright wrote:
>> I proposed this in answer to a question[1] on StackOverflow:
>>
>>
>>
>>    package RingBuffer is
>>       function Is_Full return Boolean;
>>       procedure Push(value: T) with Pre => not Is_Full;
>>       function Pop return T;
>>    private
>>       buffer: array(0..size) of T;
>>       readptr: integer := 0;
>>       writeptr: integer := 1;
>>       function Is_Full return Boolean is (Readptr = Writeptr);
>>    end RingBuffer;
>>
>> and it turns out that GNAT (GPL 2013, 4.9-20140119) is happy if I put
>> the spec of Is_Full after its use (but still in the visible part):
>>
>>       procedure Push(value: T) with Pre => not Is_Full;
>>       function Is_Full return Boolean;
>>
>> I can't see where in the ARM this is legalised?
>
> 13.1.1(11), I think.  But I'm not sure.
>
> "The usage names in an aspect_definition are not resolved at the point of 
> the associated declaration, but rather are resolved at the end of the 
> immediately enclosing declaration list."

Correct. In this case, aspect specifications are resolved at "private", so 
you can use anything in the visible part in them.

This property is necessary for some type-related aspects, else they would be 
useless:

    type Priv is private with Read => Read, Write => Write, Type_Invariant 
=> Is_Valid(Priv);

Since all of these need access to subprograms that have parameters of type 
Priv, and those *have* to follow the type declaration of Priv, none of these 
things could have been specified as aspects without this (admittedly 
strange) rule.

Most aspects are evaluated at the first freezing point of the associated 
entity (type in this case), so oddities are possible. There are some rules 
to prevent the worst ones -- but it's very unlikely that you'll ever run 
into them. After all, "the first freezing point" is something you worry 
about only if the compiler complains, and I recommend the same approach 
here. (Coincidentally, I was working on objectives and ACATS tests for those 
rules yesterday, so I'm more aware than usual about them.)

                                 Randy.