Version 1.5 of ai12s/ai1201501.txt
!standard 7.3.2(3/3) 150128 AI1201501/03
!standard 7.3.2(5/3)
!standard 7.3.2(9/3)
!standard 7.3.2(22/3)
!class binding interpretation 150126
!status Corrigendum 2015 150128
!status WG9 Approved 150626
!status ARG Approved 901 150128
!status work item 150126
!status received 150126
!priority Medium
!difficulty Medium
!qualifier Omission
!subject Classwide type invariants and statically bound calls
!summary
Classwide preconditions, postconditions, and type invariants are processed
using the actual types for the parameters of type T (not always using T'Class).
In particular, for a statically bound call, the calls within the
Type_Invariant'Class expression that apply to the type T are statically bound,
if the object being checked is itself of a specific type.
!question
RM 7.3.2(5/3) says:
[AARM Redundant: Within an invariant expression, the identifier of the
first subtype of the associated type denotes the current instance of the
type.] Within an invariant expression associated with type T, the type
of the current instance is T for the Type_Invariant aspect and T'Class
for the Type_Invariant'Class aspect.
However, in analogy with Pre'Class as discussed in AI1201131, simply
resolving all calls appearing in the Type_Invariant'Class expression for
a type T by interpreting it as T'Class will cause all calls to be
dispatching calls, even when applied to objects where their compiletime
type does not match the underlying tag were it to be converted to
T'Class.
Should this be corrected? (Yes.)
!recommendation
(See Summary.)
!wording
Modify 7.3.2(3/4) (as modified by AI1200411):
This aspect shall be specified by an expression, called an invariant
expression. Type_Invariant'Class may be specified on a
private_type_declaration, a private_extension_declaration, or a
full_type_declaration for an interface type.{ Type_Invariant'Class
determines a classwide type invariant for a tagged type.}
Modify 7.3.2(5/3):
[AARM Redundant: Within an invariant expression, the identifier of
the first subtype of the associated type denotes the current instance
of the type.] Within an invariant expression [associated with] {for
the Type_Invariant aspect of a} type T, the type of [the]{this} current
instance is T[ for the Type_Invariant aspect, and T'Class]{. Within
an invariant expression} for the Type_Invariant'Class aspect {of a
type T, the type of this current instance is interpreted as though it
had a (notional) type NT that is a visible formal derived type whose
ancestor type is T. [AARM Redundant: The effect of this
interpretation is that the only operations that can be applied to this
current instance are those defined for such a formal derived type.
This ensures that the invariant expression is welldefined for any
type descended from T.]}
Modify 7.3.2(9/3):
(In Dynamic Semantics)
If one or more invariant expressions apply to a {nonabstract} type
T, then an invariant check is performed at the following places, on
the specified object(s):
Add after 7.3.2(22/3):
For an invariant check on a value of type T1 based on a classwide invariant
expression inherited from an ancestor type T, any operations within the
invariant expression that were resolved as primitive operations of the
(notional) formal derived type NT, are in the evaluation of the invariant
expression for the check on T1 bound to the corresponding operations of type
T1.
!discussion
Consider two nearly identical hierarchies of types. First:
package P11 is
type Root is abstract tagged private
with Type_Invariant => Is_Valid (Root);
function Is_Valid (P : in Root) return Boolean;
procedure Proc (P : out Root);
procedure Proc2 (P : out Root);
private
...
end P11;
with P11;
package P12 is
type Child is new P11.Root with private
with Type_Invariant => Is_Valid (Child);
overriding
function Is_Valid (P : in Child) return Boolean;
overriding
procedure Proc (P : out Child);

private
...
end P12;
with P12;
package P13 is
type GrandChild is new P12.Child with private
with Type_Invariant => Is_Valid (GrandChild);
overriding
function Is_Valid (P : in Grandchild) return Boolean;
overriding
procedure Proc (P : out Grandchild);

private
...
end P13;
and the second hierarchy is:
package P21 is
type Root is abstract tagged private
with Type_Invariant'Class => Is_Valid (Root);
function Is_Valid (P : in Root) return Boolean;
procedure Proc (P : out Root);
procedure Proc2 (P : out Root);
private
...
end P21;
with P21;
package P22 is
type Child is new P21.Root with private;
overriding
function Is_Valid (P : in Child) return Boolean;
overriding
procedure Proc (P : out Child);

