CVS difference for ai05s/ai05-0247-1.txt
--- ai05s/ai05-0247-1.txt 2011/04/16 07:30:08 1.6
+++ ai05s/ai05-0247-1.txt 2011/04/26 05:39:53 1.7
@@ -1,4 +1,4 @@
-!standard 13.3.2(0/3) 11-04-15 AI05-0247-1/05
+!standard 13.3.2(0/3) 11-04-25 AI05-0247-1/06
!reference AI05-0145-2
!class Amendment 11-03-21
!status work item 11-03-21
@@ -173,10 +173,10 @@
precondition has to be evaluated at this call because the precondition of
Pack3.P3 is weaker (Is_Green(Obj) or Is_Valid(Obj)). Thus we end up checking the
precondition of the actual body in this case, not the weaker precondition of the
-body Pack3.P3. Indeed, the effect is to *and* the preconditions (since we also
-have to check the precondition expected by the interface dispatching call).
-OTOH, a dispatching call using an object of T1'Class does not need to check
-Is_Green at all.
+body Pack3.P3. Indeed, the effect is to *and* the preconditions when called on
+an object of type T2'Class (since we also have to check the precondition
+expected by the interface dispatching call). OTOH, a dispatching call using an
+object of T1'Class does not need to check Is_Green at all.
Since this sort of inheritance always will violate LSP, we don't want the
compiler generating such routines automatically. Thus we introduce a rule
@@ -225,14 +225,63 @@
weaker precondition of the invoked body;
* add a rule to require overriding if the class-wide precondition is
weaker than that of the inherited body(s);
- * change the rules for inherited subprograms that have Post'Class;
- such subprograms are always equivalent to a call on the concrete body (with
- the appropriate postconditions evaluated for that call).
+ * change the rules for inherited subprograms such that there always is
+ an implicit body; this implicit body is always equivalent to a call on the
+ concrete body with appropriate postconditions and invariants
+ evaluated for the new body.
We need a similar rule to the last for Type_Invariant'Class.
!wording
+Modify 3.4(27) as follows:
+
+For [the execution of] a call on an inherited subprogram, {the execution of the
+inherited subprogram is equivalent to the execution of a subprogram_body that
+simply calls} [a call on] the corresponding primitive subprogram of the parent
+or progenitor type {with its formal parameters as the actual parameters and, if
+it is a function, returns the value of the call} [is performed;]{. If there
+is more than one inherited homograph (see 8.3), the call is to the inherited
+subprogram that is neither abstract nor a null procedure, if any; otherwise,
+the call is to an arbitrary one of the null procedures. The}[the] normal
+conversion of each actual parameter to the subtype of the corresponding formal
+parameter (see 6.4.1) performs any necessary type conversion as well. If the
+result type of the inherited subprogram is the derived type, the result of
+calling the subprogram of the parent or progenitor is converted to the derived
+type, or in the case of a null extension, extended to the derived type using the
+equivalent of an extension_aggregate with the original result as the
+ancestor_part and null record as the record_component_association_list.
+
+AARM Ramification: We define calls on inherited subprograms in terms of an
+implicit body that calls the inherited subprogram. This has two effects:
+* The postconditions (see 13.3.2) and type invariants (see 13.3.3) that
+ are evaluated are those that apply to this implicit body; they may include
+ additional expressions from those that apply to the inherited routine if
+ there are multiple ancestors with such routines.
+* When multiple subprograms are inherited, this defines which one is actually
+ called.
+Note that both cases involve inheritance from more than one ancestor. If there
+is only a single parent type, this definition is the same as directly calling
+the inherited routine.
+End AARM Ramification.
+
+Replace 3.9.2(20.3/3) [as replaced by AI05-0126-1 and AI05-0197-1]:
+
+* otherwise, the action is as defined in 3.4 for a call on an
+ inherited subprogram.
+
+Replace the additional AARM note (added by AI05-0197-1) with:
+
+ For the last bullet, if there are multiple corresponding operations for the
+ parent and progenitors, there has to be at least one that is not abstract
+ (if the inherited operations are all abstract, there would have to
+ be an explicit overriding of the operation, and then the first bullet would
+ apply.) In that case, 3.4 defines that the non-null, non-abstract one is
+ called (there can only be one of these); otherwise, an arbitrary null routine
+ is called. (If the inherited operations are all abstract, there would have to
+ be an explicit overriding of the operation, and then the first bullet would
+ apply.)
+
Replace 13.3.2 [from AI05-0145-2] with the following:
[Editor's note: Parts of this wording, including all of the Static Semantics,
@@ -290,56 +339,63 @@
be specified for such a subprogram.]
If two or more homographs (see 8.3) that are subprograms are implicitly
- declared at the same place, and at least one of the homographs is not
- abstract and has a class-wide precondition expression that applies
- that is not the enumeration literal True then then the homographs
- *require overriding* and shall be overridden with a nonabstract subprogram.
+ declared at the same place and at least one of the homographs is not
+ abstract, then the homographs *require overriding* and shall be
+ overridden with a nonabstract subprogram, unless each class-wide
+ precondition that applies to each homograph fully conforms to some
+ class-wide precondition that applies to each other homograph.
-[Editor's note: I borrowed a lot of the above wording from 3.9.3(6/2) and
-8.3(12.1-3/2).]
+ [Editor's note: I borrowed a lot of the above wording from 3.9.3(6/2) and
+ 8.3(12.1-3/2).]
AARM Reason: Such an inherited subprogram would necessarily violate the
Liskov Substitutability Principle (LSP) if called via a dispatching call
- from the "wrong" ancestor. In such a case, the class-wide precondition of
- the actual body is stronger than the class-wide precondition of the
- ancestor. If we did not enforce that precondition for the body, the body
- could be called when the precondition it knows about is False - such
- "counterfeiting" of preconditions has to be avoided. But enforcing the
- precondition violates LSP. We do not want the language to be implicitly
- creating bodies that violate LSP; the programmer can still write an explicit
- body that calls the appropriate parent subprogram. In that case, the
- violation of LSP is explicitly in the code and obvious to code reviewers
- (both human and automated).
-
- If a renaming of a subprogram or entry SE overrides an inherited subprogram
- SI, then the overriding is illegal if SE has a class-wide
- precondition that applies to it that is not the enumeration literal True.
+ from an ancestor other than the one that provides the called body.
+ In such a case, the class-wide precondition of the actual body is stronger
+ than the class-wide precondition of the ancestor. If we did not enforce that
+ precondition for the body, the body could be called when the precondition it
+ knows about is False - such "counterfeiting" of preconditions has to be
+ avoided. But enforcing the precondition violates LSP. We do not want the
+ language to be implicitly creating bodies that violate LSP; the programmer
+ can still write an explicit body that calls the appropriate parent
+ subprogram. In that case, the violation of LSP is explicitly in the code and
+ obvious to code reviewers (both human and automated).
+
+ AARM Ramification: This requires the set of class-wide preconditions that
+ apply to each homograph to be identical. Since full conformance requires
+ each name to denote the same declaration, it is unlikely that independently
+ declared preconditions would conform. This rule does allow "diamond
+ inheritance" of preconditions, and of course no preconditions at all match.
+
+ We considered adopting a rule that would allow examples where the expressions
+ would conform after all inheritance has been applied, but this is complex
+ and is not likely to occur in practice. Since the penalty here is just that
+ an explicit overriding is required, the complexity is too much.
+ End AARM Ramification.
+ [Editor's note: There is more on this topic in the !discussion.]
+
+ If a renaming of a subprogram or entry S1 overrides an inherited subprogram
+ S2, then the overriding is illegal unless each class-wide
+ precondition that applies to S1 fully conforms to some
+ class-wide precondition that applies to S2 and each class-wide
+ precondition that applies to S2 fully conforms to some
+ class-wide precondition that applies to S1.
AARM Reason: Such an overriding subprogram would violate LSP, as
- the precondition of SE would usually be different (and thus stronger)
- than the one known to a dispatching call through an ancestor routine of SI.
- True is the weakest possible precondition, so we can always allow that.
+ the precondition of S1 would usually be different (and thus stronger)
+ than the one known to a dispatching call through an ancestor routine of S2.
+ This is always OK if the preconditions match, so we always allow that.
AARM Ramification: This only applies to primitives of tagged types;
other routines cannot have class-wide preconditions.
+
+ [Editor's note 1: We don't try to modify conformance, as these two are
+ the only checks that we want. We don't want to make other overridings
+ illegal; we don't want any effect on 'Access; we don't want anything to
+ change for generic formal subprograms or renamings other than the above.
-**** Notes for Tucker:
-** We could define "conformant preconditions" and use that instead of "True"
- here (all of the preconditions would have to be conformant). But that is
- complex; it's similar to full conformance, but the homographs from different
- ancestors necessarily will not conform (any subprograms will denote different
- routines as the types are different), even if we make an allowance for
- the different current-instances. I can show an example if you don't
- understand this point. I don't think the complexity is worth it.
-** Also note that the "one-sided" checks above only work for True, so far as
- I can tell. Allowing those specially would add even more to the complexity.
-** I don't see any reason to involve conformance (other than the first
- note here), as these two are the only such checks that we want. We don't
- want to make other overridings illegal; we don't want any effect on
- 'Access; we don't want anything to change for generic formal subprograms
- or renamings other than the above.
-** These rules have nothing to do with postconditions or invariants. See below.
-*** End Tucker notes.
+ [Editor's note 2: These rules have nothing to do with postconditions or
+ invariants. See below.]
Static Semantics
@@ -460,7 +516,6 @@
specific postcondition of the entity applies. Postconditions can always
be evaluated inside the invoked body.
-
If a precondition or postcondition check fails, the exception is
raised at the point of the call. [Redundant: The exception cannot
be handled inside the called subprogram.]
@@ -477,6 +532,13 @@
and we need this rule for dispatching and access-to-subprogram calls
anyway.]
+ For an inherited subprogram, we depend on the definition in 3.4 to provide
+ an implicit body that may have additional postconditions from those that
+ apply to the original subprogram. This may happen if the operation is
+ inherited from a parent and a progenitor, and both the parent operation and
+ progenitor operation have one or more associated postcondition expressions.
+ End AARM Ramification.
+
For a call via an access-to-subprogram value, the class-wide precondition
check is determined by the subprogram or entry actually invoked.
In contrast, the class-wide precondition check for other calls to a subprogram
@@ -494,7 +556,7 @@
AARM Implementation Note: These rules imply that logically, class-wide
preconditions of routines must be checked at the point of call (other
- that for access-to-subprogram calls, which must be checked in the body,
+ than for access-to-subprogram calls, which must be checked in the body,
probably using a wrapper). 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
@@ -504,65 +566,6 @@
for 'Access values.
End AARM Implementation Note.
-
-**** Note to Tucker: The following needs to be replaced by some other rules
-**** for class-wide postconditions and invariants.
-**** Since we don't have any sensible way to describe the situation (this
-**** is a case where the invoked subprogram (if inherited) may have additional
-**** postconditions that need to be evaluated, so the "clean" wording above
-**** does not work.
-**** Moreover, even if we can find a way to describe this for postconditions
-**** (which I grant is possible), I cannot imagine any such wording working
-**** for Type_Invariants (which is a conglomeration of checks).
-**** So I've left this wording until you can come up with a replacement.
-**** (I did prune out the precondition cases.) Enjoy. ;-)
-
- Notwithstanding what this standard says elsewhere, an inherited subprogram S
- (or multiple conformant inherited subprograms) that has one or or more
- class-wide 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
- procedures;
- * A call on the parent subprogram, with all of the parameters the same as the
- parameters to S (possibly with appropriate type conversions on the
- parameters and result if any).
-
- AARM Ramification: This equivalence implies that a dispatching
- call will call this body, rather than that of one of the inherited
- subprograms. This body will enforce all of the postconditions and type
- invariants inherited from all of the ancestors. 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.
-
- [Editor's Note: We really mean "equivalent", as opposed to the standard use
- in the standard when it really means something more like "pretty similar".]
-
- AARM Discussion: Only one implicit overriding subprogram is created for a
- single set of inherited subprograms that are homographs.
-
- AARM Reason: These rules eliminate two potential problems: (1) the issue
- that two null subprograms (one of which is chosen for dispatching
- arbitrarily by 3.9.2(20.3/3)) might have different aspects that apply,
- causing different runtime behavior [note that the Legality Rule requiring
- overriding preconditions also helps solve this problem]; (2) problems that
- arise because postconditions and invariants added by an interface would not
- be enforced on an 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-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 appear to change the dispatching model (even
- though compilers would not need to change in the absence of contract
- aspects).]
-
-**** End wording that is hated by Tucker, but still is the best I can do. :-)
-
-
If the Assertion_Policy in effect at the point of a
subprogram or entry declaration is Ignore, then no precondition or
postcondition check is performed on a call on that subprogram or entry.
@@ -616,22 +619,43 @@
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 that by making 'Access illegal if any significant class-wide
-precondition applies to the subprogram. (We could have used the "implicit body
-model" here as well.) ***??
+types). We fix that treating 'Access differently than a similar dispatching
+call; all of the preconditions are evaluated based on the invoked subprogram.
-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.
+The requirement that preconditions fully conform stems from the need to ensure
+that the preconditions of an inherited body are checked as the body expects. In
+particular, added class-wide preconditions can weaken the precondition, but it
+is unlikely that an existing body is prepared for such weakening. Since actually
+enforcing the preconditions would violate LSP, we instead require the subprogram
+to be overridden in such cases. That way, any violation of LSP is an explicit
+decision by the programmer and not something that happens implicitly by the
+language.
+
+Note that the requirement is that the class-wide preconditions all fully
+conform. This is a tough requirement that cannot be met for independently
+derived preconditions, even if they appear identical. For example:
+
+ type Int1 is interface;
+ function Is_Good (P : Int1) return Boolean is abstract;
+ procedure Foo (Param : Int1) is null
+ with Pre'Class => Is_Good (Param);
+
+ type Int2 is interface;
+ function Is_Good (P : Int2) return Boolean is abstract;
+ procedure Foo (Param : Int2) is null
+ with Pre'Class => Is_Good (Param);
+
+ type Int3 is Int1 and Int2;
+
+6.3.1(21) requires that each direct_name in an expression have to denote the same
+declaration. But in this example, neither Param nor Is_Good denote the same
+declaration in the two preconditions. And these preconditions are what is inherited
+(these are class-wide expressions and they are resolved only once). Thus, type Int3
+is illegal, as procedure Foo requires overriding.
+
!corrigendum 13.3.2(0)
@dinsc
@@ -7047,5 +7071,927 @@
In any case, we can't assume that "it can only be a call to a subprogram [...
which] is itself a primitive of the interface"
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Wednesday, April 6, 2011 3:35 AM
+
+> I don't understand why you care anyway about a concept that
+> necessarily violates LSP. (See my other message.) Class-wide
+> preconditions are intended solely for uses where LSP is preserved. As
+> I noted in my other message, I know think these should be illegal
+> (unless there is a brand-new body involved). Please explain why we
+> should ingrain LSP violations in the language (I think that would be
+> horrible for uses where LSP is required, especially as it would be implicit).
+
+About the LSP:
+It is a Substitution Principle. An object obeys the LSP if it can be used in a
+place where one of his ancestors is expected, without the caller noticing it.
+i.e., if B is an A, you can safely substitute a B for an A. Note that it is
+about objects, not operations.
+
+Of course, to obey the LSP, an object must provide operations whose
+preconditions are weaker and postconditions stronger (won't restate it here).
+
+Note that the LSP is somewhat of an illusion. There has to be some differences
+between A and B, otherwise they would be identical! The whole point is to define
+which differences are "relevant" and which are not. Note also that when it comes
+to real-time, "relevant" properties include WCET, blocking status, etc. To meet
+LSP, the root class must announce a WCET that is worse than any of its
+descendants!
+
+The LSP is useful for HI systems, because it is expected (I am not fully
+convinced, but that is another story) to harness the combinatorial explosion
+implied by pessimistic testing. The approach is two-steps: 1) show that the
+system behaves correctly using only root classes (or prove that pre-conditions
+are sufficient to guarantee correct behaviour of the system), and 2) prove that
+every class obeys the LSP.
+
+Our problem is what kind of support the language should provide. I don't think
+that we should force the LSP on everybody, we had some convincing examples -
+including by you Randy - where it does not apply. My position is that applying
+or not the LSP depends on the project and is a methodological aspect, not a
+language aspect.
+
+From the language point of view, I think the best we can do is to ensure my two
+previous requirements.
+
+The difference between types derived from a tagged type, and types that
+implement an interface, is that the latter do not form a consistent, homogeneous
+set - they gather unrelated types. This observation leads me to a suggestion: do
+not allow Pre'class on interfaces, but allow only Pre. Every implementation of
+an operation would simply have an additionnal Pre, comming (I do not dare say
+inherited) from its interface. It would work the same way we (almost) agreed
+already.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, April 6, 2011 9:20 AM
+
+> Note that the LSP is somewhat of an illusion. There has to be some
+> differences between A and B, otherwise they would be identical!
+
+Yes, that's quite true. It's easy to forget that LSP is not some perfectly
+general principle. It can only work with respect to certain well-understood
+properties.
+
+> Our problem is what kind of support the language should provide. I
+> don't think that we should force the LSP on everybody, we had some
+> convincing examples - including by you Randy - where it does not apply.
+
+Agreed.
+
+I don't think anybody is forcing LSP on anyone. The almost-agreed-upon idea is
+that Pre'Class/Post'Class/Invariant'Class do something like LSP, and
+Pre/Post/Invariant do not.
+
+> My position is that applying or not the LSP depends on the project and
+> is a methodological aspect, not a language aspect.
+
+Agreed. Programmers can choose the 'Class versions, or not.
+
+> The difference between types derived from a tagged type, and types
+> that implement an interface, is that the latter do not form a
+> consistent, homogeneous set - they gather unrelated types. This
+> observation leads me to a suggestion: do not allow Pre'class on
+> interfaces, but allow only Pre.
+
+I'm strongly opposed to this restriction. It's doing exactly what you said you
+didn't want above -- forcing methodological stuff at the language-design level.
+
+It means you can't do anything LSP-like if you use interfaces.
+
+I also strongly object to Ada going its own way, when this stuff has been worked
+out by Eiffel (except for the important distinction between specific and
+class-wide types). Eiffel imposes no such restrictions, and has reasonable
+semantics for class-wide preconditions.
+
+I'd be happy to implement GNAT-specific Restrictions along the lines you
+suggest. Imposing arbitrary restrictions is the business of programmers/project
+leaders, not language designers.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, April 6, 2011 2:06 PM
+
+...
+> Our problem is what kind of support the language should provide. I
+> don't think that we should force the LSP on everybody, we had some
+> convincing examples - including by you Randy - where it does not
+> apply.
+> My position is that applying or not the LSP depends on the project and
+> is a methodological aspect, not a language aspect.
+
+Right. And to that end, Ada is provide both LSP-compliant aspects (Pre'Class,
+etc.) and ones that don't require LSP (Pre, etc.).
+
+> From the language point of view, I think the best we can do is to
+> ensure my two previous requirements.
+
+But those requirements (the second one) denies the use of LSP to interfaces.
+That's not "giving the project the choice to apply LSP"!
+
+> The difference between types derived from a tagged type, and types
+> that implement an interface, is that the latter do not form a
+> consistent, homogeneous set - they gather unrelated types. This
+> observation leads me to a suggestion: do not allow Pre'class on
+> interfaces, but allow only Pre. Every implementation of an operation
+> would simply have an additionnal Pre, comming (I do not dare say
+> inherited) from its interface. It would work the same way we (almost)
+> agreed already.
+
+Pre is not inherited, so there is no possibility of "Pre" coming from it's
+interface. And if we were to add such a thing, we again have to decide how they
+are combined. If they are combined with "and" (which is what you are
+suggesting), you are denying the use of LSP to interfaces.
+
+If anything, it is more important to have LSP for interfaces. LSP is all about
+making it possible to reason about dispatching calls. For regular inheritance,
+there is the possibility of statically bound calls, for which LSP just gets in
+the way. But the only way to use an interface is with dispatching calls.
+
+One can imagine other ways to allow more flexibility on how preconditions
+combine, perhaps by specifying how they combine when the overriding routine is
+defined. (I'm convinced body inheritance cannot be allowed in these cases.) But
+specifying combining adds a lot of complication to the language and its use, so
+I'm dubious that it is a good idea. ("Modern Eiffel" requires that additional
+preconditions be flagged with "else"; this seems like a good idea to me simply
+because remembering that other preconditions are inherited seems difficult. One
+could imagine allowing flagging with other keywords as well. Such flagging could
+be restricted by tools to ensure LSP in such environments.)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, April 6, 2011 10:27 AM
+
+> I'd be happy to write up a new version of AI05-0247-1 to this end, but:
+> (1) I'd be violating the promise of no new wording I made on Friday;
+
+I'm glad you kept that promise! But I'd like to understand this particular rule you propose. You'll have to explain it either in email or during the meeting.
+
+> (2) I'm not certain that enough people agree with this approach to
+> make it worthwhile.
+
+I don't understand the proposal, so I'm not sure. [...pause] OK, Ed just
+clarified for me:
+
+ type T3 is [interface] new T1 and T2;
+
+And suppose both T1 and T2 have operation P ("same" profile).
+
+ If T1 and T2 are interfaces, there's no new restrictions.
+ (We already require overriding P in this case if both
+ P's are abstract, and T3 is concrete.)
+
+ If T3 is abstract (interface or not), then there's no restriction.
+
+The only restriction would be if the P for T1 is a concrete subprogram (so we're
+inheriting a body, and your proposal is to require that body to be overridden).
+
+Is that right? If so, I think it's a reasonable restriction.
+But I also think we ought to be learning what Eiffel does in similar cases.
+Note that in Eiffel, you can actually be inheriting 2 bodies (not possible in
+Ada, other than "null").
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, April 6, 2011 2:25 PM
+
+> > I'd be happy to write up a new version of AI05-0247-1 to this end, but:
+> > (1) I'd be violating the promise of no new wording I made on Friday;
+>
+> I'm glad you kept that promise! But I'd like to understand this
+> particular rule you propose. You'll have to explain it either in
+> email or during the meeting.
+
+OK, it would be something like:
+
+An inherited operation requires overriding if all of the below are true:
+
+* There are two or more inherited homographs with the same defining name and
+ profile; and
+
+* At least one of the inherited homographs is not an abstract subprogram,
+
+* At least one of the inherited homographs has a class-wide precondition or
+ postcondition that is not True or is primitive for a type that has
+ Type_Invariant'Class specified.
+
+> > (2) I'm not certain that enough people agree with this approach to
+> > make it worthwhile.
+>
+> I don't understand the proposal, so I'm not sure. [...pause] OK, Ed
+> just clarified for me:
+>
+> type T3 is [interface] new T1 and T2;
+>
+> And suppose both T1 and T2 have operation P ("same" profile).
+>
+> If T1 and T2 are interfaces, there's no new restrictions.
+> (We already require overriding P in this case if both
+> P's are abstract, and T3 is concrete.)
+>
+> If T3 is abstract (interface or not), then there's no restriction.
+>
+> The only restriction would be if the P for T1 is a concrete subprogram
+> (so we're inheriting a body, and your proposal is to require that body
+> to be overridden).
+>
+> Is that right? If so, I think it's a reasonable restriction.
+
+Yes, but note several things:
+
+* This only applies if class-wide contracts are in use. That's both for
+ compatibility and put no restrictions on non-LSP bodies.
+
+* This applies to any concrete body, including null procedures. Indeed, it was
+ the problems with null procedures that brought up this problem in the first
+ place. If the routines are all abstract, either they require overriding
+ anyway, or there is no problem because they can't be called.
+
+* I didn't put any restrictions on the type, specifically I make the requirement
+ any time that a concrete body is generated. It's possible that the "T3 is
+ abstract case" above could be excluded, but I haven't tried to figure out if
+ that actually works or not.
+
+* The rule could be weaker, since the real requirement is that the class-wide
+ contracts are the same. But defining "the same" is pretty hard, so I didn't
+ try.
+
+* I included the Post'Class and Type_Invariant'Class cases in the rules to fix
+ the problems that they cause. Those problems are more minor and we could
+ automatically make bodies in those cases without much weirdness. But since
+ Tucker didn't like the automatic body rules much anyway, I just made them all
+ "require overriding".
+
+> But I also think we ought to be learning what Eiffel does in similar
+> cases. Note that in Eiffel, you can actually be inheriting 2 bodies
+> (not possible in Ada, other than "null").
+
+I tried figuring that out last month when we initial discussed this, and I
+wasn't able to find anything that discussed the issue in the various references
+that you and Tucker dug up. (I looked for an hour or so.) Everything I saw
+always had a body; I wonder if Eiffel even has body inheritance. (If you never
+have body inheritance, this problem does not come up. And it surely is possible
+to have a shorthand for calling the parent operation which would look somewhat
+like body inheritance but has very different semantics. That is, the bug in Ada
+may be the way it describes dispatching rather than anything to do with
+inheritance per-se.)
+
+Anyway, I don't think I'm going to spend more time trying to figure out what
+Eiffel does; if someone else can find a reference, I'd surely be interested in
+reading about it.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, April 7, 2011 8:10 AM
+
+>> The difference between types derived from a tagged type, and types
+>> that implement an interface, is that the latter do not form a
+>> consistent, homogeneous set - they gather unrelated types. This
+>> observation leads me to a suggestion: do not allow Pre'class on
+>> interfaces, but allow only Pre.
+>
+> I'm strongly opposed to this restriction. It's doing exactly what you
+> said you didn't want above -- forcing methodological stuff at the
+> language-design level.
+
+I don't see why.
+But there is another more important reason to keep Pre'Class: it has to apply
+interfaces derived from other interfaces. I withdraw the suggestion (pending
+tonight's discussion)
+
+> It means you can't do anything LSP-like if you use interfaces.
+
+No. It means that if you want to support LSP, and you have to repeat the
+pre-condition from the interface in your implementing subprograms.
+
+> I also strongly object to Ada going its own way,
+
+I strongly agree with that
+
+> when this
+> stuff has been worked out by Eiffel (except for the important
+> distinction between specific and class-wide types). Eiffel imposes no
+> such restrictions, and has reasonable semantics for class-wide
+> preconditions.
+
+I could not find anything about what happens when several preconditions are
+inherited in parallel. All I could find is the usual weakening/strengthening for
+linear inheritance. I'd be glad if you had a reference.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, April 7, 2011 8:30 AM
+
+> But those requirements (the second one) denies the use of LSP to interfaces.
+> That's not "giving the project the choice to apply LSP"!
+
+I repeat it here:
+
+> 2) When the body is called (which in general is not an A), all
+> applicable preconditions (wheter class-wide or specific) are met, or
+> Assertion_Error is raised.
+
+If you don't agree with this, it means that you are happy if a body gets called
+with some of its preconditions false. ?????
+
+-----
+In order to save time for the discussion, let me summarize what I think we all
+agree on:
+
+1) Pre is independent from Pre'Class, and has nothing to do with the LSP.
+
+2) When a tagged type (or interface) is derived from a single type (or
+ interface), and has preconditions, these preconditions are "ored" with those
+ of the parent. (TBH: not sure when a tagged type is derived from only one
+ interface)
+
+-----
+The issue is when a tagged type has multiple progenitors. Let's have:
+
+A root tagged type RTT;
+A root interface RI;
+A derived interface DI (derived from RI);
+
+each with a primitive operation OP, and preconditions are specified for OP by
+each.
+
+Now, have a derived type DT is new RTT and DI;
+
+How are the various preconditions combined if
+1) OP is overriden (with its own preconditions)
+2) OP is not overriden
+
+My suggested formula is:
+(PRE'Class(RTT) or PRE'Class(DT)) and (PRE'Class(RI) or PRE'Class(DI))
+
+i.e.: "or" for serial inheritance, "and" for parallel inheritance
+
+Please provide your alternative formulas! (including what's provided by other
+languages if you know about)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, April 7, 2011 8:50 AM
+
+> How are the various preconditions combined if
+> 1) OP is overriden (with its own preconditions)
+> 2) OP is not overriden
+>
+> My suggested formula is:
+> (PRE'Class(RTT) or PRE'Class(DT)) and (PRE'Class(RI) or PRE'Class(DI))
+>
+> i.e.: "or" for serial inheritance, "and" for parallel inheritance
+>
+> Please provide your alternative formulas! (including what's provided
+> by other languages if you know about)
+
+Disjunction, aka "or", between all is the standard, I believe.
+See the article I referenced (and quoted in my prior e-mai).
+Also, in Eiffel, as explained in:
+ http://docs.eiffel.com/book/method/et-inheritance#Join_and_uneffecting
+
+Join and uneffecting
+
+It is not an error to inherit two deferred features from different parents under
+the same name, provided they have the same signature (number and types of
+arguments and result). In that case a process of feature join takes place: the
+features are merged into just one -- with their preconditions and
+postconditions, if any, respectively or-ed and and-ed.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, April 7, 2011 9:12 AM
+
+> > But those requirements (the second one) denies the use of LSP to interfaces.
+> > That's not "giving the project the choice to apply LSP"!
+>
+> I repeat it here:
+> > 2) When the body is called (which in general is not an A), all >
+> applicable preconditions (wheter class-wide or specific) are met, or
+> > Assertion_Error is raised.
+> If you don't agree with this, it means that you are happy if a body
+> gets called with some of its preconditions false. ?????
+
+Yes, I am happy with that. So are Tucker, Randy, B. Meyer, etc. ;-)
+
+That's what "or" means -- I am happy that "Foo or Bar" is True, even though Foo might be False, and Bar might be False.
+
+> -----
+> In order to save time for the discussion, let me summarize what I
+> think we all agree on:
+>
+> 1) Pre is independent from Pre'Class, and has nothing to do with the LSP.
+>
+> 2) When a tagged type (or interface) is derived from a single type (or
+> interface), and has preconditions, these preconditions are "ored" with
+> those of the parent.
+
+Yes, I think we all agree on the above.
+
+>... (TBH: not sure when a tagged type is derived from only one
+>interface)
+
+I'm pretty sure interfaces shouldn't be special here.
+
+> -----
+> The issue is when a tagged type has multiple progenitors. Let's have:
+>
+> A root tagged type RTT;
+> A root interface RI;
+> A derived interface DI (derived from RI);
+>
+> each with a primitive operation OP, and preconditions are specified
+> for OP by each.
+>
+> Now, have a derived type DT is new RTT and DI;
+>
+> How are the various preconditions combined if
+> 1) OP is overriden (with its own preconditions)
+> 2) OP is not overriden
+>
+> My suggested formula is:
+> (PRE'Class(RTT) or PRE'Class(DT)) and (PRE'Class(RI) or PRE'Class(DI))
+>
+> i.e.: "or" for serial inheritance, "and" for parallel inheritance
+
+IMHO "and" should be "or".
+
+> Please provide your alternative formulas! (including what's provided
+> by other languages if you know about)
+
+Yes, the above is a good description of the issue (although you don't need RI to
+illustrate the issue). Let me write it out in code:
+
+ package P1 is
+ type RTT is tagged ...;
+ procedure OP(X: RTT) with Pre'Class => Is_Green(X);
+ end P1;
+
+ package P2 is
+ type RI is interface;
+ procedure OP(X: RI) with Pre'Class => Is_Blue(X) is abstract;
+ end P2;
+
+ package P3 is
+ type DI is new RI;
+ overriding procedure OP(X: DI) with Pre'Class => Is_Red(X) is abstract;
+ end P3;
+
+ package P4 is
+ type DT is new RTT and DI;
+ overriding procedure OP(X: DT) with Pre'Class => Is_Purple(X);
+ end P4;
+
+ package body P4 is
+ overriding procedure OP(X: DT) with Pre'Class => Is_Purple(X) is
+ begin
+ -- Here, we can assume
+ -- Is_Green(X) or Is_Blue(X) or Is_Red(X) or Is_Purple(X).
+ ...
+ end OP;
+ end P4;
+
+(with's and use's omitted above)
+
+ with P2;
+ procedure Client (X : P2.RI'Class) is
+ begin
+ if Is_Blue(X) then
+ P2.OP(X); -- dispatch
+ end if;
+ end Client;
+
+Now suppose Client is passed X'Tag = DT'Tag.
+But Client has never heard of RTT, DI, or DT.
+It correctly checks the only precondition it knows about (Is_Blue), which
+ensures that when we get to the body of OP, the precondition "Is_Green(X) or
+Is_Blue(X) or Is_Red(X) or Is_Purple(X)" is True. If that body blows up when
+Is_Green is True but Is_Red is False, that's bad, because there's no way the
+Client could have known about that.
+
+If you don't like that, then you can use Pre instead of Pre'Class, and use some
+other means to prove things won't fail. That other means will necessarily break
+abstraction, which may or may not be OK.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, April 7, 2011 11:55 AM
+
+...
+> In order to save time for the discussion, let me summarize what I
+> think we all agree on:
+>
+> 1) Pre is independent from Pre'Class, and has nothing to do with the
+> LSP.
+>
+> 2) When a tagged type (or interface) is derived from a single type (or
+> interface), and has preconditions, these preconditions are "ored" with
+> those of the parent. (TBH: not sure when a tagged type is derived from
+> only one interface)
+
+Right.
+
+> -----
+> The issue is when a tagged type has multiple progenitors. Let's have:
+>
+> A root tagged type RTT;
+> A root interface RI;
+> A derived interface DI (derived from RI);
+>
+> each with a primitive operation OP, and preconditions are specified
+> for OP by each.
+>
+> Now, have a derived type DT is new RTT and DI;
+>
+> How are the various preconditions combined if
+> 1) OP is overriden (with its own preconditions)
+> 2) OP is not overriden
+>
+> My suggested formula is:
+> (PRE'Class(RTT) or PRE'Class(DT)) and (PRE'Class(RI) or PRE'Class(DI))
+>
+> i.e.: "or" for serial inheritance, "and" for parallel inheritance
+>
+> Please provide your alternative formulas! (including what's provided
+> by other languages if you know about)
+
+I've done this repeatedly, but you don't seem to read it.
+
+They all have to "or"ed together. Anything else violates LSP a-priori (unless
+the preconditions are exactly the same). I've explained why in a previous
+message, I don't have time to repeat that before the call.
+
+Implementation inheritance cannot work in this case (whether you use "and"
+or "or"!!). Thus is it banned (you must provide an overriding). I think you are
+trying to make implementation inheritance work, but any rule you choose will
+fail at least one of the requirements (usually more than one).
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, April 7, 2011 10:28 AM
+
+> To put it another way: If type T inherits from interface I, it is
+> promising that any dispatching call via I'Class will not blow up. And
+> that's true for each such I. Therefore, the precondition of T must be
+> the same as, or weaker than, the precondition of each such I.
+
+I agree. That's what the programmer should ensure. But what if he doesn't?
+
+We are not giving advice to programmers here; we are defining language rules.
+Here is the problem:
+
+I has precondition PI.
+
+T has precondition PT, which, as stated by the programmer, is not weaker that
+PI.
+
+What happens? I see three possibilities:
+1) Statically require PT to be weaker that PI => compile_time error.
+Best for LSP, but I doubt we want to go that far.
+
+2) Decide that the effective precondition for the call is PI or PT. This implies
+that the subprogram can be called with its own, specified, explicit precondition
+false. That's what I don't like - although proof making tools will consider the
+effective precondition. But I'm afraid that manual inspection is very likely to
+miss the implicit "oring". Eiffel solves this by requiring the "else", which
+acts as a reminder to the reader.
+
+3) When called from I'class, check PT and raise Assertion_Error if it does not
+hold. That's the dynamic version of 1), but is in effect "and".
+
+As I write this, I think I could live with 2) provided:
+- there is special syntax (as in Eiffel)
+- if there is no inherited precondition, forbid precondition on the implementing
+ implementations (that is the case where 1) is easily implementable).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, April 7, 2011 12:01 PM
+
+This has to be statically illegal (technically, require overriding). The
+compiler should not be in the business of automatically building bodies that
+violate LSP (and this case is always an implicit body).
+
+****************************************************************
+
+From: John Barnes
+Sent: Thursday, April 7, 2011 5:04 AM
+
+Oh dear. When I was writing the intro to the rat and wrote "There are also
+aspects Pre'Class and Post'Class for use with tagged types", I thought "I fear
+there is trouble ahead".
+
+What to do? Certainly don't mess up the plain Pre. Make the class ones distinct.
+Possibilities are
+
+1 Give it up until next time
+
+2 Have two different attributes for preconditions
+
+3 Could have two for post as well for symmentry but make them the same
+
+4 Use a temporary name so that it can be made redundant next time when a better
+ solution is found eg Pre'Classtemp, Pre'Crass, Pre'Mix, Pre'Concrete,
+ Pre'Monition...
+
+Hmm. Better read the next one.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, April 6, 2011 9:25 AM
+
+General comment about "contract" stuff:
+
+Anybody who wants to do things differently from the way Eiffel works should: (1)
+understand the Eiffel rules, and (2) present concrete reasons why Ada should be
+different.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, April 6, 2011 9:50 AM
+
+Here is a good paper on this whole topic, as it relates to JML, Java Modeling
+Language, which was inspired by Eiffel and Larch. It talks about "behavioral
+subtyping" which is pretty much what we are arguing about:
+
+ http://www.eecs.ucf.edu/~leavens/JML/fmco.pdf
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, April 7, 2011 7:03 AM
+
+Thanks, good paper, I read it on the train last night.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, April 7, 2011 7:33 AM
+
+I found it quite disappointing, as far as our problem is concerned. It does not
+address the case when you inherit from a class and an interface (both with
+preconditions).
+
+***************************************************************
+
+From: Tucker Taft
+Sent: Thursday, April 7, 2011 8:28 AM
+
+It covers that case in the following (from page 12), I believe:
+
+The meaning of specification cases conjoined by also can be a bit subtle.
+However, it is easiest to just keep in mind that all specification cases of all
+inher- ited methods have to each be obeyed by a method. If, for a given method,
+the subtype and supertypes all specify the same precondition and assignable
+clause, then the conjoined specification will be equivalent to a single
+specification case whose precondition and assignable clause are the same as in
+the individual spec- ification cases, and with a postcondition that is the
+conjunction of the postcon- ditions in the individual specification cases. If
+different preconditions are given in a sub- and supertype the meaning of the
+conjoined specification cases is more involved: the precondition of the
+conjoined specification will effectively be the disjunction of the preconditions
+from the individual specification cases, and the postcondition of the conjoined
+specification will effectively be a conjunction of implications, where each
+precondition (wrapped in \old()) implies the corre- sponding postcondition. This
+effective postcondition is slightly weaker than the conjunction of the
+postconditions, since each postcondition only has to apply in case the
+corresponding precondition was satisfied [DL96].
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, April 7, 2011 8:51 AM
+
+> It covers that case in the following (from page 12), I believe:
+
+Not to my understanding (but I may understand wrong)
+
+> The meaning of specification cases conjoined by also can be a bit
+> subtle. However, it is easiest to just keep in mind that all
+> specification cases of all inher- ited methods have to each be obeyed
+> by a method.
+
+If we interpret that as multiple inherited preconditions, it would mean that
+they are "anded".
+
+> If, for a given method, the subtype and supertypes all specify the
+> same precondition and assignable clause, then the conjoined
+> specification will be equivalent to a single specification case whose
+> precondition and assignable clause are the same as in the individual
+> spec- ification cases, and with a postcondition that is the
+> conjunction of the postcon- ditions in the individual specification cases.
+
+That's trivially the case when there is no problem
+
+> If
+> different preconditions are given in a sub- and supertype the meaning
+> of the conjoined specification cases is more involved: the
+> precondition of the conjoined specification will effectively be the
+> disjunction of the preconditions from the individual specification
+> cases,
+
+Note that here, supertype is now singular.
+And it talks about disjunction of the "individual specification cases".
+I don't get exactly what it means.
+
+[...] stuff about postconditions stripped
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, April 7, 2011 8:53 AM
+
+> It covers that case in the following (from page 12), I believe:
+
+Right. And the important point is there is not even a hint that one might want
+to treat interfaces differently from (abstract) classes.
+
+There is an added complication in the paper, because their language supports the
+"also" thing, which allows multiple independent preconditions with corresponding
+postconditions, as in "you must obey precondition A or B, and if you obey A but
+not B, you must ensure X, and if you obey B but not A, you must ensure Y". We
+don't have that feature in Ada 2012.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, April 7, 2011 9:03 AM
+
+>> If
+>> different preconditions are given in a sub- and supertype the meaning
+>> of the conjoined specification cases is more involved: the
+>> precondition of the conjoined specification will effectively be the
+>> disjunction of the preconditions from the individual specification
+>> cases,
+> Note that here, supertype is now singular.
+
+It says "a ... supertype" not "the supertype".
+
+> And it talks about disjunction of the "individual specification
+> cases". I don't get exactly what it means.
+
+"Disjunction" means "or" ("conjunction" means "and").
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, April 7, 2011 9:05 AM
+
+> Right. And the important point is there is not even a hint that one
+> might want to treat interfaces differently from
+> (abstract) classes.
+
+That's not the point. It's about what happens if you inherit in parallel (but of
+course, only interfaces can be inherited in parallel)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, April 7, 2011 9:20 AM
+
+> That's not the point.
+
+It's exactly the point. In the following two cases:
+
+ type A is interface with Pre => ...;
+ type B is new A with Pre => ...;
+ type C is new B with Pre => ...;
+
+ type A is interface with Pre => ...;
+ type B is interface with Pre => ...;
+ type C is new A and B with Pre => ...;
+
+C should end up with identical semantics in both cases.
+In both cases, it gets preconditions from A and B, and those preconditions need
+to be "or"ed in both cases.
+
+>...It's about what happens if you inherit in parallel (but of course,
+>only interfaces can be inherited in parallel)
+
+There's no "of course" about it. Ada and Java have that restriction, but Eiffel
+does not.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, April 7, 2011 9:28 AM
+
+I trust you saw the quote from the Eiffel manual where they clearly say when
+"joining" preconditions from multiple super classes, you use "or".
+
+The point is that the precondition is what is required of the caller, and if you
+combine two interfaces, one of which has no preconditions, then a caller through
+that interface should not be surprised by some precondition imposed after the
+fact. The bug is with the programmer who believes their type can "implement" an
+interface, but in fact they can't live with the minimal precondition imposed by
+that interface on its callers. That is the Eiffel model, and that is what we
+are proposing for "Pre'Class."
+
+Implementing an interface means living with the Pre'Class preconditions
+inherited from that interface as well as all of the others, which may mean
+"living with" a "True" precondition over all.
+
+****************************************************************
+
+From: John Barnes
+Sent: Thursday, April 7, 2011 9:13 AM
+
+> There is an added complication in the paper, because their language
+> supports the "also" thing, which allows multiple independent
+> preconditions with corresponding postconditions, as in "you must obey
+> precondition A or B, and if you obey A but not B, you must ensure X,
+> and if you obey B but not A, you must ensure Y". We don't have that
+> feature in Ada 2012.
+
+Presumably one could have two differently named subprograms inheriting different
+conditions. Hmm maybe not.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, April 7, 2011 9:38 AM
+
+Yes. But the case we're arguing about is the (somewhat unusual) case where you
+inherit the same procedure from two different parents. Never mind LSP (which is
+semi-bogus, IMHO) -- the point is that the clients of one of those parents
+doesn't know about the other one, and vice versa. Therefore, the body of that
+procedure cannot assume that BOTH preconditions are true -- it can only assume
+that one or the other is true. Because a dispatching call can come from 'Class
+of either parent.
+
+And this has nothing to do with interfaces -- if both parents are interfaces or
+(if Ada allowed it) both parents are not, the argument would be the same.
+
+To put it another way: If type T inherits from interface I, it is promising
+that any dispatching call via I'Class will not blow up. And that's true for
+each such I. Therefore, the precondition of T must be the same as, or weaker
+than, the precondition of each such I. Hence, "or".
+
+>... Hmm maybe not.
+
+Definitely so. ;-)
+
+I really think that the burden of proof should be on those who want to violate
+the rules of Eiffel or JMI!
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, April 7, 2011 9:45 AM
+
+For what it is worth, I am sympathetic with Randy's proposal that you must
+override under certain circumstances.
+
+Basically I would say that if you inherit a non-abstract, non-null body from the
+parent type, and it has a Pre'Class that is not merely "True", then unless all
+of the other Pre'Class's for that operation (inherited from progenitors) fully
+conform to some Pre'Class already included in the Pre'Class "disjunction" for
+the parent's subprogram, the subprogram must be overridden in the derived type.
+
+This forces the programmer to reckon with the situation explicitly, rather than
+just being surprised by the fact that the precondition has been weakened. Of
+course the implementation of the overriding operation could be a simple call of
+the parent's operation, but at least we know then that the programmer explicitly
+decided that was OK.
+
+From the compiler's point of view, if the programmer isn't forced to do this,
+the compiler probably will have to do it (that is, create a wrapper), since it
+might be assuming that certain preconditions had been checked, and if they
+haven't, it might have to generate the code for the operation again, and it
+might give additional warnings about likely check failures, etc.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, April 7, 2011 9:54 AM
+
+I can go along with that.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, April 7, 2011 9:58 AM
+
+> > I also strongly object to Ada going its own way,
+
+> I strongly agree with that
+
+Then you have to agree with "or" for preconditions.
****************************************************************
Questions? Ask the ACAA Technical Agent