CVS difference for ai05s/ai05-0197-1.txt
--- ai05s/ai05-0197-1.txt 2011/03/18 00:11:53 1.5
+++ ai05s/ai05-0197-1.txt 2011/04/02 07:30:36 1.6
@@ -316,7 +316,8 @@
> 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.
+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.
@@ -412,362 +413,7 @@
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).
+[Editor's note: Discussion of Problem #2 continues in AI05-0247-1.]
****************************************************************
-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