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

--- ai05s/ai05-0247-1.txt	2011/03/22 08:04:17	1.1
+++ ai05s/ai05-0247-1.txt	2011/03/23 00:45:42	1.2
@@ -1,4 +1,4 @@
-!standard 13.3.2(19/3)                                 11-03-21  AI05-0247-1/01
+!standard 13.3.2(19/3)                                 11-03-22  AI05-0247-1/02
 !reference AI05-0145-2
 !class Amendment 11-03-21
 !status work item 11-03-21
@@ -149,13 +149,88 @@
 OTOH, a dispatching call using an object of T1'Class does not need to check
 Is_Green at all.
 
-...
-
-
+Note that if we are using Pre rather than Pre'Class, then the preconditions of
+a dispatching call need have any real relationship. In that case, the existing
+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:
+  * 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).
 
 !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.
+
+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.
+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:
+   * 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.
+
+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.
+
+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).
+
+[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).]
+
 !discussion
 
 This issue originally came up because null procedures are considered the same
@@ -166,6 +241,27 @@
 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
+bodies, since that is the only that they can be eliminated by optimization or
+other forms of proof. (But we need to be able to effectively generate them at
+the call site in order to use them as known values in following preconditions.)
+
+In any case, the language defines all of these checks as being made at the call
+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.
+
+
+
 !corrigendum 13.3.2(0)
 
 @dinsc
@@ -1338,5 +1434,248 @@
 
 then adding a later precondition on some extension would have no effect.
 Whatever rules we come up with had better take this into account.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, March 22, 2011  9:47 AM
