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

--- ai05s/ai05-0146-1.txt	2010/08/12 04:49:48	1.8
+++ ai05s/ai05-0146-1.txt	2010/09/04 02:49:24	1.9
@@ -1,6 +1,6 @@
-!standard 11.5 (00)                                10-08-11  AI05-0146-1/05
-!standard 11.4.1 (10)
+!standard 13.3.3 (00)                                10-09-02  AI05-0146-1/06
 !class amendment 09-02-15
+!status Amendment 2012 10-09-02
 !status ARG Approved  8-0-1  10-06-20
 !status work item 09-02-15
 !status received 09-02-15
@@ -83,20 +83,22 @@
   13.3.3 Type Invariants
 
   For a private type or private extension, the following language-defined aspects
-  may be specified:
+  may be specified with an aspect_specification:
     Type_Invariant
        This aspect shall be specified by an expression, called an *invariant
-       expression*. The expected type for the expression is any boolean type.
+       expression*.
        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.
+       expression*. 
        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 any boolean type.
+
   [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,
@@ -321,9 +323,99 @@
 end Stacks;
 
 
+!corrigendum 13.3.3(0)
+
+@dinsc
+
+For a private type or private extension, the following language-defined aspects
+may be specified with an @fa<aspect_specification>:
+
+@xhang<@xterm<Type_Invariant>
+This aspect shall be specified by an @fa<expression>, called an @i<invariant
+expression>. Type_Invariant may be specified on a @fa<private_type_declaration>
+or a @fa<private_extension_declaration>.>
+
+@xhang<@xterm<Type_Invariant'Class>
+This aspect shall be specified by an @fa<expression>, called an @i<invariant
+expression>. Type_Invariant'Class may be specified on
+a @fa<private_type_declaration> or a
+@fa<private_extension_declaration>.>
+
+@s8<@i<Name Resolution Rules>>
+
+The expected type for an invariant expression is any boolean type.
+
+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 @i<T>,
+the type of the current instance is @i<T> for the Type_Invariant aspect and
+@i<T>'Class for the Type_Invariant'Class aspect.
+
+@s8<@i<Legality Rules>>
+
+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.
+
+@s8<@i<Static Semantics>>
+
+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>.
+
+@s8<@i<Dynamic Semantics>>
+
+If one or more invariant expressions apply to a type @i<T>, and the Assertion_Policy
+at the point of the partial view declaration for @i<T> is Check, then an
+invariant check is performed at the following places, on the specified object(s):
+
+@xbullet<After default initialization of an object of type @i<T>, on the new object;>
+
+@xbullet<After conversion to type @i<T>, on the result of the conversion;>
+
+@xbullet<After a call on the Read or Input stream attribute of the type @i<T>, on the object
+initialized by the stream attribute;>
+
+@xbullet<Upon return from a call on any subprogram or entry that:>
+
+@xinbull<has a result of type @i<T>, or one or more @b<in out> or @b<out>
+parameters of type @i<T>,>
+
+@xinbull<is explicitly declared within the immediate scope of type @i<T>
+(or is a part of an instance of a generic unit declared within
+the immediate scope of type @i<T>), and>
+
+@xinbull<is visible outside the immediate scope of type @i<T> or overrides
+        an operation that is visible outside the immediate scope of @i<T>,>
+
+@xindent<on the result object of type @i<T>, and on each @b<in out> or @b<out>
+actual parameter of type @i<T>.>
+
+The invariant check consists of the evaluation of each invariant
+expression that applies to @i<T>, on each of the objects specified above.
+If any of these evaluate to False, Ada.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 order of the evaluations is not
+specified, 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 @b<in out> or @b<out> parameters.  It is not
+specified whether any constraint checks associated with by-copy @b<in out>
+or @b<out> parameters are performed before or after any invariant checks.
+It is not specified whether any postcondition checks are performed
+before or after any invariant checks.
+
+The invariant checks performed on a call are determined by the subprogram
+or entry actually invoked, whether directly, as part of a dispatching call, or
+as part of a call through an access-to-subprogram value.
+
+If the Assertion_Policy in effect at the point of a
+subprogram or entry declaration is Ignore, then no invariant check is
+performed on a call on that subprogram or entry.
 
 !ACATS test
 
+An C-Test is needed to check that invariants are tested at approproiate places.
 
 !appendix