Re: Ada2012 Invariants and obaque types

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Tue, 21 Jun 2011 14:17:11 +0200, Georg Bauhaus wrote:

> On 21.06.11 14:08, Dmitry A. Kazakov wrote:
>> 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.)
> 
> 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. Constraint creates a subtype,
it is a type-algebraic operation. Invariant does nothing, it is just a
predicate known to be true for all instances of the type in public
contexts. As such it can be removed any time without changing the program
semantics. A constraint cannot be removed, because its violation is 1)
possible and legal, 2) has defined effect (exception). Violation of an
invariant in public context is impossible in a correct program.

   subtype Line is String (1..80); -- 1..80 is a constraint
   Line'Length = 80 -- This is an invariant

P.S. Again, no idea how Ada 2012 treats this issue, differently I guess.

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