Re: Type invariants and private extensions?

[Victor Porton <porton@narod.ru>]

Isn't it a good idea to modify the RM to allow type invariants also for 
derived types with null records?

Jere wrote:
> On Monday, September 11, 2017 at 5:27:54 PM UTC-4, Victor Porton wrote:
>> Egil H H wrote:
>> 
>> > On Monday, September 11, 2017 at 10:48:46 PM UTC+2, Victor Porton
>> > wrote:
>> >> > The Invariant will then be inherited by all derived types
>> >> 
>> >> It is not what I want. I want different invariants for different
>> >> derived types.
>> >> 
>> > 
>> > You can add new invariants in addition to the ones inherited
>> 
>> I cannot: the compiler gives an error:
>> 
>> package P is
>> 
>>   type T is tagged private;
>> 
>> private
>> 
>>   type T is tagged null record;
>> 
>> end P;
>> 
>> with P; use P;
>> 
>> package P1 is
>> 
>>   type T1 is new T with null record
>>     with Type_Invariant => True;
>> 
>> end P1;
>> 
>> 
>> $ gnatgcc -gnatc -c p1.ads
>> p1.ads:6:10: aspect "Type_Invariant" only allowed for private type or
>> corresponding full view
>> 
>> --
>> Victor Porton - http://portonvictor.org
> 
> You aren't applying it to a private type.  Try:
> 
>    package P1 is
>       
>       type T1 is new T with private
>          with Type_Invariant'Class => True;
>       
>    private
> 
>       type T1 is new T with null record;
>         
> 
>    end P1;
> 
> The relevant RM section:
> 
> 7.3.2
> 
> 2/3
> Type_Invariant
> 
> This aspect shall be specified by an expression, called an
> invariant expression. Type_Invariant may be specified on a
> private_type_declaration, on a private_extension_declaration,
> or on a full_type_declaration that declares the completion of
> a private type or private extension.
> 
> 3/3
> Type_Invariant'Class
> 
> This aspect shall be specified by an expression, called an
> invariant expression. Type_Invariant'Class may be specified
> on a private_type_declaration or a private_extension_declaration.
-- 
Victor Porton - http://portonvictor.org