CVS difference for ai05s/ai05-0146-1.txt

--- ai05s/ai05-0146-1.txt	2010/06/14 01:07:52	1.7
+++ ai05s/ai05-0146-1.txt	2010/08/12 04:49:48	1.8
@@ -1,6 +1,7 @@
-!standard 11.5 (00)                                10-06-06  AI05-0146-1/04
+!standard 11.5 (00)                                10-08-11  AI05-0146-1/05
 !standard 11.4.1 (10)
 !class amendment 09-02-15
+!status ARG Approved  8-0-1  10-06-20
 !status work item 09-02-15
 !status received 09-02-15
 !priority Medium
@@ -81,29 +82,36 @@
 
   13.3.3 Type Invariants
 
-  An invariant for a private type or private extension may be specified
-  using an aspect_specification for the aspect Invariant and, if tagged,
-  for the aspect Invariant'Class.  The associated expression is called
-  an *invariant expression*.
+  For a private type or private extension, the following language-defined aspects
+  may be specified:
+    Type_Invariant
+       This aspect shall be specified by an expression, called an *invariant
+       expression*. The expected type for the expression is any boolean type.
+       Type_Invariant may be specified on a private_type_declaration or a
+       private_extension_declaration.
+    Type_Invariant'Class
+       This aspect shall be specified by an expression, called an *invariant
+       expression*. The expected type for the expression is any boolean type.
+       Type_Invariant'Class may be specified on a private_type_declaration or a
+       private_extension_declaration.
 
          Name Resolution
 
-  The expected type for an invariant expression is the predefined type
-  Boolean. [Redundant: Within an invariant expression, the identifier of
+  [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 Invariant aspect and
-  T'Class for the Invariant'Class aspect.
+  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.
 
         Legality Rules
 
-  [Redundant: The Invariant'Class aspect shall not be specified for an
-  untagged type.] The Invariant aspect shall not be specified for an
+  The Type_Invariant'Class aspect shall not be specified for an
+  untagged type. The Type_Invariant aspect shall not be specified for an
   abstract type.
 
         Static Semantics
 
-  [Redundant: If the Invariant'Class aspect is specified for a tagged type T,
+  [Redundant: If the Type_Invariant'Class aspect is specified for a tagged type T,
   then the invariant expression applies to all descendants of T.]
 
         Dynamic Semantics
@@ -116,6 +124,9 @@
 
   * After conversion to type T, on the result of the conversion;
 
+  * After a call on the Read or Input stream attribute of the type T, on the object
+    initialized by the stream attribute;
+
   * Upon return from a call on any subprogram or entry that:
       - has a result of type T, or one or more IN OUT or OUT
         parameters of type T,
@@ -207,11 +218,14 @@
 by the subprogram invoked, whether directly or indirectly, to match
 the rule for pre- and postconditions.
 
-Note that we do not worry about subprograms that have their Access attribute
-evaluated, even though they might be called from outside the package.
-We recognize there are holes in the protection provided by type invariants,
-so we don't require herculean efforts to catch all possible ways a value
-might be updated and then become externally accessible.
+We do not worry about non-externally visible subprograms that have their
+Access attribute evaluated, even though the access value might be passed
+out of the package and called from outside the package. Therefore there are
+holes in the protection provided by type invariants. Note, however, these
+holes can only be created by the package itself (by passing out
+access-to-subprogram values); a client cannot create them on their own. Thus
+we don't require herculean efforts to catch all possible ways a value
+might be updated and then become externally accessible. 
 
 Assertion Policy