CVS difference for ai12s/ai12-0199-1.txt

--- 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: