Re: My bug or else regarding Visibility Rules

["Randy Brukardt" <randy@rrsoftware.com>]

"Anh Vo" <anhvofrcaus@gmail.com> wrote in message 
news:d09afc35-2ca5-4b45-9734-7263e6d353c4@googlegroups.com...
On Monday, April 1, 2013 5:56:19 PM UTC-7, Randy Brukardt wrote:
...
>>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.

>I try to put as much as post-conditions that the language allows. On the 
>other hand,
>I do not want to expose any thing that the clients can modify. In addition, 
>taking away
>post-conditions involving Buffer, In_Index, and Out_Index objects by moving 
>them
>into the body does degrade much implementation promise in this case.

The only things that should be in Post aspects are those that the client 
might care about.

We've talked a bit about "body postconditions" that wouldn't be visible to 
the client. That's what you want here, but Ada doesn't have that yet. Talk 
to your vendor and convince them to support Body_Post or something like that 
(implementation-defined aspects are allowed, just like 
implementation-defined attributes are allowed).

                                          Randy.