Version 1.6 of ai12s/ai12-0150-1.txt

Unformatted version of ai12s/ai12-0150-1.txt version 1.6
Other versions for file ai12s/ai12-0150-1.txt

!standard 7.3.2(3/3)          15-01-28 AI12-0150-1/03
!standard 7.3.2(5/3)
!standard 7.3.2(9/3)
!standard 7.3.2(22/3)
!class binding interpretation 15-01-26
!status Corrigendum 1-2012 15-01-28
!status WG9 Approved 15-06-26
!status ARG Approved 9-0-1 15-01-28
!status work item 15-01-26
!status received 15-01-26
!priority Medium
!difficulty Medium
!qualifier Omission
!subject Class-wide type invariants and statically bound calls
!summary
Class-wide 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 AI12-0113-1, 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 compile-time 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 AI12-0041-1):
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 class-wide 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 well-defined 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 class-wide 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);
-- Proc2 inherited. 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);
-- Proc2 inherited. 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);
-- Proc2 inherited. 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);
-- Proc2 inherited. 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 class-wide 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 ...; -- with Type_Invariant'Class => Is_Valid_2 (T, G) -- inherits Is_Valid_2 (A, B : T1) return Boolean;
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 non-primitive 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 class-wide 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 class-wide 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 class-wide invariant depend on that.
This does not provide a hole in the checking provided by class-wide 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 class-wide 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 well-defined 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 by-copy 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 class-wide 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 C-Test 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 AI12-0133 (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 AI12-0133 (which dealt with

You mean AI12-0113-1 (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 class-wide 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 non-dispatching 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 class-wide 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 non-dispatching 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 "class-wide 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 *class-wide 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(12-14/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 non-class-wide 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 AI12-0133 (which dealt with
>
> You mean AI12-0113-1 (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 class-wide 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 non-dispatching 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 class-wide 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 non-dispatching 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 class-wide 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 "class-wide 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 *class-wide 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 class-wide 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 non-dispatching 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 class-wide
> 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 "class-wide 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 *class-wide 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
e-mail.

(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 e-mail.

How about at the very end:

   We added "non-abstract" to 7.3.2(9/3) because a class-wide 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 non-abstract for a particular
   abstract descendant, it seems unwise and a potential maintenance trap to have
   the enforcement of the class-wide 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