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

Differences between 1.2 and version 1.3
Log of other versions for file ai12s/ai12-0150-1.txt

--- ai12s/ai12-0150-1.txt	2015/01/27 04:57:08	1.2
+++ ai12s/ai12-0150-1.txt	2015/01/30 05:23:10	1.3
@@ -1,8 +1,10 @@
-!standard 7.3.2(3/3)                                   15-01-27  AI05-0150-1/02
+!standard 7.3.2(3/3)                                   15-01-28  AI05-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 2015 15-01-28
+!status ARG Approved 9-0-1  15-01-28
 !status work item 15-01-26
 !status received 15-01-26
 !priority Medium
@@ -14,7 +16,8 @@
 
 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,
+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
@@ -34,7 +37,7 @@
 type does not match the underlying tag were it to be converted to
 T'Class.
 
-Should this be corrected? (Yes)
+Should this be corrected? (Yes.)
 
 !recommendation
 
@@ -42,7 +45,7 @@
 
 !wording
 
-Modify 7.3.2(4/3) (as modified by AI12-0041-1):
+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
@@ -70,7 +73,7 @@
 
 (In Dynamic Semantics)
 
-   If one or more invariant expressions apply to a {non-abstract} type
+   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):
 
@@ -93,7 +96,7 @@
 
        function Is_Valid (P : in Root) return Boolean;
 
-       function Proc (P : out Root)'
+       procedure Proc (P : out Root);
 
        procedure Proc2 (P : out Root);
    private
@@ -227,10 +230,10 @@
 
 ---
 
-We added "non-abstract" to 7.3.2(9/3) because a class-wide invariant cannot
+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 non-abstract for a particular
+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.
 
@@ -239,6 +242,75 @@
 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)
+
+@drepl
+@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>.>
+@dby
+@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>, a @fa<private_extension_declaration>, or
+a @fa<full_type_declaration> for an interface type. Type_Invariant'Class
+determines a @i<class-wide type invariant> for a tagged type.>
+
+!corrigendum 7.3.2(5/3)
+
+@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 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.
+@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) 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.
+This ensures that the invariant expression is well-defined for any
+type descended from @i<T>.
+
+!corrigendum 7.3.2(9/3)
+
+@drepl
+If one or more invariant expressions apply to a type @i<T>, then an
+invariant check is performed at the following places, on the specified object(s):
+@dby
+If one or more invariant expressions apply to a nonabstract type @i<T>, then an
+invariant check is performed at the following places, on the specified object(s):
+
+!corrigendum 7.3.2(22/3)
+
+@dinsa
+The invariant check consists of the evaluation of each enabled invariant
+expression that applies to @i<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 @b<in out> or @b<out> parameters.
+Invariant checks, any postcondition check, and any constraint or predicate checks
+associated with @b<in out> or @b<out> parameters are performed in an arbitrary order.
+@dinst
+For an invariant check on a value of type @i<T1> based on a class-wide invariant
+expression inherited from an ancestor type @i<T>, any operations within the
+invariant expression that were resolved as primitive operations of the
+(notional) formal derived type @i<NT>, are in the evaluation of the invariant
+expression for the check on @i<T1> bound to the corresponding operations of type
+@i<T1>.
 
 !ASIS
 

Questions? Ask the ACAA Technical Agent