From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: My bug or else regarding Visibility Rules
Date: Mon, 1 Apr 2013 19:56:19 -0500
Date: 2013-04-01T19:56:19-05:00 [thread overview]
Message-ID: <kjdabm$dck$1@munin.nbi.dk> (raw)
In-Reply-To: 89292c53-1d4e-48a7-b2ae-a10983ef4168@googlegroups.com
"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.
next prev parent reply other threads:[~2013-04-02 0:56 UTC|newest]
Thread overview: 15+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-03-28 19:54 My bug or else regarding Visibility Rules Anh Vo
2013-03-28 20:58 ` Adam Beneschan
2013-03-28 22:03 ` Randy Brukardt
2013-03-30 6:05 ` Anh Vo
2013-04-02 0:56 ` Randy Brukardt [this message]
2013-04-02 1:52 ` Anh Vo
2013-04-02 8:26 ` Simon Wright
2013-04-02 18:17 ` Anh Vo
2013-04-02 20:16 ` Simon Wright
2013-04-03 23:21 ` Anh Vo
2013-04-04 8:19 ` Simon Wright
2013-04-04 19:21 ` Anh Vo
2013-04-04 19:47 ` Simon Wright
2013-04-02 22:04 ` Randy Brukardt
2013-03-28 22:06 ` Anh Vo
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox