Re: Ada2012 Invariants and obaque types

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

On Tue, 21 Jun 2011 20:37:44 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Tue, 21 Jun 2011 14:08:15 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
> 
>> 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 understand the point and had the same first feeling too.

The first feeling is always the right one. (:-))

> While that's OK  
> in theory, in practice the user may wish methods to check for validity  
> rules defined for a type.

Validity is a misconception. In a properly typed language any value is
valid, that is the property of being typed. A value is invalid when the
type system was circumvented, which should never happen publicly.

> Then, Is_Valid is abstract enough. And  
> after-all, you already have 'Valid attribute in Ada. This is useful for  
> designs relying on defensive programming and which disallow use of  
> exceptions.

'Valid is a hack around missing value initialization enforcement or some
kludges to support Unchecked_Conversion. It cannot justify anything because
'Valid itself lacks credibility.

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