private
...
end P22;
with P22;
package P23 is
type GrandChild is new P22.Child with private;
overriding
function Is_Valid (P : in Grandchild) return Boolean;
overriding
procedure Proc (P : out Grandchild);

private
...
end P23;
The only difference between these hierarchies is that the first uses a
specific Type_Invariant on each type, the second uses a classwide
Type_Invariant just on the Root type, allowing it to be inherited by
descendant types.
Our intent is that these behave identically at runtime, with the only
difference being that there is an additional guarantee that a new
descendant of P21.Root will also have the Type_Invariant'Class
expression (that has to be manually added in the other hierarchy).

We define the meaning of Type_Invariant'Class in terms of a notional
formal derived type so that only primitive operations of the type can be
used in the expression. The original Ada 2012 definition of the current
instance as T'Class also has a runtime effect that we do not want (as
noted above).
In addition, defining the current instance as having T'Class introduces
other problems. For instance, with a global variable:
type T is tagged ...
with Type_Invariant'Class => Is_Valid_2 (T, G);
G : T'Class := ...;
function Is_Valid_2 (A, B : T) return Boolean;
If the current instance T is considered to have T'Class, this expression
is legal (both operands being dynamically tagged). But this doesn't make
sense for an inherited type:
type T1 is new T with ...;


But this Type_Invariant'Class makes no sense, as G does not match type
T1'Class.
If we simply left the current instance having type T, then nonprimitive
operations of the type could be used in Type_Invariant'Class  but
descendant types have no such operations. We could have rechecked the
Type_Invariant'Class for each descendant type, but that causes problems
if visibility has changed somehow (especially for classwide
operations).
On the other hand, a formal derived type has just the operations that we
want to allow (primitive operations) but no others. In particular, G in
the example above does not match the NT type, so the above problem can't
happen.

We added "nonabstract" to 7.3.2(9/3) because a classwide invariant cannot
be reliably enforced on an abstract type, because some of the operations used
in the original invariant expression might be abstract for an abstract
descendant. Even if all of the operations are nonabstract for a particular
abstract descendant, it seems unwise and a potential maintenance trap to have
the enforcement of the classwide invariant depend on that.
This does not provide a hole in the checking provided by classwide type
invariants, even in the case of a concrete operation inherited by a descendant,
because the checking on the implicit view conversions that are part of a call
on an inherited subprogram will make the checks for any object of a concrete
type. (And there cannot be an object of abstract type!)
!corrigendum 7.3.2(3/3)
Replace the paragraph:
 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.
by:
 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, a private_extension_declaration, or
