From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
Subject: Re: Ada2012 Invariants and obaque types
Date: Tue, 21 Jun 2011 15:29:22 +0200
Date: 2011-06-21T15:29:22+02:00 [thread overview]
Message-ID: <4e009cb2$0$6582$9b4e6d93@newsspool3.arcor-online.net> (raw)
In-Reply-To: <12jyfk40laprz.1mxczd0ze0dr7.dlg@40tude.net>
On 21.06.11 14:31, Dmitry A. Kazakov wrote:
>> In another theory, the invariant may express things
>> such as
>> Num_Green_Lights (T1) >= 3;
>> or
>> 'Length < State_of_Things (T1) * 2;
>> where Num_Green_Lights is a publicly visible function whose
>> result is somehow computed. These predicates would be informative,
>> and formal.
>
> That is not an invariant, but a constraint.
I don't see bounds in the above.
I can state, though, that there will be---invariably---at least
three green lights because that is a property of how each
implementation of the type will be constructed. How is that
variant? That is, if the (theoretical) assertion is "at least,
no matter what, under all circumstances, in each implementation",
isn't this an invariant?
next prev parent reply other threads:[~2011-06-21 13:29 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
2011-06-21 12:17 ` Georg Bauhaus
2011-06-21 12:31 ` Dmitry A. Kazakov
2011-06-21 13:29 ` Georg Bauhaus [this message]
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