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

Differences between 1.2 and version 1.3
Log of other versions for file ai05s/ai05-0197-1.txt

--- ai05s/ai05-0197-1.txt	2010/02/23 07:31:06	1.2
+++ ai05s/ai05-0197-1.txt	2011/03/17 06:55:56	1.3
@@ -1,4 +1,5 @@
-!standard  3.9.2(20.2/2)                             10-02-08    AI05-0197-1/01
+!standard  3.9.2(20.1/2)                             10-03-17    AI05-0197-1/02
+!standard  3.9.2(20.2/2)
 !class binding interpretation 10-02-08
 !status work item 10-02-08
 !status received 09-06-09
@@ -62,6 +63,14 @@
 
 !wording
 
+Insert a new bulleted item after 3.9.2(20.1/3):
+
+ * If the corresponding operation is a predefined operator
+   then the action comprises an invocation of that operator;
+
+[Editor's note: This handles predefined "=", which is not inherited but
+rather constructed anew for each time.]
+
 Modify 3.9.2(20.2/2):
 
 * otherwise, the action is the same as the action for the corresponding operation
@@ -121,7 +130,7 @@
   begin
       Op1 (X => Obj); -- (5)
   end Pack1.Pack3;
-    
+
 For the call (5), (4) is the declaration that is called. That can be verified
 by using the formal parameter name X in named notation in the call; a call using
 parameter name Y is illegal as declaration (3) is hidden from all visibility.
@@ -296,5 +305,468 @@
   end Pack1.Pack3;
 
 So I don't think the proposed wording in AI05-126 is adequate.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Thursday, March 3, 2011  3:28 PM
