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

--- ai05s/ai05-0247-1.txt	2011/04/30 07:25:44	1.8
+++ ai05s/ai05-0247-1.txt	2011/05/12 22:57:30	1.9
@@ -1,4 +1,4 @@
-!standard 3.4(27/2)                                 11-04-28  AI05-0247-1/08
+!standard 3.4(27/2)                                 11-05-12  AI05-0247-1/09
 !standard 3.9.2(20.2/2)
 !standard 6.1.1(0)
 !standard 7.3.2(0)
@@ -228,15 +228,17 @@
     weaker precondition of the invoked body;
   * add a rule to require overriding if the class-wide precondition is
     weaker than that of the inherited body(s);
-  * change the rules for inherited subprograms such that there always is
-    an implicit body; this implicit body is always equivalent to a call on the
-    concrete body with appropriate postconditions and invariants
+  * change the rules for inherited subprograms such that the effect is always
+    similar to having an implicit body; this implicit body is always equivalent
+    to a call on the concrete body with appropriate postconditions and invariants
     evaluated for the new body.
 
 We need a similar rule to the last for Type_Invariant'Class.
 
 !wording
 
+*** Begin to delete...
+
 Modify 3.4(27) as follows:
 
 For [the execution of] a call on an inherited subprogram, {the execution of the
@@ -297,6 +299,8 @@
   be an explicit overriding of the operation, and then the first bullet would
   apply.)
 
+**** End to delete....
+
 Replace 13.3.2 [from AI05-0145-2] with the following:
 
 [Editor's note: Parts of this wording, including all of the Static Semantics,
@@ -501,8 +505,8 @@
 
           Dynamic Semantics
 
-  If the Assertion_Policy in effect at the point of a subprogram or entry
-  declaration is Check, then upon a call of the subprogram or entry, after
+  If the Assertion_Policy (see 11.4.2) in effect at the point of a subprogram
+  or entry declaration is Check, then upon a call of the subprogram or entry, after
   evaluating any actual parameters, precondition checks are performed as
   follows:
 
@@ -554,7 +558,12 @@
 
   For any subprogram or entry call (including dispatching calls), the specific
   precondition check and the postcondition check that is performed is determined
-  by the those of the subprogram or entry actually invoked.
+  by the those of the subprogram or entry actually invoked. For the purposes of
+  these checks, if the subprogram actually invoked is primitive for some type T and
+  is inherited from some other type, the checks needed are determined as if the
+  body of the of the entity is declared directly as a primitive of type T;
+  in addition, if the subprogram is neither null nor abstract, the specific
+  postcondition of the invoked body is checked.
 
     AARM Ramification: This applies to access-to-subprogram calls, dispatching
     calls, and to statically bound calls. We need this rule to cover statically
@@ -563,12 +572,20 @@
     inheritance only in non-overriding situations seems to be way too complex --
     and we need this rule for dispatching and access-to-subprogram calls
     anyway.]
+
+    We use the "for these purposes" part of the rule to include additional
+    class-wide postconditions from those that apply to the original subprogram.
+    This may happen if the operation is inherited from both a parent and a progenitor,
+    and both the parent operation and progenitor operation have one or more
+    associated postcondition expressions.
+
+    For concrete routines, we require the original specific postcondition to be
+    evaluated as well as the inherited class-wide postconditions in order that
+    the semantics of an explicitly defined wrapper that does nothing but call the
+    original routine is the same as that of an inherited routine.
 
-    For an inherited subprogram, we depend on the definition in 3.4 to provide
-    an implicit body that may have additional postconditions from those that
-    apply to the original subprogram. This may happen if the operation is
-    inherited from a parent and a progenitor, and both the parent operation and
-    progenitor operation have one or more associated postcondition expressions.
+    Note that this rule does not apply to class-wide preconditions; they have
+    their own rules mentioned below.
     End AARM Ramification.
 
   For a call via an access-to-subprogram value, the class-wide precondition
@@ -577,6 +594,10 @@
   or entry consists solely of checking the class-wide preconditions that apply
   to the denoted entity (not necessarily the one that is invoked).
 
+    AARM To Be Honest: The "for these purposes" rule mentioned in the previous
+    item also apply to class-wide preconditions of calls through
+    access-to-subprogram values.
+
     AARM Ramification: For a dispatching call, we are talking about the
     Pre'Class(es) that apply to the subprogram that the dispatching call is
     resolving to, not the Pre'Class(es) for the subprogram that is ultimately
@@ -622,6 +643,30 @@
 
 Move 13.3.3 [from AI05-0146-1] to clause 7.3.2.
 
+Modify 7.3.2(18/3):
+
+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.  For the purposes of
+these checks, if the subprogram actually invoked is primitive for some type T and
+is inherited from some other type, the checks needed are determined as if the
+body of the of the entity is declared directly as a primitive of type T;
+in addition, if the subprogram is neither null nor abstract, the Type_Invariant(s)
+that apply to the parameter types of the invoked body are checked.
+
+    AARM Ramification: We use the "for these purposes" part of the rule to include
+    additional Type_Invariant'Class checks from those that apply to the original
+    subprogram. This may happen if the operation is inherited from both a parent
+    and a progenitor, nd both the parent operation and progenitor operation have
+    defined a Type_Invariant'Class.
+
+    For inherited concrete routines, we require the original Type_Invariant to be
+    evaluated as well as the inherited Type_Invariant'Classes and the current type's
+    Typee_Invariant in order that the semantics of an explicitly defined wrapper that
+    does nothing but call the original routine is the same as that of an inherited
+    routine.
+    End AARM Ramification.
+
 !discussion
 
 This issue originally came up because null procedures are considered the same
@@ -659,10 +704,10 @@
 that the preconditions of an inherited body are checked as the body expects. In
 particular, added class-wide preconditions can weaken the precondition, but it
 is unlikely that an existing body is prepared for such weakening. Since actually
-enforcing the preconditions would violate LSP, we instead require the subprogram
-to be overridden in such cases. That way, any violation of LSP is an explicit
-decision by the programmer and not something that happens implicitly by the
-language.
+enforcing the preconditions of the existing body would violate LSP, we instead
+require the subprogram to be overridden in such cases. That way, any violation
+of LSP via class-wide preconditions is an explicit decision by the programmer
+and not something that happens implicitly by the language.
 
 Note that the requirement is that the class-wide preconditions all fully
 conform. This is a tough requirement that cannot be met for independently