a full_type_declaration for an interface type. Type_Invariant'Class
determines a classwide type invariant for a tagged type.
!corrigendum 7.3.2(5/3)
Replace the paragraph:
Within an invariant expression, the identifier of
the first subtype of the associated type denotes the current instance
of the type. Within an invariant expression associated with type T,
the type of the current instance is T for the Type_Invariant aspect and
T'Class for the Type_Invariant'Class aspect.
by:
Within an invariant expression, the identifier of
the first subtype of the associated type denotes the current instance
of the type. Within an invariant expression for the Type_Invariant aspect
of a type T, the type of this current instance is T. Within
an invariant expression for the Type_Invariant'Class aspect of a type
T, the type of this current instance is interpreted as though it
had a (notional) type NT that is a visible formal derived type whose
ancestor type is T. The effect of this interpretation is that the
only operations that can be applied to this
current instance are those defined for such a formal derived type.
This ensures that the invariant expression is welldefined for any
type descended from T.
!corrigendum 7.3.2(9/3)
Replace the paragraph:
If one or more invariant expressions apply to a type T, then an
invariant check is performed at the following places, on the specified object(s):
by:
If one or more invariant expressions apply to a nonabstract type T, then an
invariant check is performed at the following places, on the specified object(s):
!corrigendum 7.3.2(22/3)
Insert after the paragraph:
The invariant check consists of the evaluation of each enabled invariant
expression that applies to T, on each of the objects specified above.
If any of these evaluate to False, Assertions.Assertion_Error is
raised at the point of the object initialization, conversion, or call.
If a given call requires more than one evaluation of an invariant
expression, either for multiple objects of a single type or for
multiple types with invariants, the evaluations are performed in an
arbitrary order, and if one of them evaluates to False, it is not specified
whether the others are evaluated. Any invariant check is performed
prior to copying back any bycopy in out or out parameters.
Invariant checks, any postcondition check, and any constraint or predicate checks
associated with in out or out parameters are performed in an arbitrary order.
the new paragraph:
For an invariant check on a value of type T1 based on a classwide invariant
expression inherited from an ancestor type T, any operations within the
invariant expression that were resolved as primitive operations of the
(notional) formal derived type NT, are in the evaluation of the invariant
expression for the check on T1 bound to the corresponding operations of type
T1.
!ASIS
No ASIS effect.
!ACATS test
An ACATS CTest is needed to check that this check is made.
!appendix
From: Tucker Taft
Sent: Monday, January 26, 2015 4:39 PM
Here is a new AI, carved off of AI120133 (which dealt with Pre'Class), to deal
with name resolution of current instances within a Type_Invariant'Class
expression. It steals liberally from the Pre'Class AI.
[This is version /01 of the AI  Editor.]
****************************************************************
From: Randy Brukardt
Sent: Monday, January 26, 2015 7:55 PM
> Here is a new AI, carved off of AI120133 (which dealt with
You mean AI1201131 (you doubled the wrong digit).
> Pre'Class), to deal with name resolution of current instances within a
> Type_Invariant'Class expression. It steals liberally from the
> Pre'Class AI.
In looking at this, you don't have any wording corresponding to the wording in
6.1.1(37/3):
{Any operations within a classwide postcondition expression that were resolved
as primitive operations of the (notional) formal derived type NT, are in the
evaluation of the postcondition bound to the corresponding operations of the
type identified by the controlling tag of the call on S. [Redundant: This
applies to both dispatching and nondispatching calls on S.]}
It would need that we'd need wording like this somewhere (probably in or after
7.3.2(22/3), although we have to be careful since not all invariant checks are
associated with a call. Maybe something like:
{For any invariant check associated with the return from a call on a primitive
subprogram S, any operations within a classwide type invariant expression that
were resolved as primitive operations of the (notional) formal derived type NT,
are in the evaluation of the type invariant bound to the corresponding
operations of the type identified by the controlling tag of the call on S.
[Redundant: This applies to both dispatching and nondispatching calls on S.].
Similarly, a type invariant check associated with a view conversion from a
specific type T are bound to the corresponding operations of the type identified
by the type T.}
[We also probably would need to define "classwide type invariant", which not
currently a term, but one I want to use every time I write wording or notes for
this clause.] So add something to 7.3.2(3/4), perhaps:
"Type_Invariant'Class determines a *classwide type invariant* for a tagged
type."
===
7.3.2(9/3) seems to represent an unrelated bug in Type_Invariants that you just
noticed in trying to match the other wording. Probably should say a few words
about it in the !discussion. Specifically:
package P is
type T is abstract tagged private
with Type_Invariant'Class => Is_OK (T);
function Is_OK (A : in T) return Boolean is abstract;
procedure Concrete (Obj : in out T);
private
...
end P;
We had better not try to call Is_OK when evaluating the type invariant for
Concrete. Thus we don't make any invariant checks on the body of Concrete.
This won't cause a hole, since the invariant will be evaluated for the view
conversion needed to reach the body of Concrete for some derived type.
Specifically:
with P;
package P2 is
type TT is new P.T with private;
function Is_OK (A : in TT) return Boolean;
 inherits procedure Concrete (Obj : in out TT);
private
...
end P2;
A call on the inherited Concrete with an object of type TT includes an implicit
view conversion to T. This triggers an invariant check via 7.3.2(1214/3), which
calls Is_OK on type TT. The same thing happens for a dispatching call. So the
lack of a check directly on the subprogram is not a problem. (Note that abstract
types can't use a nonclasswide type invariant, so the invariant is always
inherited.)
Now it makes more sense to me, hope this explanation will help someone else
understand it.
****************************************************************
From: Tucker Taft
Sent: Monday, January 26, 2015 9:10 PM
>> Here is a new AI, carved off of AI120133 (which dealt with
>
> You mean AI1201131 (you doubled the wrong digit).
Oops.
>> Pre'Class), to deal with name resolution of current instances within
>> a Type_Invariant'Class expression. It steals liberally from the
>> Pre'Class AI.
>
> In looking at this, you don't have any wording corresponding to the
> wording in 6.1.1(37/3):
>
> {Any operations within a classwide postcondition expression that were
> resolved as primitive operations of the (notional) formal derived type
> NT, are in the evaluation of the postcondition bound to the
> corresponding operations of the type identified by the controlling tag of the call on S.
> [Redundant: This applies to both dispatching and nondispatching calls
> on S.]}
>
> It would need that we'd need wording like this somewhere (probably in
> or after 7.3.2(22/3), although we have to be careful since not all
> invariant checks are associated with a call. Maybe something like:
>
> {For any invariant check associated with the return from a call on a
> primitive subprogram S, any operations within a classwide type
> invariant expression that were resolved as primitive operations of the
> (notional) formal derived type NT, are in the evaluation of the type
> invariant bound to the corresponding operations of the type identified
> by the controlling tag of the call on S. [Redundant: This applies to
> both dispatching and nondispatching calls on S.]. Similarly, a type
> invariant check associated with a view conversion from a specific type
> T are bound to the corresponding operations of the type identified by
> the type T.}
Not sure why you have the first part. Why isn't this more general. E.g.:
{For an invariant check on a value of type T1 based on a classwide invariant expression inherited from an ancestor type T, any operations within the invariant expression that were resolved as primitive operations of the (notional) formal derived type NT,
are in the evaluation of the invariant expression for the check on T1 bound to the corresponding operations of type T1.}
> [We also probably would need to define "classwide type invariant",
> which not currently a term, but one I want to use every time I write
> wording or notes for this clause.] So add something to 7.3.2(3/4), perhaps:
>
> "Type_Invariant'Class determines a *classwide type invariant*
> for a tagged type."
OK.
> ===
>
> 7.3.2(9/3) seems to represent an unrelated bug in Type_Invariants that
> you just noticed in trying to match the other wording. Probably should
> say a few words about it in the !discussion.
Oops, yes I meant to mention why I inserted "nonabstract."
****************************************************************
From: Randy Brukardt
Sent: Monday, January 26, 2015 9:25 PM
...
> > {For any invariant check associated with the return from a call on a
> > primitive subprogram S, any operations within a classwide type
> > invariant expression that were resolved as primitive operations of
> > the
> > (notional) formal derived type NT, are in the evaluation of the type
> > invariant bound to the corresponding operations of the type
> > dentified by the controlling tag of the call on S. [Redundant: This
> > applies to both dispatching and nondispatching calls on S.].
> > Similarly, a type invariant check associated with a view conversion
> > from a specific type T are bound to the corresponding operations of
> > the type identified by the type T.}
>
> Not sure why you have the first part. Why isn't this more general.
Because I couldn't figure out how to do that. That's why we keep you around.
:)
> E.g.:
>
> {For an invariant check on a value of type T1 based on a classwide
> invariant expression inherited from an ancestor type T, any operations
> within the invariant expression that were resolved as primitive
> operations of the (notional) formal derived type NT, are in the
> evaluation of the invariant expression for the check on T1 bound to
> the corresponding operations of type T1.}
Look good to me.
> > [We also probably would need to define "classwide type invariant",
> > which not currently a term, but one I want to use every time I write
> > wording or notes for this clause.] So add something to 7.3.2(3/4),
perhaps:
> >
> > "Type_Invariant'Class determines a *classwide type invariant*
> > for a tagged type."
>
> OK.
>
> > ===
> >
> > 7.3.2(9/3) seems to represent an unrelated bug in
> Type_Invariants that
> > you just noticed in trying to match the other wording.
> Probably should
> > say a few words about it in the !discussion.
>
> Oops, yes I meant to mention why I inserted "nonabstract."
Could I get a few words from you? I wrote a novella when I tried it in my
email.
(I'll update the AI this way, if you prefer. And 90% of ARG members prefer to
let Randy do the work. ;)
****************************************************************
From: Tucker Taft
Sent: Monday, January 26, 2015 10:31 PM
> Could I get a few words from you? I wrote a novella when I tried it in
> my email.
How about at the very end:
We added "nonabstract" to 7.3.2(9/3) because a classwide invariant cannot
be reliably enforced on an abstract type, because some of the operations used
in the original invariant expression might be abstract for an abstract
descendant. Even if all of the operations are nonabstract for a particular
abstract descendant, it seems unwise and a potential maintenance trap to have
the enforcement of the classwide invariant depend on that.
> (I'll update the AI this way, if you prefer. And 90% of ARG members
> prefer to let Randy do the work. ;)
Thanks.
****************************************************************
Questions? Ask the ACAA Technical Agent