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

Differences between 1.5 and version 1.6
Log of other versions for file ai12s/ai12-0113-1.txt

--- ai12s/ai12-0113-1.txt	2014/10/14 03:53:09	1.5
+++ ai12s/ai12-0113-1.txt	2014/11/19 20:58:28	1.6
@@ -1,8 +1,10 @@
-!standard 6.1.1(7/3)                                14-10-06  AI05-0113-1/02
+!standard 6.1.1(7/3)                                14-11-19  AI05-0113-1/03
 !standard 6.1.1(18/3)
+!standard 6.1.1(37/3)
 !standard 6.1.1(38/3)
-!standard 7.3.2(23/3)
 !class binding interpretation 14-05-15
+!status Corrigendum 2015 14-11-19
+!status ARG Approved 7-0-1  14-10-18
 !status work item 14-05-15
 !status received 14-04-25
 !priority Medium
@@ -44,24 +46,24 @@
 
 !wording
 
-Revise 6.1.1(7/3):
+Modify 6.1.1(7/3):
 
    Within the expression for a Pre'Class or Post'Class aspect for a
    primitive subprogram {S} of a tagged type T, a name that denotes a
    formal parameter {(or S'Result)} of type T is interpreted as [having
-   type T'Class] {though it had a (notional) type NT that is a visible
-   formal derived type whose ancestor type is T}. Similarly, a name that
-   denotes a formal access parameter {(or S'Result)} of type access-to-T
-   is interpreted as having type access-to-{NT} [T'Class]. [AARM
-   Redundant: {The result of this interpretation is that the only
-   operations that can be applied to such names are those defined for
-   such a formal derived type.} This ensures that the expression is
-   well-defined for a primitive subprogram of [a]{any} type descended
+   type T'Class] {though it had a (notional) type NT that is a formal
+   derived type whose ancestor type is T, with directly visible primitive
+   operations}. Similarly, a name that denotes a formal access parameter
+   {(or S'Result)} of type access-to-T is interpreted as having type
+   access-to-{NT} [T'Class]. [Redundant: {The result of this interpretation
+   is that the only operations that can be applied to such names are those
+   defined for such a formal derived type.} This ensures that the expression
+   is well-defined for a primitive subprogram of [a]{any} type descended
    from T.]
 
 (In Static Semantics)
 
-Revise 6.1.1(18/3) as follows:
+Modify 6.1.1(18/3) as follows:
 
    If a Pre'Class or Post'Class aspect is specified for a primitive
    subprogram {S} of a tagged type T, {or such an aspect defaults to
@@ -80,7 +82,7 @@
 the parameter names can be different. So we have to talk about corresponding
 parameters without mentioning any names.
 
-   The primitive subprogram S is illegal if it not abtract and the
+   The primitive subprogram S is illegal if it is not abstract and the
    corresponding expression for a Pre'Class or Post'Class aspect would be
    illegal.
 
@@ -88,11 +90,26 @@
 subprograms as they could never be evaluated, and we need to allow such
 expressions to contain calls to abstract subprograms.
 
----
+(In Dynamic Semantics)
 
-Revise 6.1.1(38/3) as follows:
+Modify 6.1.1(37/3):
+   For any subprogram or entry call {S} (including dispatching calls), the
+   checks that are performed to verify specific precondition expressions and
+   specific and class-wide postcondition expressions are determined by those
+   for the subprogram or entry actually invoked. Note that the class-wide
+   postcondition expressions verified by the postcondition check that is part
+   of a call on a primitive subprogram of type T includes all class-wide
+   postcondition expressions originating in any progenitor of T[Redundant:,
+   even if the primitive subprogram called is inherited from a type T1 and
+   some of the postcondition expressions do not apply to the corresponding
+   primitive subprogram of T1]. {Any operations within a class-wide
+   postcondition expression that were resolved as primitive operations of the
+   (notional) formal derived type NT, are in the evaluation of the
+   postcondition bound to the corresponding operations of the type identified
+   by the controlling tag of the call on S. [Redundant: This applies to both
+   dispatching and non-dispatching calls on S.]} 
 
-(In Dynamic Semantics)
+Modify 6.1.1(38/3) as follows:
 
    The class-wide precondition check for a call to a subprogram or entry
    {S} consists solely of checking the class-wide precondition
@@ -101,15 +118,9 @@
    such an expression that were resolved as primitive operations of the
    (notional) formal derived type NT, are in the evaluation of the
    precondition bound to the corresponding operations of the type
-   identified by the controlling tag of the call on S.  [AARM Redundant:
-   This applies to both dispatching and non-dispatching calls on S.]}
+   identified by the controlling tag of the call on S. [Redundant: This
+   applies to both dispatching and non-dispatching calls on S.]}
 
-** TBD: some dynamic semantics rule for class-wide postconditions?? Not
-   sure - RLB.
-
-** TBD - some similar rules are needed for Type_Invariants. I'll wait to find
-out if the above will fly before going further.
-
 !discussion
 
 Consider two nearly identical hierarchies of types. First:
@@ -297,6 +308,95 @@
 routine. There is nothing weaker than True, so if a routine does not have
 an explicit Pre'Class, it can't usefully be given a Pre'Class later in the
 derivation tree. This topic is further explored in AI12-0131-1.
+
+!corrigendum 6.1.1(7/3)
+
+@drepl
+Within the expression for a Pre'Class or Post'Class aspect for a primitive
+subprogram of a tagged type @i<T>, a name that denotes a formal parameter of
+type @i<T> is interpreted as having type @i<T>'Class. Similarly, a name that
+denotes a formal access parameter of type access-to-@i<T> is interpreted as
+having type access-to-@i<T>'Class. This ensures that the expression is
+well-defined for a primitive subprogram of a type descended from @i<T>.
+@dby
+Within the expression for a Pre'Class or Post'Class aspect for a primitive
+subprogram @i<S> of a tagged type @i<T>, a @fa<name> that denotes a formal
+parameter (or @i<S>'Result) of type @i<T> is interpreted as though it
+had a (notional) type @i<NT> that is a formal derived type whose ancestor type
+is @i<T>, with directly visible primitive operations. Similarly, a @fa<name>
+that denotes a formal access parameter (or @i<S>'Result) of type access-to-@i<T>
+is interpreted as having type access-to-@i<NT>. The result of this
+interpretation is that the only operations that can be applied to such
+@fa<name>s are those defined for such a formal derived type. This ensures that
+the expression is well-defined for any primitive subprogram of a type descended
+from @i<T>.
+
+!corrigendum 6.1.1(18/3)
+
+@drepl
+If a Pre'Class or Post'Class aspect is specified for a primitive
+subprogram of a tagged type @i<T>, then the associated expression also
+applies to the corresponding primitive subprogram of each descendant
+of @i<T>.
+@dby
+If a Pre'Class or Post'Class aspect is specified for a primitive
+subprogram @i<S> of a tagged type @i<T>, or such an aspect defaults to
+True, then a corresponding expression also applies to the corresponding
+primitive subprogram @i<S> of each descendant of @i<T>. The @i<corresponding
+expression> is constructed from the associated expression as follows:
+
+@xbullet<References to formal parameters of @i<S> (or to @i<S> itself) are
+replaced with references to the corresponding formal parameters of the
+corresponding inherited or overriding subprogram @i<S> (or to the
+corresponding subprogram @i<S> itself).>
+
+The primitive subprogram @i<S> is illegal if it is not abstract and the
+corresponding expression for a Pre'Class or Post'Class aspect would be
+illegal.
+
+!corrigendum 6.1.1(37/3)
+
+@drepl
+For any subprogram or entry call (including dispatching calls), the checks
+that are performed to verify specific precondition expressions and specific
+and class-wide postcondition expressions are determined by those for the subprogram
+or entry actually invoked. Note that the class-wide postcondition expressions
+verified by the postcondition check that is part of a call on a primitive subprogram
+of type @i<T> includes all class-wide postcondition expressions originating
+in any progenitor of @i<T>, even if the primitive subprogram called
+is inherited from a type @i<T1> and some of the postcondition expressions do
+not apply to the corresponding primitive subprogram of @i<T1>.
+@dby
+For any subprogram or entry call @i<S> (including dispatching calls), the
+checks that are performed to verify specific precondition expressions and
+specific and class-wide postcondition expressions are determined by those for
+the subprogram or entry actually invoked. Note that the class-wide postcondition
+expressions verified by the postcondition check that is part of a call on a
+primitive subprogram of type @i<T> includes all class-wide postcondition
+expressions originating in any progenitor of @i<T>, even if the primitive
+subprogram called is inherited from a type @i<T1> and some of the postcondition
+expressions do not apply to the corresponding primitive subprogram of @i<T1>.
+Any operations within a class-wide postcondition expression that were resolved
+as primitive operations of the (notional) formal derived type @i<NT>, are in
+the evaluation of the postcondition bound to the corresponding operations of
+the type identified by the controlling tag of the call on @i<S>. This applies
+to both dispatching and non-dispatching calls on @i<S>.
+
+!corrigendum 6.1.1(38/3)
+
+@drepl
+The class-wide precondition check for a call to a subprogram or entry consists
+solely of checking the class-wide precondition expressions that apply to the denoted
+callable entity (not necessarily the one that is invoked).
+@dby
+The class-wide precondition check for a call to a subprogram or entry @i<S>
+consists solely of checking the class-wide precondition expressions that apply
+to the denoted callable entity (not necessarily to the one that is invoked).
+Any operations within such an expression that were resolved as primitive
+operations of the (notional) formal derived type @i<NT>, are in the evaluation
+of the precondition bound to the corresponding operations of the type
+identified by the controlling tag of the call on @i<S>. This applies to both
+dispatching and non-dispatching calls on @i<S>.
 
 !ASIS
 

Questions? Ask the ACAA Technical Agent