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: a07f3367d7,75ce2ead897158b2
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.180.24.132 with SMTP id u4mr1248387wif.6.1365341486449;
        Sun, 07 Apr 2013 06:31:26 -0700 (PDT)
MIME-Version: 1.0
Path: 
 p18ni42846wiv.0!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.103.MISMATCH!feeder3.cambriumusenet.nl!feed.tweaknews.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!news.n-ix.net!news.bawue.net!news1.tnib.de!feed.news.tnib.de!news.tnib.de!weretis.net!feeder4.news.weretis.net!nuzba.szn.dk!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: My bug or else regarding Visibility Rules
Date: Mon, 1 Apr 2013 19:56:19 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <kjdabm$dck$1@munin.nbi.dk>
References: <0c77e832-e12b-446d-af24-78d77c358f1e@googlegroups.com>
 <25ee066d-3270-4efd-829f-ed40b04c0655@googlegroups.com>
 <kj2en4$9q1$1@munin.nbi.dk>
 <89292c53-1d4e-48a7-b2ae-a10983ef4168@googlegroups.com>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: munin.nbi.dk 1364864183 13716 69.95.181.76 (2 Apr 2013 00:56:23 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 2 Apr 2013 00:56:23 +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
Date: 2013-04-01T19:56:19-05:00
List-Id: <comp.lang.ada>

"Anh Vo" <anhvofrcaus@gmail.com> wrote in message 
news:89292c53-1d4e-48a7-b2ae-a10983ef4168@googlegroups.com...
> On Thursday, March 28, 2013 3:03:13 PM UTC-7, Randy Brukardt wrote:
>> "Adam Beneschan" <adam@irvine.com> wrote in message
>> news:25ee066d-3270-4efd-829f-ed40b04c0655@googlegroups.com...
>> > On Thursday, March 28, 2013 12:54:26 PM UTC-7, Anh Vo wrote:
>> >> For the codes below GNAT complains that In_Index, Buffer, and 
>> >> Out_Index
>> >> are undefined.
>> > However, if I comment out private key word, GNAT is happy. Did I 
>> > violate
>> > Ada syntax rules? Thanks.
>> >
>> > 13.1.1(11): 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.
>> >
>> > In your example, the "immediately enclosing declaration list" ends at 
>> > the
>> > keyword PRIVATE
>> > when that keyword is present; but if you take it out, the declaration 
>> > list
>> > ends at "end Circular_Queue;".
>>
>> Which is the long way to say that the expression of a public aspect has 
>> to
>> be made up only of public functions and objects. Otherwise, how would a
>> caller be able to figure out the meaning of a precondition that they are
>> required to meet? Clients can never be required to look in a private 
>> part.
>
> Actually, this part only involves post-conditions (implementer), not 
> preconditions (clients).

Clients need to know about postconditions as well, so that they know what 
properties are guaranteed after a call. Typically, that will show that some 
or all of a following precondition is going to be satisfied. Remember, both 
of these matter to both sides of a call:

A precondition is a requirement on a caller and a promise to an 
implementation; a postcondition is a promise to a caller and a requirement 
on an implementation.

                                      Randy.