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