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.224.160.65 with SMTP id m1mr3488714qax.2.1365342159261;
        Sun, 07 Apr 2013 06:42:39 -0700 (PDT)
Path: 
 ef9ni13619qab.0!nntp.google.com!border1.nntp.dca.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!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!nuzba.szn.dk!pnx.dk!eternal-september.org!feeder.eternal-september.org!mx05.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: My bug or else regarding Visibility Rules
Date: Tue, 02 Apr 2013 09:26:12 +0100
Organization: A noiseless patient Spider
Message-ID: <lywqslgwyj.fsf@pushface.org>
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>
Mime-Version: 1.0
Injection-Info: mx05.eternal-september.org;
 posting-host="72a7bb6120f61bc7749e29c9c2e535af";
	logging-data="3479"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/BWQmA5u3ZHl0BZoRDfz1bs9Z0t/ACz0g="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.2 (darwin)
Cancel-Lock: sha1:Bi9IGsNr113tRyLzXL0GCspSv9M=
	sha1:nBa6hddF0wy+GWUda7BLg2MTdhA=
Content-Type: text/plain
Date: 2013-04-02T09:26:12+01:00
List-Id: <comp.lang.ada>

Anh Vo <anhvofrcaus@gmail.com> writes:

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

This is (partly) why we now have expression functions; specify the
function in the public part, use it in a pre/postcondition, complete it
with an expression function in the private part when Buffer etc. are
visible.