+
+> AI05-0197-1: Improve this wording (with help from Tucker). [Sorry, I
+> don't have any more detail in my notes than that; they say "Tucker
+> does not like this wording which" and little else.]
+
+Neither Tuck nor I could reconstruct the problem that we thought we had identified at the Tampa meeting, but I did find a couple of new issues while trying.
+
+Again, thanks to Randy and Tuck for their review and suggestions.
+
+Problem #1:
+
+Applying 3.9.2(20-20.3) to a dispatching call to the predefined "=" operator of
+a tagged type, it says
+
+   Is it explicitly declared? No. Move to next bullet.
+
+   Is it implemented via an entry/protected subp? No. Move to next
+   bullet.
+
+   This one begins with "otherwise", so it must be right!
+   We use the parent's equality op and extension components
+   do not participate in the result. Not good.
+
+Suggested fix:
+
+!wording (in addition to the existing wording for this AI)
+
+   Insert a new bulleted item after 3.9.2(20.1/3):
+
+   * If the corresponding operation is a predefined operator
+     then the action comprises an invocation of that operator;
+
+This should not require any change to any compiler; this is just changing the
+wording to reflect what was obviously intended to begin with.
+
+
+Problem #2:
+
+Making an arbitrary choice among null procedures assumes that they are
+interchangeable, and leads to problems if they are not.
+
+Consider the following example:
+
+    declare
+       package Pkg1 is
+           type Ifc is interface;
+           procedure Op (X : in out Ifc) is null;
+       end Pkg1;
+
+       package Pkg2 is
+          type T is tagged null record
+            with Type_Invariant => Is_Valid (T);
+          procedure Op (X : in out T) is null;
+          function Is_Valid (X : T) return Boolean;
+       end Pkg2;
+       package body Pkg2 is ... end Pkg2;
+
+       package Pkg3 is
+          type D is new Pkg1.T and Pkg2.Ifc with null record;
+       end Pkg3;
+    begin ...; end;
+
+Does a dispatching call to Pkg3.Op where the tag of the controlling operand is
+Pkg3.D'Tag result in a call to Is_Valid?
+
+It seems like it depends on the "arbitrary" choice mentioned in this AI's new
+wording for 3.9.2(20.2/2), which defines the dynamic semantics of such a
+dispatching call:
+
+   * otherwise, the action is the same as the action for the
+     corresponding operation of the parent type or progenitor
+     type from which the operation was inherited. {If there is
+     more than one such corresponding operation, the action is
+     that for the operation that is not a null procedure, if any;
+     otherwise, the action is that of an arbitrary one of the
+     operations.}
+
+If we flip a coin to decide which from among two candidates is the
+"corresponding operation ... from which the operation was inherited", and if
+exactly one of these two candidates includes a call to Is_Valid in its dynamic
+semantics, then it seems like we have a problem.
+
+Both here and when 8.3(12.3/2) says "one is chosen arbitrarily", we are relying
+on the premise that syntactically null procedures with appropriately conformant
+profiles are interchangeable with respect to dynamic semantics.
+
+One approach to this problem (which Randy can explain his views on in a separate
+message) would involve two steps:
+
+    1) In these two arbitrary-choice situations (3.9.2 and 8.3),
+       we add a preference rule preferring operations inherited
+       from a non-interface type over operations inherited from
+       an interface type.
+
+    2) We take whatever steps are needed (possibly none?)
+       in order to ensure that null procedures which are primitive ops
+       of interface types really are interchangeable (e.g., we
+       already disallow pre and post conditions for null procedures).
+
+This issue needs more work.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, March 4, 2011  1:15 AM
+
+...
+> Both here and when 8.3(12.3/2) says "one is chosen arbitrarily", we
+> are relying on the premise that syntactically null procedures with
+> appropriately conformant profiles are interchangeable with respect to
+> dynamic semantics.
+>
+> One approach to this problem (which Randy can explain his views on in
+> a separate message) would involve two steps:
+>
+>     1) In these two arbitrary-choice situations (3.9.2 and 8.3),
+>        we add a preference rule preferring operations inherited
+>        from a non-interface type over operations inherited from
+>        an interface type.
+>
+>     2) We take whatever steps are needed (possibly none?)
+>        in order to ensure that null procedures which are primitive ops
+>        of interface types really are interchangeable (e.g., we
+>        already disallow pre and post conditions for null procedures).
+>
+> This issue needs more work.
+
+I don't really have any views specifically on this problem, but the discussion
+of it has gotten me very concerned that there is something fundamentally wrong
+with the way we handle Pre/Post/Type_Invariant aspects on dispatching calls.
+I'll call these "contract aspects" in the discussion below; most of the points
+apply to all three of them.
+
+Tucker has explained that the contract aspects that apply to a particular
+subprogram body are always determined when that subprogram is declared. In
+particular, inheritance never changes the contract aspects of a subprogram body.
+
+That clearly works well on the body side of the contract; if the contracts
+changed with inheritance, it would be much harder to figure out what properties
+can be depended upon (or have to be preserved in the results).
+
+OTOH, it doesn't seem to work as well on the call side of the contract. The
+current rules say that the contracts depend on the actual body executed; the
+implementation is likely to be a wrapper around the "regular" body (if the
+contracts are normally enforced at the call site).
+
+This has some unfortunate effects when interfaces are "added" into an existing
+type hierarchy. For example, consider:
+
+    package P1 is
+       type T1 is tagged private;
+       function Is_Valid (Obj : T1) return Boolean;
+       procedure P1 (Obj : in out T1);
+    private
+       ...
+    end P1;
+
+    package P2 is
+       type I2 is interface;
+       function Is_Wobbly (Obj : I2) return Boolean is abstract;
+       procedure P1 (Obj : in out I2) is null
+           with Post'Class => Is_Wobbly (I2);
+       procedure P2 (Obj : in I2) is null
+           when Pre'Class => Is_Wobbly (I2);
+    end P2;
+
+    with P1, P2;
+    package P3 is
+       type T3 is new P1.T1 and P2.I2 with private;
+       overriding
+       function Is_Wobbly (Obj : T3) return Boolean;
+       overriding
+       procedure P2 (Obj : in T3);
+    private
+       ...
+    end P3;
+
+    with P1, P3;
+    procedure Main is
+        procedure Do_It (Obj : in P3.T3'Class) is
+        begin
+           Obj.P1; -- (1)
+           Obj.P2; -- (2)
+        end Do_It;
+        O3 : P3.T3;
+    begin
+        Do_It (O3);
+    end Main;
+
+The dispatching call to P1 at (1) will call P1.P1, inherited from type T1.
+This P1 has no postcondition, so Is_Wobbly will not be called on exit from P1.
+However, the following call to P2 at (2) will call P3.P2; it will inherit the
+precondition from the interface. Thus Is_Wobbly will be called on entrance to
+P2. If P1 returned a value for which Is_Wobbly is False (perhaps because the
+programmer forgot to override P1 for type T3), the *precondition* on the call to
+P2 would fail. But that is bizarre; given the postcondition matches the
+precondition for the type of the calls, it will be totally mysterious to the
+programmer as to why the failure is there. The only way to reason about these
+calls is to know the details of the contracts for all of the various possible
+routines involved -- that way seems to lead to madness! (And of course the code
+will most likely not be this easy to analyze).
+
+It is of course possible to create similar examples with the Type_Invariant
+aspect.
+
+These examples bother me so much simply because here we have a contract that we
+appear to be promising to enforce, yet we aren't enforcing it. Lying to the
+client (whether or not there is some logical reason for it) does not seem like a
+good policy.
+
+This is just one effect of these rules. More generally, these rules prevent any
+analysis of the contracts of a dispatching call -- by the programmer, by the
+compiler, or by any tool that doesn't have access to the complete source code of
+the program. That's because even if the entire program obeys a programming style
+rule to avoid the "funny" cases, a subprogram that hasn't even been written yet
+can add additional contracts (via any of the class-wide or specific contract
+aspects) -- and those would render any analysis wrong.
+
+One side effect of this that generating the contract aspects at the point of the
+call is not possible in general. That of course means that the compiler cannot
+eliminate checks of those aspects when they are not needed, nor point out when
+they are guaranteed to fail. It also means that wrappers are needed for the
+dispatching versions of routines if the compiler generates such aspects at the
+call site for statically bound calls.
+
+The rules for combining contracts (especially preconditions) also seem confusing
+at best. Adding a precondition to an overriding routine causes a *weaker*
+precondition; the original class-wide precondition no longer needs to be true.
+That does not seem helpful and surely makes analysis harder.
+
+All of these rules seem to vary from the usual model of dispatching calls. For
+instance, constraints can be thought of a weaker form of contract aspects (as
+preconditions involving only a single parameter, for instance). Ada 95 required
+constraints to match exactly (3.9.2(10/2) requires subtype conformance) for
+routines that override inherited routines (that is, possible dispatching
+targets). (Ada 2012 will of course extend this to subtype predicates.) Ada also
+has similar rules for other properties (including Convention, also in
+3.9.2(10/2), and the No_Return aspect (6.5.1(6/2))). It would have had similar
+rules for global in/global out annotations had those been defined, and most
+likely would have similar rules for exception contracts as well.
+
+So why should contract aspects (Pre/Post/Type_Invariant) be different? If these
+are considered part of the profile, with suitable rules all of the bizarre cases
+go away.
+
+The easiest rule would be to require (full) conformance of contract aspects that
+apply to a subprogram. Effectively, only one (class-wide) precondition could
+apply to a dispatching call - the same precondition would apply to all of the
+subprograms that could be dispatched to. This sounds very limiting, but as
+Tucker has pointed out, such a precondition could be made up of other
+dispatching calls. (Sorry Tucker for using your argument against you... :-)
+
+If we were to make such aspects part of the profile, then it would seem that we
+should have similar requirements on access-to-subprogram types. That would not
+be strictly necessary, but note that the same sorts of issues apply to calls
+through access-to-subprogram types. These bother me far less (especially as
+wrappers might be required to deal with access-before-elaboration checks), but
+consistency seems valuable.
+
+We could use other somewhat weaker rules. One thing that bothers me about the
+"absolute" rule is that a lot of potentially dispatching routines are never
+called that way in practice. Such routines could have conventional specific
+contract aspects without problems.
+
+One could even imagine using Tucker's original rules (although that leaves
+Steve's problem unsolved) so long as there is the possibility of compile-time
+enforcement of a stricter rule so that at least "well-structured" dispatching
+calls could have their properties known at the call site.
+
+For me, the most important part of contract aspects is that they are known at
+the call site. This opens up the possibility of the compiler eliminating the
+checks (and even more importantly, warning when the contracts are known to fail)
+without having to know anything about the implementation of the subprogram.
+Denying this possibility to dispatching calls makes such calls a second-class
+citizen in the Ada universe, and reduces the contract aspects to little more
+than fancy Assert pragmas (only Type_Invariant does much automatically).
+
+Thus I think we need to reconsider this area. (As a side effect, such
+reconsideration may very well eliminate the problem that Steve was trying to
+fix.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, March 4, 2011  9:43 AM
+
+After thinking more about this, I now agree with Randy that we have a problem.
+It arises whenever an operation inherited from an interface is overridden with
+an operation inherited from some other type.  My conclusion is that it may be
+necessary for a new version of the inherited routine to be generated, so that
+the compiler can insert the additional checks implied by Pre'Class, Post'Class,
+etc. aspects inherited from the interface.
+
+This breaks the principle that you can always just reuse the code when you
+inherit an operation, but I believe in the presence of multiple inheritance of
+class-wide aspects, we don't really have a choice.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, March 4, 2011  9:46 PM
+
+I'm happy to hear that; I'd hate to think that I was making less sense than
+Charlie Sheen...
+
+However, I don't think this quite works, because of the "weakening" rules for
+preconditions. The new precondition inherited from the interface could
+"counterfeit" the precondition on the original body, leading to a scenario where
+the body is called without problem with parameters that violate the precondition
+that it knows about. That seems pretty nasty.
+
+To give a specific example:
+
+    package P1 is
+       type T1 is tagged private;
+       function Is_Valid (Obj : T1) return Boolean;
+       procedure P (Obj : in out T1)
+          with Pre'Class => Is_Valid (Obj);
+    private
+       ...
+    end P1;
+
+    package body P1 is
+       procedure P (Obj : in out T1) is
+       begin
+          -- Code here that assume Is_Valid is True for Obj.
+       end P;
+    end P1;
+
+
+    package P2 is
+       type I2 is interface;
+       function Is_Wobbly (Obj : I2) return Boolean is abstract;
+       procedure P (Obj : in out I2) is null
+           with Pre'Class => Is_Wobbly (I2);
+       function Something_Wobbly return I2
+           when Post'Class => Is_Wobbly (Something_Wobbly'Result);
+    end P2;
+
+    with P1, P2;
+    package P3 is
+       type T3 is new P1.T1 and P2.I2 with private;
+       overriding
+       function Is_Wobbly (Obj : T3) return Boolean;
+       overriding
+       function Something_Wobbly return T3;
+    private
+       ...
+    end P3;
+
+    with P1, P3;
+    procedure Main is
+        procedure Do_It (Obj : in P3.T3'Class) is
+        begin
+           Obj.P; -- (1)
+        end Do_It;
+    begin
+        Do_It (P3.Something_Wobbly);
+    end Main;
+
+Using the new semantics Tucker suggested, the call at (1) has to pass its
+precondition, as Is_Wobbly(Obj) has to be true (based on the postcondition of
+Something_Wobbly). However, since preconditions are effectively combined with
+"or", Is_Valid(Obj) might in fact be False. And if it is, the body of P is going
+to be mighty surprised to get an object that violates its precondition!
+
+(I don't think this problem happens for Post or Type_Invariant, as they are
+"anded", nor would it happen if the precondition was described as a
+Dynamic_Predicate.)
+
+Also note that this "weakening" means that even Pre'Class that necessarily must
+apply to all calls cannot be generated at the call-site (because of the possible
+need to "or" it with some other precondition) -- which eliminates the ability of
+the compiler to do much in the way of checking elimination. (Again, this is not
+a problem with the other aspects.)
+
+It seems that "weakening" doesn't apply to multiple inheritance as much as it
+does to the "primary" inheritance. But that doesn't seem to lead to a rule that
+makes much sense, as it would seem to treat progenitors different than interface
+parents (something we've avoided in the past).
+
+The easy fix would be to combine the preconditions with "and". But I realize
+there are logical issues with that on the call side of the equation. It strikes
+me that there are logical issues on one side or the other whenever contract
+aspects are combined; they only make sense if there is only one.
+
+Thus a radical solution would be to require that exactly one precondition apply
+to each subprogram (either Pre or Pre'Class, possibly inherited). To support
+combining and "weakening", we'd need a way to refer to the aspects of a parent
+routine, so that they can be used in a new Pre aspect. An attribute would work,
+something like: P'Parent_Pre.
+
+That would mean that you couldn't change Pre'Class precondition; if you need to
+do that, you'd have to use a Pre on each subprogram in the inheritance. Not sure
+if that is too complicated. And you couldn't assume much about the calls if you
+did that (rather than using a single Pre'Class), but as that is the current
+state, I can hardly imagine that it is harmful.
+
+Anyway, more thought is needed.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Saturday, March 5, 2011  1:26 AM
+
+> Using the new semantics Tucker suggested, the call at (1) has to pass
+> its precondition, as Is_Wobbly(Obj) has to be true (based on the
+> postcondition of Something_Wobbly). However, since preconditions are
+> effectively combined with "or", Is_Valid(Obj) might in fact be False.
+> And if it is, the body of P is going to be mighty surprised to get an
+> object that violates its precondition!
+
+Doesn't Eiffel have the same problem? How is it handled? (Just trying to avoid
+reinventing the wheel).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, March 5, 2011  2:14 AM
+
+I had wondered the same thing, but am not sure if Eiffel has interfaces or some
+other form of multiple inheritance. (Without that, this particular problem
+cannot come up.)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, March 5, 2011  7:32 AM
+
+Eiffel has multiple inheritance.  Not just interfaces -- you can inherit two
+non-abstract methods that conflict, and there's some syntax for resolving the
+conflict (combine them into one, rename one or both, ....).
+
+I haven't had time to understand the issue you guys are talking about, so I
+don't know how it relates to Eiffel.
+
+One possibly-related thing is that in Eiffel preconditions are checked by the
+caller ("as if", of course).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, March 5, 2011  10:28 AM
+
+Eiffel has full multiple inheritance.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Saturday, March 5, 2011  11:26 AM
+
+> I had wondered the same thing, but am not sure if Eiffel has
+> interfaces or some other form of multiple inheritance. (Without that,
+> this particular problem cannot come up.)
+
+Eiffel has full multiple inheritance (Bertrand Meyer has claimed that no
+language is usable without full multiple inheritance - but that was before
+interfaces)
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent