Re: Ada2012 Invariants and obaque types

[Manuel Collado <m.collado@domain.invalid>]

El 21/06/2011 20:53, Dmitry A. Kazakov escribi�:
> 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.

Humm... What about an integral type whose set of valid values are the 
prime numbers (upto some representation limit)?

Common practice is to define such type as Integer, Natural or Positive, 
and write some validation function to check values at runtime.

Or do you mean that Ada is not a properly typed language?

-- 
Manuel Collado - http://lml.ls.fi.upm.es/~mcollado