CVS difference for ai05s/ai05-0247-1.txt
--- ai05s/ai05-0247-1.txt 2011/03/23 00:45:42 1.2
+++ ai05s/ai05-0247-1.txt 2011/03/26 06:04:32 1.3
@@ -1,4 +1,4 @@
-!standard 13.3.2(19/3) 11-03-22 AI05-0247-1/02
+!standard 13.3.2(19/3) 11-03-25 AI05-0247-1/03
!reference AI05-0145-2
!class Amendment 11-03-21
!status work item 11-03-21
@@ -9,14 +9,16 @@
!summary
-** TBD **
+A variety of improvements to the model of contract aspects (preconditions,
+postconditions, and type invariants) are made.
!proposal
-The wording of 13.3.2(19/3) makes it clear that the preconditions and postconditions
-(along with type_invariants, these are collectively called contract aspects here)
-that apply to a dispatching call are those of the actual body. However, this rule
-causes logical problems when contract aspects are added by multiple inheritance.
+The wording of 13.3.2(19/3) makes it clear that the preconditions and
+postconditions (along with type_invariants, these are collectively called
+contract aspects here) that apply to a dispatching call are those of the actual
+body. However, this rule causes logical problems when contract aspects are added
+by multiple inheritance.
Consider:
@@ -104,8 +106,6 @@
going to be mighty surprised to get an object that violates its precondition
(since of course it knows nothing about Is_Green).
-[Editor's note: The rest of this is a proposed solution, which may or may not be
-a good idea...]
The key to a solution is to realize that Preconditions and Postconditions are
different and require different rules for dispatching calls. As we noted above,
@@ -154,82 +154,258 @@
rules are as good as any, and they have the advantage of working the same way
for access-to-subprogram calls.
-Thus we need to make two changes:
+
+There are additional problems. While logically preconditions are evaluated at
+the point of a call, the rules given in AI05-0145-2 don't allow that for
+dispatching calls. As noted above, we can fix that by only checking the stronger
+precondition of the denoted subprogram rather than the actual precondition of
+the invoked subprogram. But this is weird for Pre (rather than Pre'Class)
+preconditions; these aren't inherited and aren't necessarily subject to any
+"weakening" rules.
+
+Indeed, it makes more sense to treat Pre as an assertion that occurs at the
+start of the body rather than one that is combined with Pre'Class. As such, it
+provides *additional* requirements for a particular body. This means that Pre
+preconditions will have to be generated in the body (or a wrapper) for
+dispatching calls, while Pre'Class preconditions should only be generated at the
+call site.
+
+
+Finally, the wording given in AI05-0145-2 makes it clear that Pre and Post are
+not inherited. However, nothing is said about what happens to these when a
+subprogram is inherited. With the AI05-0145-2 wording, it appears. Clearly, we
+want to evaluate the Pre and Post values associated with a subprogram when that
+subprogram is inherited.
+
+
+Thus we need to make four changes:
+ * change the rules for evaluation of Pre preconditions such that they are
+ evaluated separately from any Pre'Class preconditions (and have to be True
+ for a call to succeed);
+ * change the rules for calls, such that Pre/Post are always evaluated based on
+ the invoked body;
* change the rules for classwide preconditions of dispatching calls, such that
- the precondition of the call is evaluated, not the weaker precondition of the
- body that is dispatched to;
- * change the rules for inherited subprograms that have Pre'Class; such subprograms
- are always equivalent to a call on the concrete body (with the appropriate
- preconditions evaluated).
+ the precondition of the (denoted) call is evaluated, not the (possibly)
+ weaker precondition of the invoked body;
+ * change the rules for inherited subprograms that have Pre'Class/Post'Class;
+ such subprograms are always equivalent to a call on the concrete body (with
+ the appropriate preconditions/postconditions evaluated for that call).
+
!wording
+Add at the end of 3.10.2(32/2):
+
+If P has one or more class-wide precondition expressions that apply to it, at least
+one of those expressions shall be the enumeration literal True.
+
+AARM Reason: An access to access-to-subprogram type does not have a class-wide
+precondition; that means no such precondition will be checked. This rule
+prevents a routine with a stronger class-wide precondition from being supplied,
+as it would not be enforced.
+
+
+Modify 13.3.2(2-5/3):
+
+Pre
+This aspect [specifies]{defines} a {specific} precondition for a callable
+entity; it shall be specified by an expression, called a {specific} precondition
+expression. {If not specified for an entity, the specific precondition
+expression for the entity is the enumeration literal True.}
+
+Pre'Class
+This aspect [specifies]{defines} a {class-wide} precondition for a callable
+entity and its descendants; it shall be specified by an expression, called a
+{class-wide} precondition expression. {If not specified for an entity, the
+class-wide precondition expression for the entity is the enumeration literal
+True.}
+
+Post
+This aspect [specifies]{defines} a {specific} postcondition for a callable
+entity; it shall be specified by an expression, called a {specific}
+postcondition expression. {If not specified for an entity, the specific
+postcondition expression for the entity is the enumeration literal True.}
+
+Post'Class
+This aspect [specifies]{defines} a {class-wide} postcondition for a callable
+entity and its descendants; it shall be specified by an expression, called a
+{class-wide} postcondition expression. {If not specified for an entity, the
+class-wide postcondition expression for the entity is the enumeration literal
+True.}
+
+Modify 13.3.2(6/3):
+
+The expected type for [a]{any} precondition or postcondition expression is any
+boolean type.
+
+Change 13.3.2(16/3) from:
+
+If one or more precondition expressions apply to a subprogram or entry, and the
+Assertion_Policy in effect at the point of the subprogram or entry declaration
+is Check, then upon a call of the subprogram or entry, after evaluating any
+actual parameters, a precondition check is performed. This begins with the
+evaluation of the precondition expressions that apply to the subprogram or
+entry. If and only if all the precondition expressions evaluate to False,
+Ada.Assertions.Assertion_Error is raised. The order of performing the checks is
+not specified, and if any of the precondition expressions evaluate to True, it
+is not specified whether the other precondition expressions are evaluated. It is
+not specified whether any check for elaboration of the subprogram body is
+performed before or after the precondition check. It is not specified whether in
+a call on a protected operation, the check is performed before or after starting
+the protected action. For a task or protected entry call, the check is performed
+prior to checking whether the entry is open.
+
+to:
+
+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
+evaluating any actual parameters, precondition checks are performed as follows:
+
+* The specific precondition check begins with the evaluation of the specific
+ precondition expression that applies to the subprogram or entry; if the
+ expression evaluates to False, Ada.Assertions.Assertion_Error is raised.
+
+* The class-wide precondition check begins with the evaluation of any class-wide
+ precondition expressions that apply to the subprogram or entry. If and only if
+ all the class-wide precondition expressions evaluate to False,
+ Ada.Assertions.Assertion_Error is raised.
+
+AARM Ramification: The class-wide precondition expressions of the entity itself
+as well as those of any parent or progentitor operations are evaluated, as these
+apply to all descendants.
+
+The order of performing the checks is not specified, and if any of the
+class-wide precondition expressions evaluate to True, it is not specified
+whether the other class-wide precondition expressions are evaluated. It is not
+specified whether any check for elaboration of the subprogram body is performed
+before or after the precondition checks. It is not specified whether in a call
+on a protected operation, the checks are performed before or after starting the
+protected action. For a task or protected entry call, the checks are performed
+prior to checking whether the entry is open.
+
+
+Change 13.3.2(17.3) from:
+
+If one or more postcondition expressions apply to a subprogram or entry, and the
+Assertion_Policy in effect at the point of the subprogram or entry declaration
+is Check, then upon successful return from a call of the subprogram or entry,
+prior to copying back any by-copy in out or out parameters, a postcondition
+check is performed. This consists of the evaluation of the postcondition
+expressions that apply to the subprogram or entry. If any of the postcondition
+expressions evaluate to False, then Ada.Assertions.Assertion_Error is raised.
+The order of performing the checks is not specified, and if one of them
+evaluates to False, it is not specified whether the other postcondition
+expressions are evaluated. It is not specified whether any constraint checks
+associated with copying back in out or out parameters are performed before or
+after the postcondition check.
+
+to:
+
+If the Assertion_Policy in effect at the point of a subprogram or entry
+declaration is Check, then upon successful return from a call of the subprogram
+or entry, prior to copying back any by-copy in out or out parameters, the
+postcondition checks is performed. This consists of the evaluation of the
+specific and class-wide postcondition expressions that apply to the subprogram
+or entry. If any of the postcondition expressions evaluate to False, then
+Ada.Assertions.Assertion_Error is raised. The order of performing the checks is
+not specified, and if any postcondition expression evaluates to False, it is not
+specified whether any other postcondition expressions are evaluated. It is not
+specified whether any constraint checks associated with copying back in out or
+out parameters are performed before or after the postcondition checks.
+
+AARM Ramification: The class-wide postcondition expressions of the entity itself
+as well as those of any parent or progentitor operations are evaluated, as these
+apply to all descendants; in constrast, only the specific postcondition of the
+entity applies.
+
+
Change 13.3.2(19/3) from:
-For a dispatching call or a call via an access-to-subprogram value, the precondition
-or postcondition check performed is determined by the subprogram actually invoked.
-Redundant[Note that for a dispatching call, if there is a Pre'Class aspect that
-applies to the subprogram named in the call, then if the precondition expression for
-that aspect evaluates to True, the precondition check for the call will succeed.]
+For a dispatching call or a call via an access-to-subprogram value, the
+precondition or postcondition check performed is determined by the subprogram
+actually invoked. Redundant[Note that for a dispatching call, if there is a
+Pre'Class aspect that applies to the subprogram named in the call, then if the
+precondition expression for that aspect evaluates to True, the precondition
+check for the call will succeed.]
to:
-For a dispatching call to a subprogram that does not have a Pre'Class specified,
-or a call via an access-to-subprogram value, the precondition or postcondition
-check performed is determined by the subprogram actually invoked. Similarly,
-the postcondition check for all dispatching calls is determined by the subprogram
-actually invoked.
-
-In contrast, the precondition check for a dispatching call to a subprogram that
-does have Pre'Class specified consists solely of checking the Pre'Class expressions
-that apply to the subprogram.
-
-AARM Ramification: We are talking about the Pre'Class that applies to the
-subprogram that the dispatching call is resolving to call, not the Pre'Class for
-the subprogram that is ultimately dispatched to.
-
-AARM Implementation Note: These rules imply that logically, preconditions of
-routines that have Pre'Class specified and might be called with a dispatching
-call must be checked at the point of call.
-Preconditions of other routines that might be called with a dispatching call
-must be checked inside of the subprogram body (possibly in a wrapper). It's
-possible for both conditions to be necessary
-for routines that are inherited from multiple ancestors (in that case, the
-check at the call site necessarily be the same or stronger than the one inside
-of the routine). In contrast, the postcondition checks always need to be checked
-inside the body of the routine.
+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.
+
+AARM Ramification: This applies to access-to-subprogram calls, dispatching calls,
+and to statically bound calls. We need this rule to cover statically bound calls
+as well, as Pre preconditions and Post postconditions are not inherited, but the
+subprogram might be. [Editor's note: Wording to define aspect 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.]
+
+In contrast, the class-wide precondition check for a call to a
+subprogram or entry consists solely of checking the class-wide preconditions that
+apply to the denoted entity (not necessarily the one that is invoked).
+
+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 dispatched to. For a statically
+bound call, these are the same; for an access-to-subprogram (which has no
+class-wide preconditions), no class-wide precondition check is needed at all.
+
+AARM Implementation Note: These rules imply that logically, class-wide preconditions
+of routines must be checked at the point of call. Specific preconditions that
+might be called with a dispatching call or via an access-to-subprogram value
+must be checked inside of the subprogram body. In contrast, the postcondition
+checks always need to be checked inside the body of the routine. Of course,
+an implementation can evaluate all of these at the point of call for statically
+bound calls if the implementation uses wrappers for dispatching bodies and for
+'Access values.
End AARM Implementation Note.
-Notwithstanding what this standard says elsewhere, an inherited subprogram that
-has a specified Pre'Class, Post'Class, or Type_Invariant'Class (see 13.3.3) and
-is primitive for a type that has one or more progenitors is equivalent to an
-overriding subprogram S whose body consists of:
+Notwithstanding what this standard says elsewhere, an inherited subprogram S
+(or multiple conformant inherited subprograms) that has one or or more
+class-wide precondition or postcondition expressions that apply to S,
+or has a specified Type_Invariant'Class (see 13.3.3),
+that is not explicitly overridden, and that is primitive for a type that has one
+or more progenitors is equivalent to an overriding subprogram S whose body consists of:
* The null statement, if all of the inherited subprograms are null subprograms;
* A call on the parent subprogram, with all of the parameters the same as
- the parameters to S (possibility with appropriate type conversions).
-If there are multiple conformant subprograms S, there is only one overriding
-subprogram S created.
+ the parameters to S (possibly with appropriate type conversions).
+If a subprogram renaming overrides one or more inherited subprograms, the renaming
+is equivalent of an subprogram whose body calls the renamed subprogram, with all
+of the parameters the same as the parameters to S (possibly with appropriate type
+conversions).
+
AARM Ramification: We really mean equivalent here! The call on the parent
subprogram will evaluate preconditions as needed. And a dispatching call will
-call this body, rather than that of one of the inherited subprograms.
+call this body, rather than that of one of the inherited subprograms. Note that
+if the routines are not all null, then the subprogram inherited for the parent
+type must be concrete (not abstract or null), so that is the one we want to call.
+
+AARM Discussion: Only one implicit overriding subprogram is created for a single
+set of homoegraphs.
-AARM Reason: This rule eliminates three problems: (1) the issue that two
+AARM Reason: These rules eliminates four problems: (1) the issue that two
null subprograms (one of which is chosen for dispatching arbitrarily by
3.9.2(20.3/3)) may not be equivalent at runtime; (2) "counterfeiting" problems
that arise because adding an interface precondition to the mix weakens the
-precondition of the inherited routine (in this case, we need to enforce
-the precondition of the actual body, else it might not be true when the
-call is made -- which would be bad); (3) problems that arise because
-postconditions and invariants added by an interface would not be enforced
-on a inherited routine (it does not know about any such contracts).
+class-wide precondition of the inherited routine (in this case, we need to
+enforce the class-wide precondition of the actual body, else it might not be
+true when the call is made -- which would be bad); (3) problems that arise
+because postconditions and invariants added by an interface would not be
+enforced on a inherited routine (it does not know about any such contracts);
+(4) problems with the "wrong" class-wide precondition being enforced
+for an overriding rename of a routine that has it's own class-wide
+precondition.
[Editor's note: We do not need to talk about this in single inheritance
-cases because the contract aspects cannot change in that case. We do not
-need to talk about this unless there is a 'Class aspect involved because
-other aspects (Pre, Post, Type_Invariant) are not inherited. Thus we do
-not talk about it as it appears to change the dispatching model (even though
-it would have no effect on compilers in these other cases).]
+cases (other than the renames one) because the contract aspects cannot change in
+that case. We do not need to talk about this unless there is a class-wide aspect
+involved because other aspects (Pre, Post, Type_Invariant) are not inherited.
+We could have made this apply to all inheritance of routines that can have
+class-wide aspects, but we didn't do that as that would appears to change the
+dispatching model (even though compilers would not need to change in the
+absence of contract aspects).]
!discussion
@@ -241,10 +417,6 @@
general problems of inheritance.
-Note that we do not change any rules for evaluation of any contract aspects on
-non-dispatching calls.
-
-
In general, we want to be able to generate preconditions at call sites, since
that is the only way that they can be eliminated by optimization or other forms
of proof. Similarly, we want to be able to generate postconditions inside of
@@ -256,12 +428,36 @@
site. Doing so elsewhere is in general an optimization.
-We have to be careful that the absence of a Pre'Class routine is not treated as
-"True", as it would be impossible to weaken that further. We do that by treating
-dispatching calls as those to routines with unknown preconditions.
+The change to separate Pre from Pre'Class introduces additional problems with
+renames and 'Access. Since renaming can change the dispatching status of a
+subprogram (from dispatching to statically bound, or the reverse), it introduces
+some interesting problems.
+
+We also would like access-to-subprogram to work the same way as a dispatching
+call. But that only works if the designated subprogram does not have any Pre'Class
+(as we don't have any such preconditions on access-to-subprogram types).
+
+We fix these both by including Pre'Class in conformance checking, such that
+subprograms don't match if the Pre'Class precondition(s) that apply to the
+subprogram are not equivalent (fully conformant). But we don't want a condition
+this strong for overriding (we want to be able to weaken the precondition
+with additional Pre'Class items) [although I cannot think of
+any case in practice when a weaker precondition would be what you want - RLB],
+so this rule does not apply to overriding.
+We could have solved the Pre/Post inheritance problem by changing the model of
+inheritance in Ada to always generate an implicit body as in the wording proposed
+at the end of the AI. As well as solving that problem, it also would simplify the
+model of dispatching a lot (there would always be a body defined for each type,
+there would never need to be any looking at parents or progenitors for bodies).
+But this would be a substantial change in the presentation of Ada (even though
+it is unlikely that compilers would have to actually generate such bodies in most
+cases). As such it seems like a likely way to inject new bugs into the language --
+and thus it was rejected.
+
+
!corrigendum 13.3.2(0)
@dinsc
@@ -1594,6 +1790,41 @@
****************************************************************
+From: Tucker Taft
+Sent: Tuesday, March 22, 2011 8:51 PM
+
+I am pretty sure there is a restriction of 'Class aspects to tagged types or
+dispatching subprograms. Ah yes, last legality rule of AI-183:
+
+ If the aspect_mark includes 'Class, then the associated
+ entity shall be a tagged type or a primitive subprogram
+ of a tagged type.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, March 23, 2011 8:24 PM
+
+OK, good to find out that it is covered. But I have to admit I never thought to
+look there, given that there are only a handful of such aspects and as such I
+didn't expect there to be a blanket rule existing only for them. Thus, I'm not
+sure that such a blanket rule is a great idea. Maybe there needs to be an AARM
+note in 13.3.2 and 13.3.3 mentioning this rule.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, March 23, 2011 10:05 PM
+
+It turns out that 13.3.3(6/3) repeats this rule, while there is no similar text
+in 13.3.2. I marked the text in 13.3.3 as redundant (presuming no other change),
+and added an AARM note to 13.3.2 for future readers that are as confused as I
+was. I suspect that either the text should be deleted from 13.3.3 or something
+similar added to 13.3.2 -- but I'll wait for someone other than me to make a
+formal editorial change request to that effect.
+
+****************************************************************
+
From: Randy Brukardt
Sent: Tuesday, March 22, 2011 5:53 PM
@@ -1677,5 +1908,1341 @@
call (2), even though it will be executed.]
If we made this sort of thing illegal, this could not happen.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, March 22, 2011 6:10 PM
+
+> !wording
+>
+> Change 13.3.2(19/3) from:
+>
+> For a dispatching call or a call via an access-to-subprogram value,
+> the precondition or postcondition check performed is determined by the
+> subprogram actually invoked.
+> Redundant[Note that for a dispatching call, if there is a Pre'Class
+> aspect that applies to the subprogram named in the call, then if the
+> precondition expression for that aspect evaluates to True, the
+> precondition check for the call will succeed.]
+>
+> to:
+>
+> For a dispatching call to a subprogram that does not have a Pre'Class
+> specified, or a call via an access-to-subprogram value, the
+> precondition or postcondition check performed is determined by the
+> subprogram actually invoked. Similarly, the postcondition check for
+> all dispatching calls is determined by the subprogram actually
+> invoked.
+>
+> In contrast, the precondition check for a dispatching call to a
+> subprogram that does have Pre'Class specified consists solely of
+> checking the Pre'Class expressions that apply to the subprogram.
+
+What about the "Pre" aspect? Is this meant to imply that if there is a
+Pre'Class aspect specified, then the Pre aspect is ignored?
+
+Also, when you say the "the Pre'Class expressions that apply to the subprogram"
+do you mean the subprogram denoted by the call prefix, or do you mean the
+subprogram actually invoked? The wording seems ambiguous.
+
+Finally, what are the implications that only the Pre'class known to the caller
+be checked? If one of the Pre'Class expressions that applies to the subprogram
+actually invoked is True, must we still raise an Assertion_Error if all of the
+expressions that apply to the denoted subprogram evaluate to False?
+
+> AARM Ramification: We are talking about the Pre'Class that applies to
+> the subprogram that the dispatching call is resolving to call, not the
+> Pre'Class for the subprogram that is ultimately dispatched to.
+
+I believe this needs to be made clearer in the normative wording.
+An AARM note seems inadequate. The word "denote" could be used to emphasize the
+compile-time denoted subprogram, rather than the run-time invoked subprogram.
+
+> AARM Implementation Note: These rules imply that logically,
+> preconditions of routines that have Pre'Class specified and might be
+> called with a dispatching call must be checked at the point of call.
+> Preconditions of other routines that might be called with a
+> dispatching call must be checked inside of the subprogram body
+> (possibly in a wrapper). It's possible for both conditions to be
+> necessary for routines that are inherited from multiple ancestors (in
+> that case, the check at the call site necessarily be the same or
+> stronger than the one inside of the routine).
+
+I don't understand the "preconditions of other routines". What does that mean?
+Is this the "Pre" aspects as opposed to the "Pre'Class" aspects?
+
+> In contrast, the postcondition checks always need to be
+> checked
+> inside the body of the routine.
+> End AARM Implementation Note.
+>
+> Notwithstanding what this standard says elsewhere, an inherited
+> subprogram that has a specified Pre'Class, Post'Class, or
+> Type_Invariant'Class (see 13.3.3) and
+
+that
+
+> is primitive for a type that has one or more progenitors is equivalent
+> to an overriding subprogram S whose body consists of:
+> * The null statement, if all of the inherited subprograms are null
+> subprograms;
+> * A call on the parent subprogram, with all of the parameters the same as
+> the parameters to S (possibility with appropriate type conversions).
+> If there are multiple conformant subprograms S, there is only one
+> overriding subprogram S created....
+
+Is this needed? It feels awfully mechanistic. Can't we accomplish this some
+other way?
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, March 22, 2011 9:29 PM
+
+> The important point is whether we want to enforce this with Legality
+> Rules, or just make it the model implicitly.
+>
+> I should note that we don't enforce it with Legality Rules, some
+> subprograms can be called both ways (from dispatching calls that
+> expect the body to check preconditions, and from dispatching calls are
+> required to check the precondition themselves).
+
+The above parenthetical comment confuses me. Should one of those said
+"non-dispatching calls"?
+
+> ... Which means that you might have to generate code in both places
+> (ugh). For instance:
+>
+> package Pack1 is
+> type T1 is tagged private;
+> function Is_Valid (Obj : T1) return Boolean;
+> procedure P3 (Obj : in T1)
+> with Pre => Is_Valid (Obj);
+> private
+> ...
+> end Pack1;
+>
+> package Pack2 is
+> type I2 is interface;
+> function Is_Green (Obj : I2) return Boolean is abstract;
+> procedure P3 (Obj : in I2) is null
+> when Pre'Class => Is_Green (Obj);
+> end Pack2;
+>
+> with Pack1, Pack2;
+> package Pack3 is
+> type T3 is new Pack1.T1 and Pack2.I2 with private;
+> overriding
+> function Is_Green (Obj : T3) return Boolean;
+> -- P3 is inherited from Pack1.P3.
+> private
+> ...
+> end Pack3;
+>
+> with Pack1, Pack2, Pack3;
+> procedure Main is
+> procedure Do_It1 (Obj : in Pack1.T1'Class) is
+> begin
+> Obj.P3; -- (1)
+> end Do_It1;
+> procedure Do_It2 (Obj : in Pack2.T2'Class) is
+> begin
+> Obj.P3; -- (2)
+> end Do_It2;
+> O3 : P3.T3;
+> begin
+> Do_It1 (O3);
+> Do_It2 (O3);
+> end Main;
+>
+> Call (1) is to a routine with an ordinary Precondition, so the body
+> always checks the precondition. Call (2) is to a routine with a
+> Pre'Class precondition, but the check is at the call site. But of
+> course these call the same body, so the body must have the code even
+> for call (2). [That code can never fail for call (2), even though it
+> will be executed.]
+
+I'm losing you. What do you mean by "the body must have the code even for call
+(2)"?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, March 23, 2011 9:37 PM
+
+> > For a dispatching call to a subprogram that does not have a
+> > Pre'Class specified, or a call via an access-to-subprogram value,
+> > the precondition or postcondition check performed is determined by
+> > the subprogram actually invoked. Similarly, the postcondition check
+> > for all dispatching calls is determined by the subprogram actually
+> > invoked.
+> >
+> > In contrast, the precondition check for a dispatching call to a
+> > subprogram that does have Pre'Class specified consists solely of
+> > checking the Pre'Class expressions that apply to the subprogram.
+>
+> What about the "Pre" aspect? Is this meant to imply that if there is
+> a Pre'Class aspect specified, then the Pre aspect is ignored?
+
+Yes, but not because of any explicit intent, but rather the way that Pre works.
+Pre is "or"ed with all of the other Pre'Class aspects that are inherited. Since
+we're using a stronger precondition on such calls than that of the invoked
+subprogram, this necessarily means that any precondition of the body must
+succeed. Thus there is no need to evaluate Pre in such cases; if the compiler
+can prove that all calls are either this kind of dispatching calls or statically
+bound calls, it can always generate the preconditions at the call site and do no
+evaluation in the body. That seems like a good thing.
+
+I was wondering whether we should even allow this mixing; that's covered in my
+other e-mail which I see has a separate answer from you so I'll give it a
+separate answer as well.
+
+> Also, when you say the "the Pre'Class expressions that apply to the
+> subprogram" do you mean the subprogram denoted by the call prefix, or
+> do you mean the subprogram actually invoked?
+> The wording seems ambiguous.
+
+The former. I thought that it is necessary to explicitly talk about the dynamic
+meaning of subprogram explicitly; anything else is necessarily static. But I
+agree that it is not that clear, so if there is some better wording available,
+we should use it.
+
+> Finally, what are the implications that only the Pre'class known to
+> the caller be checked? If one of the Pre'Class expressions that
+> applies to the subprogram actually invoked is True, must we still
+> raise an Assertion_Error if all of the expressions that apply to the
+> denoted subprogram evaluate to False?
+
+Yes. The intent is that the stronger precondition of the call is what is
+checked; that avoids "counterfeiting". If we want to be able to do analysis at
+the call site (and code generation!), we have to be able to know what
+preconditions and postconditions apply to that call. For postconditions, these
+are "weaker" (or the same), so we need no special rules. But for preconditions,
+these can be "stronger" than those of the body; in order to have any chance to
+generate these at the call site, we have to be able to evaluate the "stronger"
+precondition rather than the potentially weaker one of the called body.
+
+I considered making this a permission rather than a requirement, but that only
+seemed to make it harder for users to figure out what preconditions are
+enforced.
+
+Beyond that, this makes perfect sense (to me at least): the only precondition
+the caller can know about for a dispatching call is the Pre'Class that applies
+to the (statically) resolved subprogram. It is the one that a caller has to
+conform to have a provably correct program. That being the case, why shouldn't
+we also enforce it??
+
+Note that this rule change is sort of an optimization; it is intended to allow
+code generation for preconditions at the call site of dispatching calls and also
+to enforce the intended (Eiffel-like) model for subprograms that have Pre'Class
+aspects. We could live without it, but doing so would pretty much eliminate the
+ability of compilers to optimize preconditions for dispatching calls -- that
+seems bad to me. (This is the same reason that we go out of are way to allow
+postconditions to be generated inside of a subprogram body -- mostly so that the
+compiler can prove that they are already true and eliminate the checks.)
+
+> > AARM Ramification: We are talking about the Pre'Class that applies
+> > to the subprogram that the dispatching call is resolving to call,
+> > not the Pre'Class for the subprogram that is ultimately dispatched to.
+>
+> I believe this needs to be made clearer in the normative wording.
+> An AARM note seems inadequate. The word "denote" could be used to
+> emphasize the compile-time denoted subprogram, rather than the
+> run-time invoked subprogram.
+
+OK, I'll make an attempt to clarify up this wording. Humm, 3.9.2 uses "denotes
+the declaration of a dispatching operation". But I can't quite find a way to
+work "denotes" into "For a dispatching call to a subprogram that does not have a
+Pre'Class specified,".
+
+"For a dispatching call to a denoted subprogram that does not have a Pre'Class
+specified,"
+
+doesn't make much sense.
+
+"For a dispatching call to a subprogram that does not have a Pre'Class specified
+for the denoted subprogram,"
+
+is right but way too redundant. But I can't think of anything better. I did add
+a parenthetical remark to the last paragraph:
+
+ In contrast, the precondition check for a dispatching call to a subprogram
+ that does have Pre'Class specified for the denoted subprogram consists solely
+ of checking the Pre'Class expressions that apply to the denoted subprogram
+ (not necessarily the one that is invoked).
+
+> > AARM Implementation Note: These rules imply that logically,
+> > preconditions of routines that have Pre'Class specified and might be
+> > called with a dispatching call must be checked at the point of call.
+> > Preconditions of other routines that might be called with a
+> > dispatching call must be checked inside of the subprogram body
+> > (possibly in a wrapper). It's possible for both conditions to be
+> > necessary for routines that are inherited from multiple ancestors
+> > (in that case, the check at the call site necessarily be the same or
+> > stronger than the one inside of the routine).
+>
+> I don't understand the "preconditions of other routines".
+> What does that mean? Is this the "Pre" aspects as opposed to the
+> "Pre'Class" aspects?
+
+Both "Pre" aspects, and "Pre'Class" aspects added further down the inheritance
+tree. The precondition of a dispatching call is that which is known at the call
+site, period. There is no advantage to weakening here, while there might be for
+statically bound calls (or dispatching calls whose root is higher up the tree).
+
+I gave the example that led to this in my other note, the one that confused you
+so. I'll try to explain that again when I answer that one.
+
+> > In contrast, the postcondition checks always need to be checked
+> > inside the body of the routine.
+> > End AARM Implementation Note.
+> >
+> > Notwithstanding what this standard says elsewhere, an inherited
+> > subprogram that has a specified Pre'Class, Post'Class, or
+> > Type_Invariant'Class (see 13.3.3) and
+>
+> that
+>
+> > is primitive for a type that has one or more progenitors is
+> > equivalent to an overriding subprogram S whose body consists of:
+> > * The null statement, if all of the inherited subprograms are
+> > null subprograms;
+> > * A call on the parent subprogram, with all of the parameters
+> > the same as
+> > the parameters to S (possibility with appropriate type conversions).
+> > If there are multiple conformant subprograms S, there is only one
+> > overriding subprogram S created....
+>
+> Is this needed? It feels awfully mechanistic. Can't we accomplish
+> this some other way?
+
+Maybe, but I doubt it will help much. Everything I thought of always led back
+here. Note that this rule is required to fix the three problems outlined in the
+AARM Reason note; some solution to these problems is required. I thought that
+one rule to fix all three was preferable to inventing three separate rules that
+really complicate things.
+
+As a reminder, the AARM note says:
+
+AARM Reason: This rule eliminates three problems: (1) the issue that two null
+subprograms (one of which is chosen for dispatching arbitrarily by
+3.9.2(20.3/3)) may not be equivalent at runtime; (2) "counterfeiting" problems
+that arise because adding an interface precondition to the mix weakens the
+precondition of the inherited routine (in this case, we need to enforce the
+precondition of the actual body, else it might not be true when the call is made
+-- which would be bad); (3) problems that arise because postconditions and
+invariants added by an interface would not be enforced on a inherited routine
+(it does not know about any such contracts).
+
+All three problems occur because of dispatching that calls inherited routines
+that have a different view of the preconditions, postconditions, and invariants
+that apply to them than an otherwise identical explicitly declared routine.
+Besides the logical problems that arise, we also have a problem simply because
+an explicitly declared routine works differently than an inherited one. That
+seems bad on its face, even ignoring the other problems.
+
+It immediately was obvious to me that there is no problem with explicitly
+declared routines. That led to my original idea, which was simply to require
+overriding for the problem cases - that is a nice, simple solution. That would
+be a Legality Rule something like:
+
+If the set of Pre'Class or Post'Class or Type_Invariant'Class aspects that would
+apply to a call of an inherited subprogram is different than the set of
+corresponding aspects of a call to the parent subprogram, then the subprogram
+requires overriding.
+
+But this rule is difficult to define properly; we don't want to talk about
+"calls", really, and we don't want confusion about the implicit inherited
+subprogram as opposed to the subprogram that was inherited from, and it is hard
+to define "different" very well. (Since this is a Legality Rule that requires
+the programmer to do something, we don't want it to apply unless we really need
+it; thus we would want to be able to prevent it from applying when the same
+Pre'Class comes from multiple parents - to take one example.)
+
+The difficulty of defining this, along with the simple fact that it requires
+people to write overriding subprograms (containing calls that they could easily
+make a mistake in) just to get the preconditions right caused me to look
+elsewhere.
+
+Since it is easy to define what the body of such a subprogram looks like, and
+ensuring that it exists for both contract aspects and for dispatching purposes
+is needed to fix the problems (in a straightforward manner), I decided to write
+the proposed rules.
+
+The best way (IMHO) to simplify these rules is to make the proposed rules apply
+to *all* inherited primitive routines of tagged types -- that is, there is (for
+language rule purposes) an explicit body (defined as I proposed above) for
+*every* such body. Then, we could get rid of almost all of 3.9.2(20-20.3) --
+only the first bullet is even possible. Compilers still can share bodies as they
+do now (except in the pre/post cases of course) -- only the language definition
+is changed. In that case, this rule would move somewhere else in the Standard
+(3.9.2??). I didn't do this because it is a lot of language change for what is
+clearly a corner case.
+
+The alternative of trying to define these properly in place is just too hard
+IHMO. The wording for each of these cases would be very complex. The problem
+cases come up when there are multiple inherited routines with different
+preconditions, postconditions, and the like. In those cases, the effective
+aspect is the combined one. I can't figure out how to talk about that
+combination, because you cannot talk about "the" inherited subprogram; there is
+more than one.
+
+And the rules themselves are complex. Specifically, the precondition for an
+inherited routine called via a dispatching call is the Pre'Class of the
+subprogram denoted by the call "and"ed with the actual precondition of the
+parent routine. (These are often the same, but don't have to be when interfaces
+are involved -- they can be completely disjoint in that case.) This is what you
+would get with an explicit body, and it is best that the inherited routines work
+the same way.
+
+The precondition of a statically bound call to such an inherited subprogram is
+(effectively) the precondition of the parent routine. OTOH, the postcondition of
+a statically bound call is the postcondition of the parent routine "and"ed with
+any postconditions inherited from other routines.
+
+And on and on and on...
+
+Ideas welcome, of course.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, March 23, 2011 9:52 PM
+
+...
+> > The important point is whether we want to enforce this with Legality
+> > Rules, or just make it the model implicitly.
+> >
+> > I should note that we don't enforce it with Legality Rules, some
+> > subprograms can be called both ways (from dispatching calls that
+> > expect the body to check preconditions, and from dispatching calls
+> > are required to check the precondition themselves).
+>
+> The above parenthetical comment confuses me. Should one of those said
+> "non-dispatching calls"?
+
+No. If you recall from the rules I previously proposed, there are two kinds of
+dispatching calls:
+
+If the denoted subprogram has one or more Pre'Class expressions specified, then
+the precondition expressed by those expressions (only) is evaluated (for
+dispatching calls). These conform to the Eiffel-like model, so for the sake of
+discussion, let's call them "Eiffel-like contract dispatching calls".
+
+OTOH, if the denoted subprogram does not have a Pre'Class expressions specified,
+then the precondition that is evaluated is that of the invoked subprogram; the
+precondition can be anything, and reasoning about it at the call site is not
+possible. Let's call these "Ad-hoc contract dispatching calls."
+
+The question I had was whether we should enforce a separation of these two
+models of contracts and calls. If we don't do that, it is possible to call the
+same subprogram from both an "Eiffel-like contract dispatching call" and a
+"ad-hoc contract dispatching call". As in the example that follows...
+
+> > ... Which means that you might have to generate code in both places
+> > (ugh). For instance:
+> >
+> > package Pack1 is
+> > type T1 is tagged private;
+> > function Is_Valid (Obj : T1) return Boolean;
+> > procedure P3 (Obj : in T1)
+> > with Pre => Is_Valid (Obj);
+> > private
+> > ...
+> > end Pack1;
+> >
+> > package Pack2 is
+> > type I2 is interface;
+> > function Is_Green (Obj : I2) return Boolean is abstract;
+> > procedure P3 (Obj : in I2) is null
+> > when Pre'Class => Is_Green (Obj);
+> > end Pack2;
+> >
+> > with Pack1, Pack2;
+> > package Pack3 is
+> > type T3 is new Pack1.T1 and Pack2.I2 with private;
+> > overriding
+> > function Is_Green (Obj : T3) return Boolean;
+> > -- P3 is inherited from Pack1.P3.
+> > private
+> > ...
+> > end Pack3;
+> >
+> > with Pack1, Pack2, Pack3;
+> > procedure Main is
+> > procedure Do_It1 (Obj : in Pack1.T1'Class) is
+> > begin
+> > Obj.P3; -- (1)
+> > end Do_It1;
+> > procedure Do_It2 (Obj : in Pack2.T2'Class) is
+> > begin
+> > Obj.P3; -- (2)
+> > end Do_It2;
+> > O3 : P3.T3;
+> > begin
+> > Do_It1 (O3);
+> > Do_It2 (O3);
+> > end Main;
+> >
+> > Call (1) is to a routine with an ordinary Precondition, so the body
+> > always checks the precondition. Call (2) is to a routine with a
+> > Pre'Class precondition, but the check is at the call site. But of
+> > course these call the same body, so the body must have the code even
+> > for call (2). [That code can never fail for call (2), even though it
+> > will be executed.]
+>
+> I'm losing you. What do you mean by "the body must have the code even
+> for call (2)"?
+
+(1) is an ad-hoc dispatching call; it requires that the precondition (Is_Valid
+(Obj) or Is_Green (Obj)) is evaluated within the invoked subprogram.
+
+(2) is an Eiffel-like dispatching call; it requires that the precondition
+(Is_Green (Obj)) is evaluated at the call site. It does not need to evaluate any
+other precondition, and shouldn't evaluate a precondition in the body. Luckily,
+evaluating a precondition in the body has to be harmless -- the precondition of
+the call has to be part of the larger precondition, and whatever part it is must
+be "or"ed (and is True), so the rest is irrelevant -- but it still wastes time.
+
+It should noted that this scenario would happen if P3 for T1 had no Pre at all,
+so this is a fairly likely case in practice.
+
+> > If we made this sort of thing illegal, this could not happen.
+
+I hope this explains what I'm talking about here.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, March 23, 2011 11:00 PM
+
+> Yes, but not because of any explicit intent, but rather the way that
+> Pre works. Pre is "or"ed with all of the other Pre'Class aspects that
+> are inherited. Since we're using a stronger precondition on such calls
+> than that of the invoked subprogram, this necessarily means that any
+> precondition of the body must succeed. Thus there is no need to
+> evaluate Pre in such cases; if the compiler can prove that all calls
+> are either this kind of dispatching calls or statically bound calls,
+> it can always generate the preconditions at the call site and do no
+> evaluation in the body. That seems like a good thing. ...
+
+I thought we were discussing the possibility of treating Pre'Class and Pre completely
+independently. That is Pre'Class is "or"ed with other Pre'Class aspects, but the
+Pre aspect is not "or"ed with anything. In other words, the Pre aspect is *always*
+checked. The Pre'Class aspect can only be weakened, thanks to the "or"-ing rules.
+The Pre aspect has no such guarantee -- it acts almost exactly like an Assert pragma
+placed immediately after the "is" of the body.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, March 23, 2011 11:52 PM
+
+I've only considered such a separation at compile-time (via Legality Rules). That is,
+a given subprogram can only have Pre or Pre'Class, never both. But since that wasn't
+necessary in order to define the dynamic semantics of calls and especially the fixes
+to the bugs that triggered this AI, I just defined that and was continuing to explore
+whether or not the Legality Rules were a good idea.
+
+As far as just treating them independently at runtime, that is a whole different kettle
+of fish. That effectively means that the Pre and Pre'Class aspects are "and"ed together
+-- which is a big change in the model. I suspect that it might in fact be a *better*
+model, but it means starting over completely in thinking about all of these examples of
+inheritance and the like.
+
+One thing that immediately comes to mind is how Pre'Class is treated vis-a-vis
+access-to-subprogram. One of the advantages of the model that I proposed is that
+access-to-subprogram is treated the same way as a similar dispatching call (one without
+a Pre'Class aspect). I don't see how that could work in the model you are suggesting;
+since Pre'Class would be unknown (and thus True), it would be ignored on any
+access-to-subprogram call (at least unless we allowed Pre'Class on access-to-subprogram
+types). Sounds like a nasty hole.
+
+I'm presuming that in this model, the Pre'Class aspects are "or"ed together, then the
+result is "and"ed with Pre. If there is no Pre'Class, it is treated as True.
+
+I'd hope that we continue to have the Pre'Class model as I laid out in my wording proposal
+(that we use the Pre'Class of the statically identified subprogram, which is necessarily
+the same or stronger than the Pre'Class of the invoked body). And then Pre of the invoked
+body would be evaluated.
+
+Please tell me if I understand your model correctly.
+
+I'll definitely have to think about this some more.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, March 24, 2011 1:29 AM
+
+I think this discussion focuses too much on technical aspects, before the
+principles. So here is my view of what this all means.
+
+Pre'Class and Post'Class are the enforcement of the LSP. i.e., if B "is an" A,
+then every input acceptable to an A must be accepted by a B, and every output
+produced by a B must be something that could have been produced by an A. Hence
+the "or" and "and" semantics.
+
+Pre-conditions are a contract imposed on the caller. A failure of a
+pre-condition is an error made by the caller. Therefore, it seems logical to
+check it at the caller's site.
+
+Post-Conditions are a promise made by the callee. Failure of a post-condition is
+a flaw in the callee, therefore it seems logical to check it in the body - even
+maybe at the place of the return statement, which would give the possibility to
+have an exception handler in case of a failure. (AFAIR, we never discussed the
+place of the check in the light of who could handle the exception).
+
+Pre is totally different. It is a special check of a condition that must hold
+for a particular subprogram, not transmitted to any one else. I agree with Tuck
+that it is basically like an Assert just after the "is" of the body. It's like
+explicitely checking for some special value (or combination of values) in the
+body of the subprogram. I even think the latter is preferable, since you can
+choose which exception is raised, so I see little value in Pre (except than the
+test is performed before elaborating the declarative part of the callee).
+
+In short, my model implies:
+- Pre'class checked at the call site
+- Pre, Post, and Post'class checked in the body.
+
+(Note that the checking of Pre in the body would take care of the "anding" of
+the preconditions that worried Randy).
+
+As far as optimization is concerned, the compiler can assume that all Post and
+Post'Class hold in determining if checks for Pre'Class can be eliminated.
+Nothing can be done for Pre (as for an explicit check, or an Assert in the
+body).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 2:06 AM
+
+I'm glad to hear from someone else in this discussion.
+
+I had thought we'd already done the first principles discussion that you lay out
+above; I've just been trying to fix the bugs. Apparently all of the previous
+discussion is junk (since that previous model has been rejected).
+
+Anyway, I assume that you are talking about dispatching calls in most of the
+above. Pre and Pre'Class are equivalent (except for the "and"!) for statically
+bound calls. Specifically, you surely can generate Pre at the call point, and
+optimize it. It would be pretty bad if you couldn't. Especially as you can't
+give Pre'Class on anything other than primitives of tagged types (I think I want
+call-site preconditions on other subprograms!).
+
+The current rules proposal does not allow any Pre/Post exceptions to be handled
+by the body, and I think that is exactly right. Your assertion that we never
+discussed it is wrong; we discussed it ad-nausem at the Tallehasse meeting (I
+think you missed that one, probably why you don't know that). 13.3.2(18/3) is
+pretty clear that this is the intent. The reason is that for statically bound
+cases, we ought to let the compiler have the freedom to generate the checks
+wherever it wants (in the body or at the call site) - in order to maximize the
+possibilities for optimization/proof. Dispatching calls and access-to-subprogram
+are different, of course.
+
+I can't tell from your discussion as to exactly which Pre'Class you expect to
+enforce at the call site of a dispatching call. I've proposed that it is the
+statically known one, which by definition is stronger than the Pre'Class for the
+actually invoked body. Is that what you are intending?? (It definitely isn't
+possible to generate the code at the call site unless we specify this.)
+
+Also, it would be helpful if you could explain in your model what you expect to
+happen for calls through access-to-subprogram values to subprograms that have
+Pre'Class preconditions. This seems to have to work differently than dispatching
+calls, which is uncomfortable.
+
+Finally, none of this has any effect on the actual bug fixes; the rules that
+Tucker found too "mechanistic". Those rules are needed to fix bugs that only
+involve Pre'Class (and Post'Class and Type_Invariant'Class); nothing about
+changing the handling of Pre has anything to do with that.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 8:05 AM
+
+> As far as just treating them independently at runtime, that is a whole
+> different kettle of fish. That effectively means that the Pre and
+> Pre'Class aspects are "and"ed together -- which is a big change in the
+> model. I suspect that it might in fact be a *better* model, but it
+> means starting over completely in thinking about all of these examples
+> of inheritance and the like.
+
+I don't think it is that big a deal, since it means you simply ignore the "Pre"
+as far as inheritance, and only worry about Pre'Class. One reason I prefer this
+is that it means "Pre" can be all about the code you are "protecting" with the
+precondition, while Pre'Class can be about what the abstract interface requires.
+
+Cyrille from AdaCore finds the whole Pre'Class inheritance "or"-ing thing
+unpleasant, and I think there are others who might have the same view, and it
+seems potentially a benefit if Pre and Pre'Class are treated independently.
+
+Note that this doesn't come up for Post and Post'Class, since everything is
+and-ed together.
+
+> One thing that immediately comes to mind is how Pre'Class is treated
+> vis-a-vis access-to-subprogram. One of the advantages of the model
+> that I proposed is that access-to-subprogram is treated the same way
+> as a similar dispatching call (one without a Pre'Class aspect). I
+> don't see how that could work in the model you are suggesting; since
+> Pre'Class would be unknown (and thus True), it would be ignored on any
+> access-to-subprogram call (at least unless we allowed Pre'Class on
+> access-to-subprogram types). Sounds like a nasty hole.
+
+The model I thought we were talking about for access-to-subprogram was that you
+effectively created a call at the point of the 'Access, and whatever Pre'Class
+or Pre aspects that would be enforced at that point are the Pre'Class/Pre that
+would be enforced at the point of any call through that access value. That
+seems very well defined, and yes, does imply a wrapper in some implementations.
+So it is really the code calling 'Access that has to worry about whether the
+preconditions will be satisfied at the point of any indirect call. That seems
+about right.
+
+> I'm presuming that in this model, the Pre'Class aspects are "or"ed
+> together, then the result is "and"ed with Pre. If there is no
+> Pre'Class, it is treated as True.
+
+Yes, that is effectively what I am proposing.
+
+>
+> I'd hope that we continue to have the Pre'Class model as I laid out in
+> my wording proposal (that we use the Pre'Class of the statically
+> identified subprogram, which is necessarily the same or stronger than
+> the Pre'Class of the invoked body). And then Pre of the invoked body would be evaluated.
+
+Right, though I would still allow the additional Pre'Class aspects to be
+*evaluated*, even if the caller isn't aware of them.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 1:43 PM
+
+> Cyrille from AdaCore finds the whole Pre'Class inheritance "or"-ing
+> thing unpleasant, and I think there are others who might have the same
+> view, and it seems potentially a benefit if Pre and Pre'Class are
+> treated independently.
+>
+> Note that this doesn't come up for Post and Post'Class, since
+> everything is and-ed together.
+
+OK, I'll think about this in wording terms.
+
+> > One thing that immediately comes to mind is how Pre'Class is treated
+> > vis-a-vis access-to-subprogram. One of the advantages of the model
+> > that I proposed is that access-to-subprogram is treated the same way
+> > as a similar dispatching call (one without a Pre'Class aspect). I
+> > don't see how that could work in the model you are suggesting; since
+> > Pre'Class would be unknown (and thus True), it would be ignored on
+> > any access-to-subprogram call (at least unless we allowed Pre'Class
+> > on access-to-subprogram types). Sounds like a nasty hole.
+>
+> The model I thought we were talking about for access-to-subprogram was
+> that you effectively created a call at the point of the 'Access, and
+> whatever Pre'Class or Pre aspects that would be enforced at that point
+> are the Pre'Class/Pre that would be enforced at the point of any call
+> through that access value. That seems very well defined, and yes,
+> does imply a wrapper in some implementations. So it is really the
+> code calling 'Access that has to worry about whether the preconditions
+> will be satisfied at the point of any indirect call. That seems about
+> right.
+
+OK, again I'll try to think about this in wording terms.
+
+> > I'm presuming that in this model, the Pre'Class aspects are "or"ed
+> > together, then the result is "and"ed with Pre. If there is no
+> > Pre'Class, it is treated as True.
+>
+> Yes, that is effectively what I am proposing.
+> >
+> > I'd hope that we continue to have the Pre'Class model as I laid out
+> > in my wording proposal (that we use the Pre'Class of the statically
+> > identified subprogram, which is necessarily the same or stronger
+> > than the Pre'Class of the invoked body). And then Pre of the
+> invoked body would be evaluated.
+>
+> Right, though I would still allow the additional Pre'Class aspects to
+> be *evaluated*, even if the caller isn't aware of them.
+
+Do we need wording for that? I had thought that was irrevelant (if the compiler
+wants to evaluate 50 digits of PI between each statement, it is allowed to do
+that). Or is there some issue with side-effects?
+
+Anyway, you need to think about the implicit body wording that you thought was
+too "mechanistic". Since that only exists to fix various problems with
+Pre'Class/Post'Class/Type_Invariant'Class combinations, and nothing said above
+has any effect on those problems, we still need that wording or something
+equivalent. I tried to explain how I arrived at that wording in a previous
+message, hopefully so that you or someone else could come up with a better idea
+of how to approach it wording-wise. Please help (or decide to live with my
+proposal)...
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 2:57 PM
+
+>> Right, though I would still allow the additional Pre'Class aspects to
+>> be *evaluated*, even if the caller isn't aware of them.
+>
+> Do we need wording for that? I had thought that was irrevelant (if the
+> compiler wants to evaluate 50 digits of PI between each statement, it
+> is allowed to do that). Or is there some issue with side-effects?
+
+I think the bigger issue is if one of them evaluates to True even though the one
+visible to the caller evaluates to False, can we go ahead and execute the body.
+
+> Anyway, you need to think about the implicit body wording that you
+> thought was too "mechanistic". Since that only exists to fix various
+> problems with Pre'Class/Post'Class/Type_Invariant'Class combinations,
+> and nothing said above has any effect on those problems, we still need
+> that wording or something equivalent. I tried to explain how I arrived
+> at that wording in a previous message, hopefully so that you or
+> someone else could come up with a better idea of how to approach it
+> wording-wise. Please help (or decide to live with my proposal)...
+
+I'll see if I can come up with something less mechanistic.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 3:19 PM
+
+> >> Right, though I would still allow the additional Pre'Class aspects
+> >> to be *evaluated*, even if the caller isn't aware of them.
+> > Do we need wording for that? I had thought that was irrevelant (if
+> > the compiler wants to evaluate 50 digits of PI between each
+> > statement, it is allowed to do that). Or is there some issue with side-effects?
+>
+> I think the bigger issue is if one of them evaluates to True even
+> though the one visible to the caller evaluates to False, can we go
+> ahead and execute the body.
+
+That's not a "bigger issue"; it's the whole point of the rule. The answer is
+"NO"! Because there is no way to allow that and still have a check at the call
+site. (You can evaluate the preconditions you know about at the call site, but
+if you can't raise an exception when they evaluate to False [because some
+precondition you don't know about might be True], what is the point? The only
+other way to implement that would be to pass in what you know as an additional
+parameter, which seems way over the top.)
+
+I've repeatedly said that we have to require the checking of the stronger
+precondition, because it is consistent with the caller's view of the world, and
+it is the only way to do the check at the call site. Moreover, I'm dubious that
+"weakening" the class-wide precondition is useful in practice -- and since
+"strenghtening" it violates LIS, in most programs it will be the same all the
+way up. (Meaning this only will matter in corner cases.)
+
+The only reason to worry about evaluation of the others is because you want to
+generate them in the body (or wrapper) for some reason. But that does not appear
+to be necessary (assuming we use my "required body" model for the messy cases).
+In that case, why even allow it?
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 4:28 PM
+
+I guess what I was considering, at least for a moment, was whether we wanted it
+to be "OK" for it be *unspecified* whether an exception is raised in the case
+where the weaker Pre'Class is satisfied but the caller-visible Pre'Class is
+*not* satisfied.
+
+I admit that sounds pretty weird... And it sure sounds like bad news for
+portability.
+
+So I guess I am convinced that you *must* do Pre'Class checks at the call site,
+and only at the call site.
+
+I do think this begins to argue pretty strongly for separating out "Pre" from
+Pre'Class, and effectively putting the "Pre" checks in the body (though *not*
+handleable! -- they are like a pragma Assert in the outer declarative part of
+the subprogram), along with the Post and Post'Class, while the Pre'Class checks
+remain strictly at the caller, and are based on the particular "view" denoted by
+the caller, not by the body actually reached.
+
+I also think that for access-to-subprogram, if the designated subprogram has a
+Pre'Class aspect, the access value generated by 'Access must designate a wrapper
+that checks it (unless of course Assertions are being ignored). Otherwise, a
+simple way of bypassing a Pre'Class check would be to declare a local
+access-to-subprogram type, and then call through that. Hardly seems desirable.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 3:32 PM
+
+...
+> The current rules proposal does not allow any Pre/Post exceptions to
+> be handled by the body, and I think that is exactly right. Your
+> assertion that we never discussed it is wrong; we discussed it
+> ad-nausem at the Tallehasse meeting (I think you missed that one,
+> probably why you don't know that).
+> 13.3.2(18/3) is pretty clear that this is the intent. The reason is
+> that for statically bound cases, we ought to let the compiler have the
+> freedom to generate the checks wherever it wants (in the body or at
+> the call site) - in order to maximize the possibilities for
+> optimization/proof.
+> Dispatching calls and access-to-subprogram are different, of course.
+
+One additional point I thought of on the way home last night: the body of a
+subprogram does not necessarily know about all of the postconditions that apply
+to it. Additional ones can be added to inherited versions via progenitors. Those
+also have to be evaluated, and I can't think of any sane way to do that so that
+the exception could be handled within the body. (You could pass in a thunk with
+such postconditions, but that would be a lot of overhead for something that is
+going to happen very rarely.) The other possibility would be to make such
+subprograms illegal in some way (one of the options I already considered for
+this case); but that requires users to write wrappers by hand, with all of the
+possibilities for error that entails.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 4:14 PM
+
+I agree we discussed the issue of handling pre/post-condition exceptions and
+concluded they should *not* be handle-able in the body. Let's not re-open that
+one.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, March 24, 2011 6:03 PM
+
+> One additional point I thought of on the way home last night: the body
+> of a subprogram does not necessarily know about all of the
+> postconditions that apply to it. Additional ones can be added to
+> inherited versions via progenitors. Those also have to be evaluated,
+> and I can't think of any sane way to do that so that the exception
+> could be handled within the body. (You could pass in a thunk with such
+> postconditions, but that would be a lot of overhead for something that
+> is going to happen very rarely.) The other possibility would be to
+> make such subprograms illegal in some way (one of the options I
+> already considered for this case); but that requires users to write
+> wrappers by hand, with all of the possibilities for error that entails.
+
+If true, this is very worrisome, I don't see any easy way for us to accomodate
+that in our implementation
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 7:11 PM
+
+The model that Tucker and I have been discussing is that for such inherited
+subprograms, the semantics is as if there was an explicit body for the routine
+(complete with the expected postcondition checks, if you are doing them inside
+of the body), which just calls the parent routine. This seems to be about as
+hard to implement as the other cases where you have to generate a wrapper for a
+tag or a use of 'Access, so I don't think there can be a major implementation
+problem. If there is, however, we probably should use the "requires overriding"
+solution instead (which would insist that the client write an explicit body for
+the routine).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 7:44 PM
+
+> If true, this is very worrisome, I don't see any easy way for us to
+> accomodate that in our implementation
+
+Randy was simply giving more reasons why exceptions arising from postconditions
+shouldn't be handleable in the body. But we decided a long time ago that these
+exceptions are not handle-able inside the body, so this whole thread is merely
+reinforcing that decision.
+
+Actually adding the additional postcondition checks isn't that hard, it just
+means creating a wrapper. But Randy's point was that such a wrapper cannot
+raise an exception that could be handled inside the body it is wrapping! But
+who cares, since we don't want the exception to be handle-able anyway.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 5:24 PM
+
+> I also think that for access-to-subprogram, if the designated
+> subprogram has a Pre'Class aspect, the access value generated by
+> 'Access must designate a wrapper that checks it (unless of course
+> Assertions are being ignored). Otherwise, a simple way of bypassing a
+> Pre'Class check would be to declare a local access-to-subprogram type,
+> and then call through that. Hardly seems desirable.
+
+Alternatively, we say that a subprogram to which a Pre'Class aspect applies has
+effectively an "Intrinsic" convention, so you can't take 'Access of it. That
+would mean the compiler wouldn't have to create the wrapper. The user could of
+course always create an explicit wrapper if they needed one.
+
+OK, this brings up another Baird-ish question: What happens if you rename a
+subprogram to which a Pre'Class applies. Does it still apply? If you rename it
+to be something that is not a dispatching operation, then it is only interesting
+if it is non-abstract, and you can only call it in a non-dispatching way, so it
+feels like it should still be subject to the same Pre'Class check. But we have
+a rule that you can't specify a Pre'Class attribute on anything but a
+dispatching operation. But we aren't really specifying it, we are just carrying
+it over. It would again seem weird if you could get rid of the effect of a
+Pre'Class aspect simply by renaming the subprogram. Perhaps we are adopting the
+renaming-as-body semantics, which is essentially a wrapper model.
+
+OK, now here is the killer follow-up: What happens if you rename it to be
+another dispatching operation, and it overrides an inherited subprogram which
+had its own Pre'Class attribute? This feels like trouble, and almost argues for
+the same trick suggested above for access-to-subprogram, namely disallow the
+rename, since effectively the "conventions" don't match, where "convention" has
+now been augmented to include the Pre'Class aspect, since that certainly affects
+what you have to do at the call site.
+
+The simplest solution to all of these problems might be to say that subtype
+conformance (which is needed for 'Access, overriding, and renaming-as-body)
+requires that the "same" Pre'Class aspects, if any, apply to both subprograms
+(for overriding, clearly this has to allow a new Pre'Class aspect to be applied
+*after* the overriding occurs -- which is sort of OK, since aspect specs don't
+get elaborated until the freezing point).
+
+This also implies that if some day we allow Pre'Class aspects on access-to-subp,
+then that might be a way to support 'Access on these guys (though it doesn't
+seem like an important capability at this point).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 7:21 PM
+
+Fascinating. I proposed something like this a while back, but rejected it as too
+outlandish. I personally would go further and *not* allow further specification
+of Pre'Class (or Post'Class or Type_Invariant'Class for that matter). Then there
+is no combination cases, no one is confused by "or" or "and". We don't need
+implicit bodies when there is multiple inheritance. If you need to add some
+precondition, you still have Pre/Post/Type_Invariant.
+
+This indeed is my model of how these should work -- modifying Pre'Class or
+Post'Class on a dispatching routines just does not make sense to me -- we don't
+allow that for any other property. And I cannot think of any significant reason
+why you would want to do this in practice. (Maybe there is some reason relating
+to multiple inheritance -- I don't think too hard about that.)
+
+But I thought all of this would end up way too limiting. Especially because
+there isn't any way for it to allow no precondition to match, making it much
+harder to match interfaces. And I can't see any way to add Pre'Class to subtype
+conformance and then somehow not have it apply to an overriding routine. That
+would be a major change in model -- it would invalidate 3.9.2(10/2) which seems
+to be the cornerstone of Ada OOP. (At least of the implementability of Ada OOP.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 7:59 PM
+
+> Fascinating. I proposed something like this a while back, but rejected
+> it as too outlandish. I personally would go further and *not* allow
+> further specification of Pre'Class (or Post'Class or
+> Type_Invariant'Class for that matter). Then there is no combination
+> cases, no one is confused by "or" or "and". We don't need implicit
+> bodies when there is multiple inheritance. If you need to add some precondition, you still have Pre/Post/Type_Invariant.
+
+I am *not* recommending that. You can still override, but you can't do so by
+renaming another dispatching operation that already has a Pre'Class. And you
+*can* weaken the Pre'Class if you wish.
+
+I think that is important because the Pre'Class on the root type might be too
+strong for some important subtree of the type hierarchy. That subtree should be
+able to have a weaker Pre'Class if it makes sense in that subtree.
+
+> This indeed is my model of how these should work -- modifying
+> Pre'Class or Post'Class on a dispatching routines just does not make
+> sense to me -- we don't allow that for any other property.
+
+I don't follow you when you say "any other property." To what are you
+referring. Clearly the 'Address, the names of the formal parameters, the
+default expressions, whether the routine is inlined, and most importantly the
+code itself, can change with the overriding.
+
+> ... And I cannot think of any
+> significant reason why you would want to do this in practice. (Maybe
+> there is some reason relating to multiple inheritance -- I don't think
+> too hard about that.)
+
+I don't agree; weakening the Pre'Class can make sense as you go into a
+particular subtree of the type hierarchy.
+
+> But I thought all of this would end up way too limiting. Especially
+> because there isn't any way for it to allow no precondition to match,
+> making it much harder to match interfaces.
+
+I believe you are going to far. I was using the subtype conformance as a way to
+eliminate various unpleasant cases that require wrappers. I am not suggesting we
+break the whole model, just that we effectively outlaw things like 'Access and
+weird renamings.
+
+> ... And I can't see any way to add Pre'Class to subtype conformance
+> and then somehow not have it apply to an overriding routine.
+
+This just requires a wording tweak in my view. Para 3.9.2(10/2) now says:
+
+ ... If the dispatching operation overrides an inherited
+ subprogram, it shall be subtype conformant with the inherited
+ subprogram. ...
+
+If we add Pre'Class matching to subtype conformance, then that is almost exactly
+what we want. But after the overriding takes place, we want to allow further
+weakening of the Pre'Class, so if necessary we add something to the above
+sentence to make it clear that that is OK.
+
+> ... That would be a major change in model -- it would invalidate
+> 3.9.2(10/2) which seems to be the cornerstone of Ada OOP. (At least of
+> the implementability of Ada OOP.)
+
+I'm not suggesting we drop the above sentence, but rather have it say something
+about Pre'Class if necessary to allow weakening it, but not replacing the
+Pre'Class via a renaming of some other dispatching operation which has a
+completely different Pre'Class.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 8:31 PM
+
+> I don't follow you when you say "any other property." To what are you
+> referring. Clearly the 'Address, the names of the formal parameters,
+> the default expressions, whether the routine is inlined, and most
+> importantly the code itself, can change with the overriding.
+
+"Interesting" property visible in the contract: constraints, no-return, not
+null, predicates, "Is_Synchronized", etc.
+
+My personal feeling is that allowing the parameter names and defaults to change
+was a mistake, but not a very important one.
+
+> > ... And I cannot think of any
+> > significant reason why you would want to do this in practice. (Maybe
+> > there is some reason relating to multiple inheritance -- I don't
+> > think too hard about that.)
+>
+> I don't agree; weakening the Pre'Class can make sense as you go into a
+> particular subtree of the type hierarchy.
+
+I would like to see an example of why you would want this in practice (not in
+theory!!). There is a lot of OOP stuff that makes sense in theory but never
+actually happens in practice. Needing to "weaken" the precondition seems to me
+like there was a bug in the original definition of the precondition (most
+likely, the boolean functions that make it up are not defined properly). But I
+am willing to believe that I am wrong -- but to do that I'd need to see an
+example for which the weaker precondition makes sense.
+
+> > But I thought all of this would end up way too limiting. Especially
+> > because there isn't any way for it to allow no precondition to
+> > match, making it much harder to match interfaces.
+>
+> I believe you are going to far. I was using the subtype conformance
+> as a way to eliminate various unpleasant cases that require wrappers.
+> I am not suggesting we break the whole model, just that we effectively
+> outlaw things like 'Access and weird renamings.
+
+Fine, but then you can't do it with subtype conformance, since overriding
+routines are required to be subtype conformant.
+
+> > ... And I can't see any way to add Pre'Class to subtype conformance
+> > and then somehow not have it apply to an overriding routine.
+>
+> This just requires a wording tweak in my view. Para
+> 3.9.2(10/2) now says:
+>
+> ... If the dispatching operation overrides an inherited
+> subprogram, it shall be subtype conformant with the inherited
+> subprogram. ...
+>
+> If we add Pre'Class matching to subtype conformance, then that is
+> almost exactly what we want. But after the overriding takes place, we
+> want to allow further weakening of the Pre'Class, so if necessary we
+> add something to the above sentence to make it clear that that is OK.
+
+Then you're breaking the definition of subtype conformance. That seems really
+bad to me; in large part because it seems likely that you'll want other such
+exceptions in the future. It just turns into a morass.
+
+> > ... That would be a major change in model -- it would invalidate
+> > 3.9.2(10/2) which seems to be the cornerstone of Ada OOP. (At least
+> > of the implementability of Ada OOP.)
+>
+> I'm not suggesting we drop the above sentence, but rather have it say
+> something about Pre'Class if necessary to allow weakening it, but not
+> replacing the Pre'Class via a renaming of some other dispatching
+> operation which has a completely different Pre'Class.
+
+That just does not make any sense. You're saying that it has to be subtype
+conformant, but it is OK for it not to be subtype conformant sometimes. That way
+lies madness (mine :-).
+
+I do agree that requiring that always it too strong a restriction, so I think
+you have to change something else. Perhaps we need a fifth kind of conformance
+(subtype - Pre'Class) -- "overriding conformance" which is the current
+definition of subtype conformance. Then add "subtype conformance" which would be
+the current kind + Pre'Class??
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, March 24, 2011 7:24 PM
+
+> If true, this is very worrisome, I don't see any easy way for us to
+> accomodate that in our implementation
+
+Is there any hope that I can get through this email thread without reading all
+of it? Randy and Tuck have been going at it for 3 days, and I've saved the
+emails unread. Do I need to read all the emails?
+
+I think it's important and I need to understand the issues, but I feel
+overwhelmed. Any possibility of a summary?
+
+P.S. I think we should at least ALLOW preconditions to be checked at the call
+site.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 24, 2011 8:13 PM
+
+Here is what we are debating:
+
+ 1) Must Pre'Class be checked at the call site,
+ or could it be done inside the body?
+ Answer: we seem to agree it only makes sense
+ if it is done at the point of call, and only
+ the Pre'Class aspects known at the point of call
+ are checked.
+
+ 2) Should specifying a Pre'Class have any affect on
+ the "Pre" aspects?
+ Tuck's Answer: No, let's split them completely.
+ This allows (and pretty much requires) "Pre" aspects
+ to be checked in the body.
+ Randy's Answer: Not sure.
+
+ 3) What are some of the implications of renaming and taking
+ 'Access of a subprogram to which Pre'Class applies?
+ Tuck's Answer: Make hard stuff illegal, by incorporating
+ Pre'Class matching into subtype conformance, but still
+ allow Pre'Class weakening.
+ Randy's Answer: Not sure. Maybe disallow Pre'Class weakening
+ completely.
+
+One other issue that seems clear is that when you inherit code for an operation
+from a parent type, and you also inherit the "same" operation from one or more
+interfaces where the operation has a Post'Class aspect, you will probably have
+to create a wrapper to properly incorporate the inherited Post'Class aspects
+into the inherited code, since they all get and-ed together.
+
+Randy can fill in more if I have forgotten something.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 24, 2011 8:43 PM
+
+> 2) Should specifying a Pre'Class have any affect on
+> the "Pre" aspects?
+> Tuck's Answer: No, let's split them completely.
+> This allows (and pretty much requires) "Pre" aspects
+> to be checked in the body.
+> Randy's Answer: Not sure.
+
+I think you've convinced me on this one.
+
+> 3) What are some of the implications of renaming and taking
+> 'Access of a subprogram to which Pre'Class applies?
+> Tuck's Answer: Make hard stuff illegal, by incorporating
+> Pre'Class matching into subtype conformance, but still
+> allow Pre'Class weakening.
+> Randy's Answer: Not sure. Maybe disallow Pre'Class weakening
+> completely.
+
+I'm not against the idea, I'm against the execution. I'm surely in favor of
+making hard stuff illegal!
+
+> One other issue that seems clear is that when you inherit code for an
+> operation from a parent type, and you also inherit the "same"
+> operation from one or more interfaces where the operation has a
+> Post'Class aspect, you will probably have to create a wrapper to
+> properly incorporate the inherited Post'Class aspects into the
+> inherited code, since they all get and-ed together.
+
+This also applies to Type_Invariant'Class (it works like Post'Class in that
+sense).
+
+This latter issue is the "bug"; this has to be addressed or we will have
+problems with missed Pre'Class/Post'Class in inherited operations (bodies that
+get called without their preconditions being satisfied are really bad. The other
+things are all about making the model better, we could live without them but
+everyone will be happier if we don't.
+
+> Randy can fill in more if I have forgotten something.
+
+I think that is it. Lots of examples in my various e-mails; it will help to go
+back and make sure those all make sense in the end.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, March 25, 2011 10:53 PM
+
+I've been trying to work on the wording for this AI, and...
+
+...
+> The simplest solution to all of these problems might be to say that
+> subtype conformance (which is needed for 'Access, overriding, and
+> renaming-as-body) requires that the "same"
+> Pre'Class aspects, if any, apply to both subprograms (for overriding,
+> clearly this has to allow a new Pre'Class aspect to be applied *after*
+> the overriding occurs -- which is sort of OK, since aspect specs don't
+> get elaborated until the freezing point).
+
+I don't understand why you only are worrying about renames-as-body here. Doesn't
+renames-as-declaration have the same problem? An overriding is not a completion,
+after all, it is a new declaration of a homograph.
+
+The problem in question is renaming a routine that has one or more class-wide
+preconditions as an overriding of another routine that has one or more different
+class-wide preconditions. We can only allow weakening, but this is not likely to
+be that. I don't see any reason that you can't use a renames-as-declaration in
+such a context.
+
+("Class-wide preconditions" is the nice name I gave Pre'Class in my wording
+proposal - trying to talk about Pre'Class separately from Pre is beyond what I
+can do wording-wise.)
+
+If that's the case, modifying subtype conformance does not do the trick, since
+renames-as-declaration only needs mode-conformance. We probably need separate
+legality rules in that case.
+
+The basic problem (both for renames and for access-to-subprogram) is that we
+don't allow specifying the class-wide precondition, so we have to assume "True"
+and that starts to get weird.
+
+===============
+
+The aspects of a renames are the same as the renamed entity (unless otherwise
+specified), so there does not seem to be a problem with any sort of renames that
+isn't overriding. So I have to think we just want a hack to cover that case.
+
+Indeed, all we really need to do is declare that a renames is just a shorthand
+for an explicit body in this case; indeed this is exactly the same sort of
+problem that occurs via multiple inheritance. We should solve these the same way
+(either make both illegal, with a specific rule) or just use the rules I've
+previously laid out.
+
+The access-to-subprogram also might as well get a specific Legality Rule.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, March 25, 2011 11:59 PM
+
+Attached find a new draft of the AI (version /03) covering these issues. I fear
+that I didn't do a very good job of explaining the overall model, but I was
+concentrating on the wording changes needed. Now back to pragmas => aspects.
****************************************************************
Questions? Ask the ACAA Technical Agent