+
+I think you need to put a Pre'Class
+precondition on the operations of the root type if you want any of this to work.
+
+I suppose we could treat the "Pre" and the "Pre'Class"
+preconditions completely independently, and the "Pre'Class" get weakened as you
+go down the hierarchy, and the Pre are evaluated as is, and a failure of the
+"Pre" is a failure, end of story, just as though the precondition were an
+assertion as the first line of the subprogram body.
+
+That way you could add Pre's anywhere, and not have to worry about your
+ancestors.  They would be effectively enforced in the body.  Meanwhile,
+Pre'Class would be consistently described as enforced at the call site, and
+would undergo weakening.  I guess I kind of favor this model. Mixing Pre and
+Pre'Class seems like a mistake in general, and I believe that projects will
+adopt one approach or the other.
+
+We would still need to think about how access-to-subp interacts with this.
+Probably should still be modeled as a call on a conjured-up subprogram that
+contains a normal, non-dispatching call on the designated subprogram.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, March 22, 2011  4:52 PM
+
+> I think you need to put a Pre'Class
+> precondition on the operations of the root type if you want any of
+> this to work.
+
+I can believe that that is preferred. But the language rules have to make sense
+even when that is not done, because of compatibility concerns. There is a lot of
+code out there without preconditions, and we don't want to prevent using it, or
+make it hard to use preconditions.
+
+> I suppose we could treat the "Pre" and the "Pre'Class"
+> preconditions completely independently, and the "Pre'Class"
+> get weakened as you go down the hierarchy, and the Pre are evaluated
+> as is, and a failure of the "Pre" is a failure, end of story, just as
+> though the precondition were an assertion as the first line of the
+> subprogram body.
+
+Yes, I think I suggested something on this line a week or two ago. I think it
+makes more sense.
+
+> That way you could add Pre's anywhere, and not have to worry about
+> your ancestors.  They would be effectively enforced in the body.
+> Meanwhile, Pre'Class would be consistently described as enforced at
+> the call site, and would undergo weakening.  I guess I kind of favor
+> this model.
+> Mixing Pre and Pre'Class seems like a mistake in general, and I
+> believe that projects will adopt one approach or the other.
+
+I have to wonder if we shouldn't enforce that. Mixing them makes no logical
+sense. (I also proposed this last week.)
+
+Specifically, either one of Pre'Class or Pre can be specified on a subprogram.
+And, for an overriding/inherited routine, Pre'Class can only be specified/added
+to a subprogram if its ancestors have Pre'Class. (And if Pre'Class is inherited,
+then Pre cannot be specified, only Pre'Class.)
+
+These rules would avoid confusion with mixed Pre/Pre'Class environments.
+Pre'Class works like the Eiffel contracts; Pre is more of a free-form assertion.
+
+Pre would always just be that of the body. Pre'Class would be that of the
+*call* (with the special cases for inheritance from two subprograms).
+
+One could even consider access-to-subprogram in the same way, as a profile that
+does not have a Pre'Class, meaning that subprograms with Pre'Class couldn't
+match it. We could then consider adding Pre'Class/Post'Class to
+access-to-subprogram, making the similarity with dispatching calls complete.
+
+This might be going too far, but it seems that combining Pre and Pre'Class is
+too confusing for everyone. We're better off without it.
+
+> We would still need to think about how access-to-subp interacts with
+> this.  Probably should still be modeled as a call on a conjured-up
+> subprogram that contains a normal, non-dispatching call on the
+> designated subprogram.
+
+I've answered this repeatedly, and you don't seem to be registering my various
+ideas. So I'm not sure what's wrong with them.
+
+Anyway, it strikes me that any model separation would be on top of the existing
+rules. I think I've figured out a consistent set of changes to the dynamic
+semantics that fixes the issues (but I'm sure once Steve reviews it I will have
+that misconception removed ;-). I think we could add some Legality Rules to it
+if we wanted to seriously separate Pre and Pre'Class, but I don't think it is
+required. I'll try to write it up ASAP.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, March 22, 2011  5:05 PM
+
+>> I suppose we could treat the "Pre" and the "Pre'Class"
+>> preconditions completely independently, and the "Pre'Class"
+>> get weakened as you go down the hierarchy, and the Pre are evaluated
+>> as is, and a failure of the "Pre" is a failure, end of story, just as
+>> though the precondition were an assertion as the first line of the
+>> subprogram body.
+>
+> Yes, I think I suggested something on this line a week or two ago. I
+> think it makes more sense.
+
+Yes, I should have acknowledged you.  But I frequently lose track of where ideas
+come from (sorry about that), and just slowly integrate them into the overall
+possibilities...
+
+>> We would still need to think about how access-to-subp interacts with
+>> this.  Probably should still be modeled as a call on a conjured-up
+>> subprogram that contains a normal, non-dispatching call on the
+>> designated subprogram.
+>
+> ... I've answered this repeatedly, and you don't seem to be
+> registering my various ideas. So I'm not sure what's wrong with them.
+
+Sorry, again I am having trouble keeping track of whose ideas are whose.  Are we
+in agreement on this one, namely that an access-to-subp is equivalent to a
+"normal" call on the designated subprogram, with the appropriate pre or
+pre'class enforced?  That is, any precondition check to be performed is bundled
+into a wrapper if necessary?  Or if not, how does your idea differ?
+
+> Anyway, it strikes me that any model separation would be on top of the
+> existing rules. I think I've figured out a consistent set of changes
+> to the dynamic semantics that fixes the issues (but I'm sure once
+> Steve reviews it I have that misconception removed ;-). I think we
+> could add some Legality Rules to it if we wanted to seriously separate
+> Pre and Pre'Class, but I don't think it is required. I'll try to write it up ASAP.
+
+Great.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, March 22, 2011  5:14 PM
+
+> Yes, I think I suggested something on this line a week or two ago. I
+> think it makes more sense.
+
+Minor aside: There doesn't seem to be any rule restricting Pre'Class or
+Post'Class to dispatching routines of a tagged type. It seems these are allowed
+on untagged types, routines that aren't primitive, and the like. Is this
+intended, or even a good idea??
+
+    type Foo is new Integer;
+    function "+" (Left, Right : Foo) return Foo
+       with Pre'Class => Left > 0 and Right > 0;
+
+    type Bar is new Foo;
+    function "+" (Left, Right : Bar) return Bar;
+       -- Inherits Pre'Class???
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, March 22, 2011  5:53 PM
+
+...
+>> I'll try to write it up ASAP.
+>
+> Great.
+
+Hopefully this was an optimistic "great" and not the other kind. :-) Anyway,
+here is version /02 of this AI, complete with a wording proposal. I didn't do
+anything with legality rules (even though I think some restrictions there would
+be a good idea). This seems to me to be about the minimum change to fix the
+problems previously identified.
+
+As always, comments welcome.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, March 22, 2011  6:10 PM
+
+> Yes, I should have acknowledged you.  But I frequently lose track of
+> where ideas come from (sorry about that), and just slowly integrate
+> them into the overall possibilities...
+
+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). 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.]
+
+If we made this sort of thing illegal, this could not happen.
 
 ****************************************************************