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.92.202 with SMTP id co10mr2345925wib.1.1365340756109;
        Sun, 07 Apr 2013 06:19:16 -0700 (PDT)
MIME-Version: 1.0
Path: 
 p18ni42828wiv.0!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.139.MISMATCH!xlned.com!feeder7.xlned.com!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!gandalf.srv.welterde.de!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: Tue, 2 Apr 2013 17:04:34 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <kjfkli$3g8$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>
 <kjdabm$dck$1@munin.nbi.dk>
 <d09afc35-2ca5-4b45-9734-7263e6d353c4@googlegroups.com>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: munin.nbi.dk 1364940275 3592 69.95.181.76 (2 Apr 2013 22:04:35 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 2 Apr 2013 22:04:35 +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-02T17:04:34-05:00
List-Id: <comp.lang.ada>

"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.