From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Ada2012 Invariants and obaque types
Date: Tue, 21 Jun 2011 14:08:15 +0200
Date: 2011-06-21T14:08:15+02:00 [thread overview]
Message-ID: <17t4afbmsrbm4.7llaajq91zz3.dlg@40tude.net> (raw)
In-Reply-To: 239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com
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
next prev parent reply other threads:[~2011-06-21 12:08 UTC|newest]
Thread overview: 31+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-06-21 8:53 Ada2012 Invariants and obaque types Martin
2011-06-21 10:27 ` Yannick Duchêne (Hibou57)
2011-06-21 10:36 ` Martin
2011-06-21 10:46 ` Martin
2011-06-21 18:42 ` Yannick Duchêne (Hibou57)
2011-06-21 10:43 ` Ludovic Brenta
2011-06-21 10:53 ` Martin
2011-06-21 11:14 ` Martin
2011-06-21 11:31 ` Robert A Duff
2011-06-21 11:48 ` Martin
2011-06-21 12:01 ` Martin
2011-06-21 12:13 ` Robert A Duff
2011-06-21 12:22 ` Martin
2011-06-21 12:54 ` Robert A Duff
2011-06-21 13:00 ` Martin
2011-06-21 12:08 ` Dmitry A. Kazakov [this message]
2011-06-21 12:17 ` Georg Bauhaus
2011-06-21 12:31 ` Dmitry A. Kazakov
2011-06-21 13:29 ` Georg Bauhaus
2011-06-21 14:42 ` Dmitry A. Kazakov
2011-06-21 18:37 ` Yannick Duchêne (Hibou57)
2011-06-21 18:53 ` Dmitry A. Kazakov
2011-06-21 19:34 ` Vinzent Hoefler
2011-06-21 20:52 ` Dmitry A. Kazakov
2011-06-21 21:50 ` Vinzent Hoefler
2011-06-22 7:55 ` Dmitry A. Kazakov
2011-06-21 21:18 ` Manuel Collado
2011-06-22 8:00 ` Dmitry A. Kazakov
2011-06-22 10:39 ` Egil Høvik
2011-06-22 13:57 ` Martin
2011-06-23 16:21 ` anon
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox