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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,146d9a693430fff2
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news1.google.com!news.glorb.com!feeder.erje.net!feeder.news-service.com!94.75.214.39.MISMATCH!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Ada2012 Invariants and obaque types
Date: Tue, 21 Jun 2011 14:08:15 +0200
Organization: cbb software GmbH
Message-ID: <17t4afbmsrbm4.7llaajq91zz3.dlg@40tude.net>
References: 
 <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: g2news1.google.com comp.lang.ada:19978
Date: 2011-06-21T14:08:15+02:00
List-Id: <comp.lang.ada>

On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:

> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);

Unrelated to Ada, but in theory, an invariant is a private implementation
dependent thing. An invariant is trivially true in all public views of the
object, i.e. between any two calls to the object's operations. From that
follows, when mentioned in a public part then:

   type T1 is tagged private with Invariant => True;

(Again, I don't know which ideas Ada designers had about invariants, I am
not a language lawyer.)

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de