--- ai12s/ai12-0199-1.txt 2016/10/06 01:29:00 1.2 +++ ai12s/ai12-0199-1.txt 2016/11/15 01:10:52 1.3 @@ -1,5 +1,8 @@ -!standard 7.3.2(5/4) 16-10-05 AI12-0199-1/02 +!standard 7.3.2(5/4) 16-11-14 AI12-0199-1/03 +!standard 7.3.2(8/3) !class binding interpretation 16-07-21 +!status Amendment 1-2012 16-11-14 +!status ARG Approved 7-0-2 16-10-09 !status work item 16-07-21 !status received 16-06-11 !priority Low @@ -8,11 +11,11 @@ !subject Abstract subprogram calls in class-wide invariant expressions !summary -Do not apply class-wide type invariants to abstract types, to avoid -various problems. Define the notion of a "corresponding expression" for -a class-wide type invariant, replacing references to components as -appropriate, taking into account rules for corresponding and specified -discriminants. +Class-wide type invariants do not apply to abstract types, to avoid various +problems. Define the notion of a "corresponding expression" for a class-wide +type invariant, replacing references to components as appropriate, taking into +account rules for corresponding and specified discriminants when applying them +to a nonabstract descendant. !question @@ -25,9 +28,10 @@ function F1 (X : Ifc) return Boolean is abstract; end Pkg; -Does the call to F1 violate the rule against non-dispatching calls to abstract +Does the call to F1 violate the rule against nondispatching calls to abstract subprograms? - (No, because aspect re-interpreted using notional, non-abstract descendant) + (No, because the aspect is reinterpreted using notional, nonabstract + descendant) !recommendation @@ -48,11 +52,11 @@ can be applied to this current instance are those defined for such a formal derived type. -Modify 7.3.2(8): +Modify 7.3.2(8/3): If the Type_Invariant'Class aspect is specified for a tagged type T, - then [the invariant expression applies to all descendants of T] {then - a /corresponding expression/ also applies to each non-abstract - descendant T1 of T [(including T itself if it is non-abstract)]}. {The + then [the invariant expression applies to all descendants of T] {a + /corresponding expression/ also applies to each nonabstract + descendant T1 of T [(including T itself if it is nonabstract)]}. {The corresponding expression is constructed from the associated expression as follows: @@ -60,8 +64,12 @@ replaced with references to the corresponding components of T1 (or to T1 as a whole). + AARM Ramification: The only nondiscriminant components visible at the + point of such an aspect specification are necessarily inherited from some + nonprivate ancestor. + * References to discriminants of T are replaced with references to the - corresponding discriminant of T1 (see 3.7), or to the specified + corresponding discriminant of T1, or to the specified value for the discriminant, if the discriminant is specified by the derived_type_definition for some type that is an ancestor of T1 and a descendant of T (see 3.7).} @@ -69,7 +77,7 @@ !discussion For simplicity, we say that class-wide type invariants only apply to -non-abstract types. For an abstract type, no type invariant checks are +nonabstract types. For an abstract type, no type invariant checks are performed, nor should the type invariant expression be presumed true. This AI provides rules for class-wide type invariants analogous to those @@ -84,7 +92,7 @@ package Pkg2 is type T is tagged null record - with Type_Invariant'Class => Is_OK (X); -- OK. + with Type_Invariant'Class => Is_OK (X); function Is_Ok (X : T) return Boolean; procedure Proc (X : in out T); end Pkg2; @@ -95,7 +103,7 @@ with Pkg2; package Pkg3 is type NT is abstract new Pkg2.T null record; - -- inherits Type_Invariant'Class => Is_OK (X); -- Illegal. + -- inherits Type_Invariant'Class => Is_OK (X); function Is_Ok (X : NT) return Boolean is abstract; -- inherits Proc. end Pkg3; @@ -109,6 +117,55 @@ eliminates problems associated with type conversions to or across abstract types, and so on. +!corrigendum 7.3.2(5/4) + +@drepl +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 @i<T>, the type of this current instance is @i<T>. Within +an invariant expression for the Type_Invariant'Class aspect of a type +@i<T>, the type of this current instance is interpreted as though it +had a (notional) type @i<NT> that is a visible formal derived type whose +ancestor type is @i<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. +@dby +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 @i<T>, the type of this current instance is @i<T>. Within +an invariant expression for the Type_Invariant'Class aspect of a type +@i<T>, the type of this current instance is interpreted as though it +had a (notional) nonabstract type @i<NT> that is a visible formal derived +type whose ancestor type is @i<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. + + +!corrigendum 7.3.2(8/3) + +@drepl +If the Type_Invariant'Class aspect is specified for a tagged type @i<T>, +then the invariant expression applies to all descendants of @i<T>. +@dby +If the Type_Invariant'Class aspect is specified for a tagged type @i<T>, +then a /corresponding expression/ also applies to each nonabstract +descendant @i<T1> of @i<T> (including @i<T> itself if it is nonabstract). +The corresponding expression is constructed from the associated expression +as follows: + +@xbullet<References to non-discriminant components of @i<T> (or to @i<T> +itself) are replaced with references to the corresponding components of @i<T1> +(or to @i<T1> as a whole).> + +@xbullet<References to discriminants of @i<T> are replaced with references to +the corresponding discriminant of @i<T1>, or to the specified value for the +discriminant, if the discriminant is specified by the +@fa<derived_type_definition> for some type that is an ancestor of @i<T1> and +a descendant of @i<T> (see 3.7).> + + !ASIS No ASIS effect. @@ -180,17 +237,17 @@ case, so we do have some limits.) The straighforward version of the 6.1.1(18.2/4) rule would be something like: -A non-abstract type T is illegal if corresponding expression for a +A nonabstract type T is illegal if corresponding expression for a Type_Invariant'Class or Post'Class aspect would be illegal. But that doesn't fix the bug (NT is abstract in the example above). And -dropping "non-abstract" runs afoul of (1) above: it would make all invariants +dropping "nonabstract" runs afoul of (1) above: it would make all invariants of interfaces illegal. It seems easy enough to craft a rule to plug this particular bug: If the corresponding class-wide invariant expression for an abstract type T contains a call to an abstract routine, then there cannot be any - non-abstract subprograms in the immediately enclosing scope (including in + nonabstract subprograms in the immediately enclosing scope (including in nested scopes) that have a parameter with a part of T. But that has issues:

Questions? Ask the ACAA Technical Agent