Re: Ada2012 Invariants and obaque types

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

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.

Would they be private implementation dependent things?  Or could
I expect, seeing the public view and its invariant, the possibility
of different implementations (of both the view and the invariant)?