CVS difference for ai05s/ai05-0247-1.txt
--- ai05s/ai05-0247-1.txt 2011/03/26 06:04:32 1.3
+++ ai05s/ai05-0247-1.txt 2011/03/29 07:13:55 1.4
@@ -1,4 +1,4 @@
-!standard 13.3.2(19/3) 11-03-25 AI05-0247-1/03
+!standard 13.3.2(19/3) 11-03-28 AI05-0247-1/04
!reference AI05-0145-2
!class Amendment 11-03-21
!status work item 11-03-21
@@ -62,7 +62,7 @@
with Pack1, Pack3;
procedure Main is
- procedure Do_It (Obj : in Pack3.T3'Class) is
+ procedure Do_It (Obj : in out Pack3.T3'Class) is
begin
Obj.P1; -- (1)
Obj.P2; -- (2)
@@ -87,9 +87,9 @@
point. (This would require nothing more than the compiler generating a wrapper
at this point.) But that brings up a new problem. Consider the following:
- with Pack1, Pack2, Pack3;
+ with Pack2, Pack3;
procedure Main2 is
- procedure Do_It (Obj : in Pack2.T2'Class) is
+ procedure Do_It (Obj : in out Pack2.T2'Class) is
begin
Obj.P3; -- (3)
end Do_It;
@@ -150,7 +150,7 @@
Is_Green at all.
Note that if we are using Pre rather than Pre'Class, then the preconditions of
-a dispatching call need have any real relationship. In that case, the existing
+a dispatching call need not have any real relationship. In that case, the existing
rules are as good as any, and they have the advantage of working the same way
for access-to-subprogram calls.
@@ -173,9 +173,11 @@
Finally, the wording given in AI05-0145-2 makes it clear that Pre and Post are
not inherited. However, nothing is said about what happens to these when a
-subprogram is inherited. With the AI05-0145-2 wording, it appears. Clearly, we
-want to evaluate the Pre and Post values associated with a subprogram when that
-subprogram is inherited.
+subprogram is inherited. With the AI05-0145-2 wording, it appears that there is
+no inheritance of Pre and Post. Clearly, we want to evaluate the Pre and Post
+values associated with a subprogram when that subprogram is inherited, otherwise
+the body of the subprogram could be called without the preconditions it is
+expecting.
Thus we need to make four changes:
@@ -197,12 +199,11 @@
Add at the end of 3.10.2(32/2):
If P has one or more class-wide precondition expressions that apply to it, at least
-one of those expressions shall be the enumeration literal True.
+one of those expressions shall statically denote the Boolean enumeration literal True.
-AARM Reason: An access to access-to-subprogram type does not have a class-wide
-precondition; that means no such precondition will be checked. This rule
-prevents a routine with a stronger class-wide precondition from being supplied,
-as it would not be enforced.
+AARM Reason: An access-to-subprogram type does not have a class-wide precondition; that
+means no such precondition will be checked. This rule prevents a routine with a stronger
+class-wide precondition from being supplied, as it would not be enforced.
Modify 13.3.2(2-5/3):
@@ -263,12 +264,12 @@
* The specific precondition check begins with the evaluation of the specific
precondition expression that applies to the subprogram or entry; if the
- expression evaluates to False, Ada.Assertions.Assertion_Error is raised.
+ expression evaluates to False, Assertions.Assertion_Error is raised.
* The class-wide precondition check begins with the evaluation of any class-wide
precondition expressions that apply to the subprogram or entry. If and only if
all the class-wide precondition expressions evaluate to False,
- Ada.Assertions.Assertion_Error is raised.
+ Assertions.Assertion_Error is raised.
AARM Ramification: The class-wide precondition expressions of the entity itself
as well as those of any parent or progentitor operations are evaluated, as these
@@ -304,7 +305,7 @@
If the Assertion_Policy in effect at the point of a subprogram or entry
declaration is Check, then upon successful return from a call of the subprogram
or entry, prior to copying back any by-copy in out or out parameters, the
-postcondition checks is performed. This consists of the evaluation of the
+postcondition check is performed. This consists of the evaluation of the
specific and class-wide postcondition expressions that apply to the subprogram
or entry. If any of the postcondition expressions evaluate to False, then
Ada.Assertions.Assertion_Error is raised. The order of performing the checks is
@@ -336,7 +337,7 @@
AARM Ramification: This applies to access-to-subprogram calls, dispatching calls,
and to statically bound calls. We need this rule to cover statically bound calls
-as well, as Pre preconditions and Post postconditions are not inherited, but the
+as well, as specific pre- and postconditions are not inherited, but the
subprogram might be. [Editor's note: Wording to define aspect inheritance only in
non-overriding situations seems to be way too complex -- and we need this rule
for dispatching and access-to-subprogram calls anyway.]
@@ -367,35 +368,39 @@
or has a specified Type_Invariant'Class (see 13.3.3),
that is not explicitly overridden, and that is primitive for a type that has one
or more progenitors is equivalent to an overriding subprogram S whose body consists of:
- * The null statement, if all of the inherited subprograms are null subprograms;
+ * 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).
+ the parameters to S (possibly with appropriate type conversions on the parameters
+ and result if any).
If a subprogram renaming overrides one or more inherited subprograms, the renaming
-is equivalent of an subprogram whose body calls the renamed subprogram, with all
+is equivalent of a subprogram whose body calls the renamed subprogram, with all
of the parameters the same as the parameters to S (possibly with appropriate type
-conversions).
+conversions on the parameters and result if any).
-AARM Ramification: We really mean equivalent here! The call on the parent
-subprogram will evaluate preconditions as needed. And a dispatching call will
+AARM Ramification: This equivalence implies that the call on the parent
+subprogram will evaluate preconditions as needed. And that a dispatching call will
call this body, rather than that of one of the inherited subprograms. Note that
if the routines are not all null, then the subprogram inherited for the parent
type must be concrete (not abstract or null), so that is the one we want to call.
+[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 homoegraphs.
+set of inherited subprograms that are homographs.
-AARM Reason: These rules eliminates four problems: (1) the issue that two
+AARM Reason: These rules eliminate four potential problems: (1) the issue that two
null subprograms (one of which is chosen for dispatching arbitrarily by
-3.9.2(20.3/3)) may not be equivalent at runtime; (2) "counterfeiting" problems
-that arise because adding an interface precondition to the mix weakens the
-class-wide precondition of the inherited routine (in this case, we need to
-enforce the class-wide precondition of the actual body, else it might not be
-true when the call is made -- which would be bad); (3) problems that arise
-because postconditions and invariants added by an interface would not be
-enforced on a inherited routine (it does not know about any such contracts);
+3.9.2(20.3/3)) might have different aspects that apply, causing different runtime
+behavior; (2) "counterfeiting" problems that arise because adding an interface
+precondition to the mix weakens the class-wide precondition of the inherited routine
+(in this case, we need to enforce the class-wide precondition of the actual body,
+else it might not be true when the call is made -- which would be bad); (3) problems
+that arise because postconditions and invariants added by an interface would not be
+enforced on an inherited routine (it does not know about any such contracts);
(4) problems with the "wrong" class-wide precondition being enforced
-for an overriding rename of a routine that has it's own class-wide
+for an overriding rename of a routine that has its own class-wide
precondition.
[Editor's note: We do not need to talk about this in single inheritance
@@ -403,7 +408,7 @@
that case. We do not need to talk about this unless there is a class-wide aspect
involved because other aspects (Pre, Post, Type_Invariant) are not inherited.
We could have made this apply to all inheritance of routines that can have
-class-wide aspects, but we didn't do that as that would appears to change the
+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).]
@@ -412,7 +417,7 @@
This issue originally came up because null procedures are considered the same
when inherited, so a dispatching call may call an arbitrary one. That however,
does not work if the null procedures have different preconditions,
-postconditions, or type_invariants -- that case, the routines are
+postconditions, or type_invariants -- in that case, the routines are
distinguishable. The solution here has to address this case as well as the more
general problems of inheritance.
@@ -431,22 +436,16 @@
The change to separate Pre from Pre'Class introduces additional problems with
renames and 'Access. Since renaming can change the dispatching status of a
subprogram (from dispatching to statically bound, or the reverse), it introduces
-some interesting problems.
+some interesting problems. This is fixed by applying the "implicit body model" to
+overriding renames.
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).
+(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.)
-We fix these both by including Pre'Class in conformance checking, such that
-subprograms don't match if the Pre'Class precondition(s) that apply to the
-subprogram are not equivalent (fully conformant). But we don't want a condition
-this strong for overriding (we want to be able to weaken the precondition
-with additional Pre'Class items) [although I cannot think of
-any case in practice when a weaker precondition would be what you want - RLB],
-so this rule does not apply to overriding.
-
-
We could have solved the Pre/Post inheritance problem by changing the model of
inheritance in Ada to always generate an implicit body as in the wording proposed
at the end of the AI. As well as solving that problem, it also would simplify the
@@ -3246,3 +3245,1697 @@
concentrating on the wording changes needed. Now back to pragmas => aspects.
****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 26, 2011 5:20 AM
+
+>> Cyrille from AdaCore finds the whole Pre'Class inheritance "or"-ing
+>> thing unpleasant, and I think there are others who might have the
+>> same view, and it seems potentially a benefit if Pre and Pre'Class
+>> are treated independently.
+
+I also dislike the Pre'Class oring!
+And I definitely think they should be treated independently.
+You really want to be able to specify Pre that means what it says, and not have
+it intefered with by peculiar incomprehensible (to me and others) oring.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 26, 2011 5:21 AM
+
+> The model that Tucker and I have been discussing is that for such
+> inherited subprograms, the semantics is as if there was an explicit
+> body for the routine (complete with the expected postcondition checks,
+> if you are doing them inside of the body), which just calls the parent
+> routine. This seems to be about as hard to implement as the other
+> cases where you have to generate a wrapper for a tag or a use of
+> 'Access, so I don't think there can be a major implementation problem.
+
+At first reading, sounds reasonable, to be investigated
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 26, 2011 5:22 AM
+
+> Actually adding the additional postcondition checks isn't that hard,
+> it just means creating a wrapper. But Randy's point was that such a
+> wrapper cannot raise an exception that could be handled inside the
+> body it is wrapping! But who cares, since we don't want the exception
+> to be handle-able anyway.
+
+Yes, sounds ok
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 26, 2011 5:22 AM
+
+> P.S. I think we should at least ALLOW preconditions to be checked at
+> the call site.
+
+of course ... no one suggested otherwise, we can't handle the exceptions within
+the body, everyone agrees on that.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, March 26, 2011 10:28 AM
+
+> I don't understand why you only are worrying about renames-as-body here.
+> Doesn't renames-as-declaration have the same problem? An overriding is
+> not a completion, after all, it is a new declaration of a homograph.
+>
+> The problem in question is renaming a routine that has one or more
+> class-wide preconditions as an overriding of another routine that has
+> one or more different class-wide preconditions. We can only allow
+> weakening, but this is not likely to be that. I don't see any reason
+> that you can't use a renames-as-declaration in such a context.
+>
+> ("Class-wide preconditions" is the nice name I gave Pre'Class in my
+> wording proposal - trying to talk about Pre'Class separately from Pre
+> is beyond what I can do wording-wise.)
+>
+> If that's the case, modifying subtype conformance does not do the
+> trick, since renames-as-declaration only needs mode-conformance. We
+> probably need separate legality rules in that case. ...
+
+Subtype conformance is required when overriding an inherited dispatching
+operation, per 3.9.2(10/2). This rule is independent of whether the overriding
+is by a simple declaration or by a renaming.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 11:52 PM
+
+OK, but that's the case where we can't change subtype conformance, because we
+want to be able to add additional an Pre'Class to weaken the precondition. So
+that doesn't help any.
+
+But no matter, I gave up completely on this conformance model in the draft AI I
+created. Changing conformance has the potential of causing weird effects for
+formal subprograms and it doesn't seem worth the hassle, especially as the
+"implicit body" model fixes the renames problems just as cleanly as it fixes the
+three other odditities.
+
+So I just wrote an explicit legality rule for 'Access, and a bit of wording to
+invoke the "implicit body" model for any overriding rename, and we're all set.
+
+At least until you try to replace the "mechanistic" "implicit body" wording with
+something prettier but fiendishly complex. :-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 11:40 PM
+
+[Editor's note: On Monday morning, Bob Duff sent a message that quoted the
+entire 30K+ AI in order to make a number of typo corrections and wording
+improvements. These have all been addressed in version /04, except for
+a few below that are mentioned in the following mail: ">>" is the original
+AI wording, ">" is Bob's comments, and unquoted stuff is this reply.]
+
+> > !standard 13.3.2(19/3) 11-03-25
+> > AI05-0247-1/03
+>
+> Thanks for writing this up. I haven't (yet?) read the long discussion
+> that led up to this, but I've got a bunch of (mostly editorial)
+> comments below.
+
+And thanks for reading this and making an attempt to understand it.
+
+> I have a feeling we're re-treading the same ground covered by Meyer /
+> Eiffel.
+
+Probably, but Ada also has legacy issues that aren't necessarily present in
+Eiffel. In particular, we have to do something useful for existing code that
+doesn't have preconditions defined.
+
+> I think this AI addresses some major concerns I had several months ago
+> (but never got around to bringing up, because I didn't fully
+> understand the issues).
+
+Good to hear.
+
+...
+> > with Pack1, Pack2;
+> > package Pack3 is
+> > type T3 is new Pack1.T1 and Pack2.I2 with private;
+> > overriding
+> > function Is_Green (Obj : T3) return Boolean;
+> > overriding
+> > procedure P2 (Obj : in T3);
+> > overriding
+> > function Something_Green return T3;
+> > -- P1 and P3 are inherited from Pack1.P1 and Pack1.P3,
+> > -- respectively.
+>
+> Not "respectively". The Pack1 versions override in both cases.
+
+Not sure what you mean here. I meant P1 is inherited from Pack1.P1, and P3 is
+inherited from Pack1.P3. Pack2 is not mentioned, and I wasn't interested in the
+details as to why (irrelevant for this AI). I suppose I could have written this
+as two separate comments, but I fail to see anything wrong with the one I have.
+
+> > with Pack1, Pack3;
+> > procedure Main is
+> > procedure Do_It (Obj : in Pack3.T3'Class) is
+> > begin
+> > Obj.P1; -- (1)
+>
+> P1 takes an 'in out', but Obj is constant.
+
+Oops. Fixed.
+
+> I wonder if these sorts of examples would be clearer if we avoid
+> prefix notation calls?!
+
+Unless you want to confuse the heck out of yourself, you'll never use prefix
+calls for dispatching in Ada 2005 or later. The alternative is lots of use
+clauses (which is not going to help make these examples more understandable), or
+lengthy prefixes which are really hard to get right. (And I'm not quite sure
+what the prefix needs to be here...)
+
+...
+> > It has been suggested that the contract aspects of an inherited
+> > routine ought to be considered the same as those for an overriding
+> > routine declared at the same point. (This would require nothing more
+> > than the compiler generating a wrapper at this point.) But that brings
+> > up a new problem. Consider the following:
+> >
+> > with Pack1, Pack2, Pack3;
+>
+> Remove Pack1. The whole point of the example is that we don't know
+> about Pack1 here.
+
+OK.
+
+...
+> > Note that if we are using Pre rather than Pre'Class, then the
+> > preconditions of a dispatching call need have any real relationship.
+> > In that case, the
+>
+> "need not"
+
+Oops again.
+
+> > Finally, the wording given in AI05-0145-2 makes it clear that Pre
+> > and Post are not inherited. However, nothing is said about what
+> > happens to these when a subprogram is inherited. With the
+> > AI05-0145-2 wording, it appears. Clearly,
+>
+> What appears what?
+
+"that there is no inheritance of Pre and Post".
+
+> > we
+> > want to evaluate the Pre and Post values associated with a
+> > subprogram when that subprogram is inherited.
+
+I added another phrase here:
+
+ , otherwise the body of the subprogram could be called without the
+ preconditions it is expecting.
+
+...
+> > Add at the end of 3.10.2(32/2):
+> >
+> > If P has one or more class-wide precondition expressions that apply
+> > to it, at least one of those expressions shall be the enumeration
+> > literal True.
+>
+> "shall statically denote True"?
+
+A precondition aspect represents an expression, not a value. Thus, we have to
+word this in terms of the expression, not the value that we might evaluate it to
+have. In particular, my intent was to require that this expression is exactly
+the Boolean enumeration literal True. I suppose it would be OK to have used
+"statically denotes" instead (that allows renames of True):
+
+shall statically denote the Boolean enumeration literal True.
+
+I didn't want to call this "True" by itself (that invites confusion with the
+value), "literal True" doesn't make much sense, so I used the entire long thing.
+
+> > AARM Reason: An access to access-to-subprogram type does not have a
+>
+> Too many access-to's.
+
+Access 3?? :-)
+
+...
+> > Modify 13.3.2(2-5/3):
+> >
+> > Pre
+> > This aspect [specifies]{defines} a {specific} precondition for a
+> > callable entity; it shall be specified by an expression, called a
+> > {specific} precondition expression. {If not specified for an entity,
+> > the specific precondition expression for the entity is the
+> > enumeration literal True.}
+>
+> "enumeration literal True" --> "True" (and below)
+
+See above. This is *not* a value, but an expression consisting of nothing but
+the Boolean enumeration literal True. I figured I could leave out "Boolean"
+since that is the type of the expression, but the other part is necessary to
+emphasize the distinction.
+
+...
+
+> > Modify 13.3.2(6/3):
+> >
+> > The expected type for [a]{any} precondition or postcondition
+> > expression is any boolean type.
+>
+> I think "a" is just as clear.
+
+OK, but I disagree; there are two different preconditions, and we never defined
+"precondition expression" to mean both kinds. That seemed like overkill, so I
+used "any" consistently to mean all of the kinds.
+
+...
+> > * The specific precondition check begins with the evaluation of the specific
+> > precondition expression that applies to the subprogram or entry;
+> > if the expression evaluates to False, Ada.Assertions.Assertion_Error is
+> > raised.
+>
+> "Ada.Assertions.Assertion_Error" --> "Assertion_Error".
+> We don't normally spell out full expanded names; it's just noise. For
+> example, in A.10.5:
+>
+> 11 The exception Mode_Error is propagated if the mode is not In_File.
+> The exception End_Error is propagated if an attempt is made to read
+> a file terminator.
+>
+> (I don't see any difference between "raised" and "propagated".)
+
+We treated Assertion_Error differently for some reason (see 11.4.2(18/2)).
+Probably because no one would have a clue where this exception is declared if we
+didn't give the prefix (it is not anywhere near here, and it it not in the same
+package as in the case given above). But the "Ada." prefix shouldn't be there
+(we never write that).
+
+And there is a difference between "raised" and "propagated". Subprograms
+"propagate" exceptions; checks "raise" exceptions. This is a check, so the
+exception is raised.
+
+(Why you Ada 95 guys wrote the text that way I don't know, but reviewers beat on
+me until all of the containers were consistent with the above.)
+
+...
+> > The order of performing the checks is not specified, and if any of
+> > the class-wide precondition expressions evaluate to True, it is not
+> > specified whether the other class-wide precondition expressions are
+> > evaluated. It is not specified whether any check for elaboration of
+> > the subprogram body is performed before or after the precondition
+> > checks. It is not specified whether in a call on a protected
+> > operation, the checks are performed before or after starting the
+> > protected action. For a task or protected entry call, the checks are
+>
+> "task or protected entry call" --> "entry call"
+>
+> > performed
+> > prior to checking whether the entry is open.
+
+That's existing Tucker wording which I left unchanged. I assume he was
+reinforcing some idea here (probably the intent that it applies to both) with
+the redundancy.
+
+...
+> > If the Assertion_Policy in effect at the point of a subprogram or
+> > entry declaration is Check, then upon successful return from a call of
+> > the subprogram or entry, prior to copying back any by-copy in out or
+> > out parameters, the postcondition checks is performed. This consists
+> > of the evaluation of the
+>
+> "are"
+
+"is". :-). More accurately, "postcondition check is" - there is only one
+postcondition check (everything is lumped together because there is no need to
+talk about them individually). I for a while had separated the checks, but I
+obviously left some vestige of that model when I switched it back.
+
+...
+> > AARM Ramification: This applies to access-to-subprogram calls, dispatching
+> > calls, and to statically bound calls. We need this rule to cover
+> > statically bound calls as well, as Pre preconditions and Post
+> > postconditions are not inherited, but
+>
+> "Pre preconditions and Post postconditions" --> "specific
+> pre- and postconditions"
+
+Yes, that's better. Although I was trying to remind the reader of what that
+means. But they probably should go look it up if they are confused.
+
+...
+> > Notwithstanding what this standard says elsewhere, an inherited subprogram S
+> > (or multiple conformant inherited subprograms) that has one or or
+> > more class-wide precondition or postcondition expressions that apply
+> > to S, or has a specified Type_Invariant'Class (see 13.3.3), that is
+> > not explicitly overridden, and that is primitive for a type that has
+> > one or more progenitors is equivalent to an overriding subprogram S whose
+> > body consists of:
+> > * The null statement, if all of the inherited subprograms are
+> > null subprograms;
+> > * A call on the parent subprogram, with all of the parameters the same
+> > as the parameters to S (possibly with appropriate type conversions).
+>
+> Do we need, "The same rule applies to functions (possibly with
+> appropriate type conversion of the result)"?
+
+Why? This wording is about primitive *subprograms*, and those surely include
+functions with controlling results. The type conversion wording can be read to
+apply to everything. I could see expanding that a bit to say "(possibly with
+appropriate type conversions on the parameters and result if any)", but that's
+all that could be needed.
+
+> > If a subprogram renaming overrides one or more inherited
+> > subprograms, the
+> > renaming is equivalent of an subprogram whose body calls the renamed
+> > subprogram, with
+>
+> "an" --> "a"
+>
+> > all
+> > of the parameters the same as the parameters to S (possibly with appropriate
+> > type
+> > conversions).
+>
+> Functions?
+
+Same change as above (not that I think it is necessary, but it isn't worth the
+argument).
+
+> > AARM Ramification: We really mean equivalent here! The call on the parent
+> > subprogram will evaluate preconditions as needed. And a dispatching
+> > call will call this body, rather than that of one of the inherited
+> > subprograms. 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.
+>
+> For some reason, the "really mean it" part rubs me the wrong way.
+> Can we say, "This equivalence implies that..."?
+
+We could, but this is a nod to the usual "we said 'equivalent', but we really
+meant pretty similar" that always seems to happen. Here, we really did mean
+"equivalent" in the literal sense of the word. So it is an ARG inside remark.
+
+I made the change and added a "Editor's Note" to mention the difference. If
+Tucker ever has his "better idea", this will all be different anyway.
+
+> > AARM Discussion: Only one implicit overriding subprogram is created
+> > for a
+> > single set of homoegraphs.
+>
+> "homographs".
+
+Yeah, I already saw that.
+
+> But I think it might be better to say "single set of inherited
+> subprograms".
+
+Not sure. I used "homographs" because it is formally clear that the set includes
+only routines with the proper profile. "Inherited subprograms" could mean that,
+or all of the routines with the same name, or all of the routines in total. I
+didn't want any confusion. Maybe "inherited homographs"? Or "inherited
+subprograms that are homographs"? "inherited homographic subprograms"? :-)
+
+> > AARM Reason: These rules eliminates four problems: (1) the issue that two
+>
+> "eliminate"
+>
+> "problems" --> "potential problems" (they're not problems anymore,
+> once we adopt this AI!)
+
+OK.
+
+> > null subprograms (one of which is chosen for dispatching arbitrarily by
+> > 3.9.2(20.3/3)) may not be equivalent at runtime; (2) "counterfeiting"
+>
+> "may not be equivalent at runtime" --> "might have different
+> contracts"?
+
+"contract" is not an RM technical term (at least in this sense), so I didn't
+want to use that term here. "might have different Pre'Class, Post'Class, and
+Type_Invariant'Class aspects" is better, but the latter part is possibly
+confusing.
+
+"might have different contract aspects that apply" would be better, but again
+"contract aspects" is a term that isn't defined.
+
+"might have different aspects that apply" seems vague. Besides, the fact that
+there could be different behavior for two null subprograms is the crux of the
+issue and needs to be mentioned somehow.
+
+I used "might have different aspects that apply, causing different runtime
+behavior", but there might be something better possible.
+
+...
+Following this are several suggestions that I used unmodified.
+
+...
+> > We fix these both by including Pre'Class in conformance checking, such that
+>
+> I don't see anything about conformance in this AI. Maybe this
+> discussion section is obsolete?
+
+Just this paragraph. Tucker had suggested this model, but I discovered that the
+"implicit body" model fixed the problems with renames -- and without making
+anything illegal.
+
+I almost used the same rule for 'Access, but didn't solely because it seemed a
+bit more confusing there.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, March 28, 2011 12:59 PM
+
+Like some others, I am overwhelmed by the details of the discussion on the exact
+semantics of Pre'Class and Post'Class. I am concerned about the difficulties of
+presenting this to users in an intuitive fashion. I am also concerned that with
+different rules for Pre'Class and Pre the danger is that once again (as Erhard
+remarked in connection with aspects vs. attributes) the perception will be that
+Ada always offers two ways of doing roughly the same thing. This perception may
+be misguided but the complications are plenty real.
+
+So here is a timid suggestion: we agree that Pre and Post by themselves are
+little more that assert statements, and the real meat is in the inheritable and
+combinable aspects. So what about renaming Pre'Class and Post'Class as Pre and
+Post, and ditch the non- inheritable versions? For those timid souls that shy
+away from complex inheritance patterns things will work as they expect, and the
+others will have to understand how the RM faithfully matches LSP and all is
+well.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 28, 2011 1:25 PM
+
+I think abandoning "simple" Pre would be a mistake.
+Assert statements are not visible in the spec, and there is a very important
+documentation and contract associated with specifying a "simple" precondition.
+
+I also think it is quite important that Pre'Class remain named "Pre'Class" to
+emphasize its inheritability.
+
+I remember a long debate with Cyrille at AdaCore, and the conclusion was that it
+was important to provide both inheritable and a non-inheritable preconditions.
+I don't believe we should back down on that (despite the legitimate concern
+about two different ways to do the same thing).
+
+The fact is Pre and Pre'Class are really two different things, in the same way
+that T and T'Class are different. Admittedly Ada is unusual among OOP languages
+in making the distinction between T and T'Class, but I think it was one of the
+better choices we made in our OOP model. I feel Pre and Pre'Class go hand in
+hand with the T and T'Class distinction.
+
+Getting the right answer is not trivial, but we shouldn't be frightened by the
+length of the road, but rather be focused on the end result. If we don't like
+the end result, that is fine (and I understand and appreciate your concern about
+the "two ways" issue).
+
+But if we mainly don't like the way the sausage was made, don't watch... ;-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 1:41 PM
+
+> So here is a timid suggestion: we agree that Pre and Post by
+> themselves are little more that assert statements, and the real meat
+> is in the inheritable and combinable aspects. So what about renaming
+> Pre'Class and Post'Class as Pre and Post, and ditch the non-
+> inheritable versions? For those timid souls that shy away from
+> complex inheritance patterns things will work as they expect, and the
+> others will have to understand how the RM faithfully matches LSP and
+> all is well.
+
+That doesn't work because Pre'Class is only allowed on primitives of tagged
+types, while Pre can be used anywhere. You'd end up with two different semantics
+with the same name.
+
+The other reason it doesn't work is a practical one: the LIS semantics is way
+too fierce for most real uses. I have been completely unable to come up with
+anything even vaguely plasible as to when you would want to weaken a
+precondition. As such, I think Pre'Class will typically be used on a root
+subprogram and then never changed on any child subprograms. If you have
+additional properties (not known to the root type) that need to be enforced on a
+routine, the only way to do that is via a Pre expression. Unless you are willing
+to completely give up on compile-time optimizability.
+
+Keep in mind that this whole debate is solely about how dispatching calls and
+inherited calls should work. In the normal statically bound case, this is all
+very straightforward.
+
+If we are going to drop anything, it should be Pre'Class etc. It may not be
+worth it to allow dispatching calls to be analyzed/optimized. (I disagree with
+that idea, but I can imagine why others would not.)
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, March 28, 2011 1:56 PM
+
+> Keep in mind that this whole debate is solely about how dispatching
+> calls and inherited calls should work. In the normal statically bound
+> case, this is all very straightforward.
+
+Is it? Aren't the inherited Pre'class involved, even if this is a static call?
+
+> If we are going to drop anything, it should be Pre'Class etc. It may
+> not be worth it to allow dispatching calls to be analyzed/optimized.
+> (I disagree with that idea, but I can imagine why others would not.)
+
+From your previous paragraph, this does not seem like such a big loss. Either we
+want inheritance all along, and then we should call it with the shorter name
+anyway, or else inheritance is a minor convenience and we can drop it. Tuck
+indicates that Pre'Class is indispensable, but you seem to say that in practice
+it is only useful at the root of a hierarchy. ???
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 28, 2011 2:22 PM
+
+> ...
+>> If we are going to drop anything, it should be Pre'Class etc. It may
+>> not be worth it to allow dispatching calls to be analyzed/optimized.
+>> (I disagree with that idea, but I can imagine why others would not.)
+>
+> From your previous paragraph, this does not seem like such a big
+> loss. Either we want inheritance all along, and then we should call it
+> with the shorter name anyway, or else inheritance is a minor convenience and
+> we can drop it. Tuck indicates that Pre'Class is indispensable, but you seem
+> to say that in practice it is only useful at the root of a hierarchy. ???
+
+Remember that with interfaces, there are many "roots" of a hierarchy.
+Without Pre'Class, you really can't say anything interesting on an interface,
+and that would be a shame. In fact, one could argue that it is really
+interfaces (or other abstract tagged types) that need Pre'Class, and without
+Pre'Class, you essentially lose the ability to specify any kind of contract for
+such types.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, March 28, 2011 2:50 PM
+
+Could be, but I have trouble imagining different preconditions for different
+primitives of the same interface. As you say, these are contracts for these
+abstract types, but I suspect that in most cases these are going to be
+(abstract) properties of the type, and not operation-specific predicates. Maybe
+this lack of imagination disqualifies me from this discussion, but the
+precondition Is_Green is not a compelling example! How come no one has come up
+with a good motivating example with independent Pre'Class predicates on, say an
+interface and a concrete ancestor type in this discussion?
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 28, 2011 3:00 PM
+
+A precondition is a set of requirements
+on any input to the subprogram, which includes the controlling object(s), other
+parameters, any global state read by the subprogram, etc.
+
+You are definitely lacking in imagination if you think preconditions only depend
+on the single "primary" controlling object.
+
+Imagine a vector-like collection of some sort.
+Typically there is an operation for indexing into the vector. Clearly the
+precondition would be something like "Pre'Class => Index in 1..Length(Vec)".
+
+And then you could have extensible vectors with some upper bound, in which case
+the precondition on indexed assignment might be weakened to be:
+
+ Pre'Class => Index in 1..Max_Size(Vec)
+
+with a postcondition of
+
+ Post'Class => Length(Vec) = Integer'Max(Length(Vec'Old), Index)
+
+presuming elsewhere we ensure that Length(Vec) <= Max_Size(Vec).
+
+Or a vector that could grow one element at a time, which would allow the
+precondition on indexed assignment to be:
+
+ Pre'Class => Index in 1..Length(Vec)+1
+
+etc., etc.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 3:11 PM
+
+> A precondition is a set of requirements on any input to the
+> subprogram, which includes the controlling object(s), other
+> parameters, any global state read by the subprogram, etc.
+>
+> You are definitely lacking in imagination if you think preconditions
+> only depend on the single "primary" controlling object.
+
+I *know* I qualify as "lacking in imagination" this way. But then again I don't
+think multiple inheritance is useful enough to go to the absurd lengths it
+requires in definition and implementation.
+
+> Imagine a vector-like collection of some sort.
+> Typically there is an operation for indexing into the vector.
+> Clearly the precondition would be something like "Pre'Class => Index
+> in 1..Length(Vec)".
+
+Looks good.
+
+> And then you could have extensible vectors with some upper bound, in
+> which case the precondition on indexed assignment might be weakened to
+> be:
+>
+> Pre'Class => Index in 1..Max_Size(Vec)
+
+I'm glad that you are giving an example. But I disagree here. "Length" is a
+dispatching operation in Pre'Class; the appropriate design is to change the
+meaning of Length.
+
+> with a postcondition of
+>
+> Post'Class => Length(Vec) = Integer'Max(Length(Vec'Old), Index)
+>
+> presuming elsewhere we ensure that Length(Vec) <= Max_Size(Vec).
+
+This doesn't make much sense to me.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March 28, 2011 3:16 PM
+
+> I'm glad that you are giving an example. But I disagree here. "Length"
+> is a dispatching operation in Pre'Class; the appropriate design is to
+> change the meaning of Length.
+
+I think you're misunderstanding Tucker's example. In the "extensible"
+vector, you can set the I'th element to X, even though I is bigger than the
+_current_ length, and it automatically grows the vector.
+
+Overriding Length doesn't accomplish that.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 28, 2011 3:32 PM
+
+Correct. And only on an indexed *assignment* operation is the Index allowed to
+be larger than Length. On an indexed *fetch* operation, the Index must be no
+larger than the Length.
+
+BTW, when I said lacking in imagination, I was making reference to Ed's comment.
+He seemed to be saying that a single precondition would be adequate for an
+entire set of operations (unless I misunderstood him, which is possible). That
+seemed like a lack of imagination (though probably more likely a
+misunderstanding on my part).
+
+In any case, this was meant to show both that preconditions vary from one
+operation to another, and how preconditions can be usefully weakened as you add
+bells and whistles to a data structure as you extend it.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 3:38 PM
+
+> I think you're misunderstanding Tucker's example. In the "extensible"
+> vector, you can set the I'th element to X, even though I is bigger
+> than the _current_ length, and it automatically grows the vector.
+>
+> Overriding Length doesn't accomplish that.
+
+OIC.
+
+I was thinking of "extensible" in the sense of Ada.Containers.Vectors, and not
+in the sense of some horrible auto-extending semantics. I don't think this is a
+very good example simply because it is such a bad idea at the core that I'd be
+happier if the language didn't permit it in the first place. :-)
+
+The "overdraw" example is better. But I still don't think that these examples
+are likely to occur often in practice. Maybe the people who think everything in
+the world should be written by OOP would run into them, but those people are
+nuts. :-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 3:46 PM
+
+> BTW, when I said lacking in imagination, I was making reference to
+> Ed's comment. He seemed to be saying that a single precondition would
+> be adequate for an entire set of operations (unless I misunderstood
+> him, which is possible).
+> That seemed like a lack of imagination (though probably more likely a
+> misunderstanding on my part).
+
+I know, but I am thinking like Ed here. And I am perfectly willing to admit a
+lack of imagination when it comes to the use of OOP. I find it useful in
+specialized circumstances, but not something that you will want to use for
+everything. I suspect that a lot of these examples come up because people are
+defining way too many types with way too much inheritance. And that won't happen
+in practice (most "hierarchies" are only one level deep).
+
+> In any case, this was meant to show both that preconditions vary from
+> one operation to another, and how preconditions can be usefully
+> weakened as you add bells and whistles to a data structure as you
+> extend it.
+
+I have no problem believing that they might vary. I'm still dubious that
+weakening is useful in practice (but at least you have finally shown an example
+where it might be useful).
+
+I'd be happy if we treated the contract as we do most other contract items in
+Ada (must match, period). But I realize that is too limiting for interfaces
+(virtually nothing would match, so almost all interfaces would be illegal). I
+personally don't care that much about interfaces, but I can't seriously advocate
+a rule that would make them useless, either. (If it wasn't for this issue, I
+would be pushing harder for such a rule, especially as the additional Pre takes
+care of most of the realistic cases.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 28, 2011 3:51 PM
+
+> ... The "overdraw" example is better. But I still don't think that
+> these examples are likely to occur often in practice. Maybe the people
+> who think everything in the world should be written by OOP would run
+> into them, but those people are nuts. :-)
+
+Why do people use inheritance at all? One reason is because they have
+hierarchies of abstractions of increasing complexity.
+
+I think we should be very wary of trying to predict exactly how people will use
+these capabilities. Bob and I came up with a few examples, and could almost
+certainly come up with more and better examples if we felt the need, but at some
+point, you have to agree that OOP involves hierarchies where what changes as you
+go down the hierarchy is very much application specific. If we start saying
+that this or that abstraction is a "bad idea," we are going out on a pretty
+fragile limb in my view.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March 28, 2011 2:32 PM
+
+> Here is what we are debating:
+
+Thanks for the summary. I actually went back and read the whole thread as well.
+
+> 1) Must Pre'Class be checked at the call site,
+> or could it be done inside the body?
+> Answer: we seem to agree it only makes sense
+> if it is done at the point of call, and only
+> the Pre'Class aspects known at the point of call
+> are checked.
+
+Question: One way to implement "check at call site" is to create a wrapper at
+the point of type derivation (in cases where it's needed -- multiple
+inheritance). Correct?
+
+If so, I agree.
+
+> 2) Should specifying a Pre'Class have any affect on
+> the "Pre" aspects?
+> Tuck's Answer: No, let's split them completely.
+> This allows (and pretty much requires) "Pre" aspects
+> to be checked in the body.
+> Randy's Answer: Not sure.
+
+OK, I guess. If Pre is equivalent to a pragma Assert in the body, then it's not
+much use, and (like Assert), a Pre that the caller can't see might fail. I
+suppose that's OK, but I'd be inclined to stick with 'Pre'Class when using
+tagged types.
+
+> 3) What are some of the implications of renaming and taking
+> 'Access of a subprogram to which Pre'Class applies?
+> Tuck's Answer: Make hard stuff illegal, by incorporating
+> Pre'Class matching into subtype conformance, but still
+> allow Pre'Class weakening.
+> Randy's Answer: Not sure. Maybe disallow Pre'Class weakening
+> completely.
+
+These are corner cases. I don't have strong opinions, but the general idea of
+outlawing things that cause trouble seems OK.
+
+Speaking of outlawing things, please remind me why we don't want to outlaw
+pre/post/invariant on (ops of) interfaces. These features seem useful on
+interfaces, so we shouldn't outlaw them, but I'm having trouble articulating
+exactly why.
+
+> One other issue that seems clear is that when you inherit code for an
+> operation from a parent type, and you also inherit the "same"
+> operation from one or more interfaces where the operation has a
+> Post'Class aspect, you will probably have to create a wrapper to
+> properly incorporate the inherited Post'Class aspects into the
+> inherited code, since they all get and-ed together.
+
+I must be missing something. It seems like this is exactly
+(1) above, hence my question above.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 2:57 PM
+
+...
+> > 1) Must Pre'Class be checked at the call site,
+> > or could it be done inside the body?
+> > Answer: we seem to agree it only makes sense
+> > if it is done at the point of call, and only
+> > the Pre'Class aspects known at the point of call
+> > are checked.
+>
+> Question: One way to implement "check at call site" is to create a
+> wrapper at the point of type derivation (in cases where it's needed --
+> multiple inheritance).
+> Correct?
+
+Not really, since the Pre'Class aspects known at the point of the call can
+differ depending on precisely which routine is called. This is most obvious when
+calling through an interface.
+
+You *could* do it with wrappers, but you'd need one wrapper for every possible
+set of Pre'Class -- while this is ususally a small set, it probably doesn't make
+sense to generate a lot of wrappers.
+
+> > 2) Should specifying a Pre'Class have any affect on
+> > the "Pre" aspects?
+> > Tuck's Answer: No, let's split them completely.
+> > This allows (and pretty much requires) "Pre" aspects
+> > to be checked in the body.
+> > Randy's Answer: Not sure.
+>
+> OK, I guess. If Pre is equivalent to a pragma Assert in the body,
+> then it's not much use, and (like Assert), a Pre that the caller can't
+> see might fail. I suppose that's OK, but I'd be inclined to stick
+> with 'Pre'Class when using tagged types.
+
+That's a decision for the user to make, not the language. I agree that users
+probably should either use Pre'Class or Pre exclusively (not mixing them), but
+that is the sort of "style" rule that we usually leave to separate tools to
+enforce.
+
+> > 3) What are some of the implications of renaming and taking
+> > 'Access of a subprogram to which Pre'Class applies?
+> > Tuck's Answer: Make hard stuff illegal, by incorporating
+> > Pre'Class matching into subtype conformance, but still
+> > allow Pre'Class weakening.
+> > Randy's Answer: Not sure. Maybe disallow Pre'Class weakening
+> > completely.
+>
+> These are corner cases. I don't have strong opinions, but the general
+> idea of outlawing things that cause trouble seems OK.
+>
+> Speaking of outlawing things, please remind me why we don't want to
+> outlaw pre/post/invariant on (ops of) interfaces.
+> These features seem useful on interfaces, so we shouldn't outlaw them,
+> but I'm having trouble articulating exactly why.
+
+Same here. I can't quite figure out how you could usefully use Pre on interfaces
+(given the weakening semantics). Post and Invariants don't suffer from that.
+
+> > One other issue that seems clear is that when you inherit code for an
+> > operation from a parent type, and you also inherit the "same"
+> > operation from one or more interfaces where the operation has a
+> > Post'Class aspect, you will probably have to create a wrapper to
+> > properly incorporate the inherited Post'Class aspects into the
+> > inherited code, since they all get and-ed together.
+>
+> I must be missing something. It seems like this is exactly
+> (1) above, hence my question above.
+
+(1) is only talking about Pre'Class. Post'Class and Post are handled identically
+(we check everything based on the actual body). It doesn't work very well to
+skip inherited Post'Class, and it doesn't help code generation or
+understandability any.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March 28, 2011 2:32 PM
+
+> > I don't agree; weakening the Pre'Class can make sense as you go into
+> > a particular subtree of the type hierarchy.
+>
+> I would like to see an example of why you would want this in practice
+> (not in theory!!).
+
+There are lots of examples out there. Read Meyer's book on OOP, for example.
+(Yeah, I know that's not practical in the short term -- it's thick enough to
+make a good doorstop on a windy day. ;-))
+
+Anyway, I'm pretty sure this is an important OOP capability.
+But we also want plain-old Pre on plain-old non-OO procedures.
+
+>... There is a lot of OOP stuff that makes sense in theory but never
+>actually happens in practice. Needing to "weaken" the precondition
+>seems to me like there was a bug in the original definition of the
+>precondition (most likely, the boolean functions that make it up are
+>not defined properly). But I am willing to believe that I am wrong --
+>but to do that I'd need to see an example for which the weaker
+>precondition makes sense.
+
+How about:
+
+ type Money is digits ... range 0.0 .. ...; -- nonnegative!
+
+ type Bank_Account is ...
+ procedure Withdraw
+ (Account: in out Bank_Account;
+ Amount: Money) with
+ Pre'Class => Current_Balance(Account) >= Amount;
+
+ type Bank_Account_With_Overdraw is ...
+ -- You know, the kind where the bank gives you an automatic loan.
+ overriding procedure Withdraw
+ (Account: in out Bank_Account_With_Overdraw;
+ Amount: Money) with
+ Pre'Class => True; -- weaken, to allow overdraw
+
+A dispatching call on Withdraw, passing Bank_Account'Class should ensure the
+balance is enough. But with Bank_Account_With_Overdraw'Class, the caller can
+rely on the automatic loan.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March 28, 2011 2:32 PM
+
+> > By the way, Bob implied that postconditions were to be associated
+> > with the body. I don't agree.
+
+Well, I don't really agree either. ;-)
+
+> > ...Postconditions are
+> > both more time *and* space efficient if performed inside the body,
+> > but the right semantic view is still from the caller's point of
+> > view. Preconditions and postconditions are promises made to the
+> > *caller*.
+
+No, that's not right, either. I don't remember exactly what I said, but here's
+what I think now:
+
+A precondition is a promise made by the caller to the callee.
+A postcondition is a promise made by the callee to the caller.
+
+Or, equivalently:
+A precondition is a requirement on the caller, which the body can rely on.
+A postcondition is a requirement on the body, which the caller can rely on.
+
+As for efficiency, it's more complicated than I implied.
+Let's let implementers worry about efficiency.
+
+> > In any case, I think we are in agreement that the caller view is the
+> > key to understanding the semantics for preconditions and
+> > postconditions.
+
+I think it's necessary to take both caller and callee views.
+
+> > ...Type invariants are more like
+> > postconditions in my view,
+
+Ideally, they are. But Eiffel checks them going both in and out, and for good
+reason.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 3:23 PM
+
+> > That doesn't work because Pre'Class is only allowed on primitives of
+> > tagged types, while Pre can be used anywhere. You'd end up with two
+> > different semantics with the same name.
+>
+> "is only allowed" in the current version of the AI. Easy to change,
+> in particular if it simplifies the text.
+
+But it won't simply the text. Pre is not inherited on other operations for good
+reason - the allowed changes in profile would make a mess out of any existing
+Pre and we definitely do not need or want any "weakening" for operations of
+untagged types.
+
+> > The other reason it doesn't work is a practical one: the LIS
+> > semantics is way too fierce for most real uses. I have been
+> > completely unable to come up with anything even vaguely plasible as
+> > to when you would want to weaken a precondition. As such, I think
+> > Pre'Class will typically be used on a root subprogram and then never
+> > changed on any child subprograms. If you have additional properties
+> > (not known to the root
+> > type) that need to be enforced on a routine, the only way to do that
+> > is via a Pre expression. Unless you are willing to completely give
+> > up on compile-time optimizability.
+> >
+> > Keep in mind that this whole debate is solely about how dispatching
+> > calls and inherited calls should work. In the normal statically
+> > bound case, this is all very straightforward.
+>
+> Is it? Aren't the inherited Pre'class involved, even if this is a
+> static call?
+
+Sure, but the reason Pre'Class and Post'Class are inherited is so that
+dispatching calls have well-defined preconditions and postconditions and thus
+are analyzable. It doesn't provide any value to statically bound calls.
+
+For a dispatching call to be analyzable, it has to have the "same" contract for
+all overriding routines. For existing contract elements (constraints, not null,
+no return, etc.) this is enforced by requiring subtype conformance and matching
+for all descendants. For Preconditions, this requires that the precondition is
+the same (or weaker) on all descendants. For postconditions, this requires that
+the postcondition is the same (or stronger) on all descendants.
+
+> > If we are going to drop anything, it should be Pre'Class etc. It may
+> > not be worth it to allow dispatching calls to be analyzed/optimized.
+> > (I disagree with that idea, but I can imagine why others would not.)
+>
+> From your previous paragraph, this does not seem like such a big loss.
+> Either we want inheritance all along, and then we should call it with
+> the shorter name anyway, or else inheritance is a minor convenience
+> and we can drop it. Tuck indicates that Pre'Class is indispensable,
+> but you seem to say that in practice it is only useful at the root of
+> a hierarchy. ???
+
+As previously noted, I don't think weakening will come up often in practice.
+(Tucker seems to disagree.) In the absence of useful weakening, the Pre'Class is
+the same all the way from the root. [That makes sense to me, this is a contract
+and you do not change contracts for inherited routines -- but it apparently
+doesn't make sense to OOP mavens.] But this is a property that has to be ensured
+in order for the compiler (and static analysis tools) to be able to take
+advantage of it. There cannot be any possibility of cheating -- thus it has to
+be inherited automatically.
+
+OTOH, in practice I think you are going to need to be able to add other
+preconditions that violate the OOP model. You could use assertions for that, but
+then statically bound callers will not be able to "see" and depend on those
+added preconditions. And in Ada, the vast majority of calls are statically
+bound. We really do not want to make the normal case worse just to support some
+OOP orthodoxy.
+
+So I do think we need both -- since I think it is horrible to eliminate the
+possibility of analysis on dispatching calls.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 3:33 PM
+
+> > Remember that with interfaces, there are many "roots" of a hierarchy.
+> > Without Pre'Class, you really can't say anything interesting on an
+> > interface, and that would be a shame. In fact, one could argue that
+> > it is really interfaces (or other abstract tagged types) that need
+> > Pre'Class, and without Pre'Class, you essentially lose the ability
+> > to specify any kind of contract for such types.
+>
+> Could be, but I have trouble imagining different preconditions for
+> different primitives of the same interface.
+> As you say, these are contracts for these abstract types, but I
+> suspect that in most cases these are going to be (abstract) properties
+> of the type, and not operation-specific predicates. Maybe this lack of
+> imagination disqualifies me from this discussion, but the precondition
+> Is_Green is not a compelling example! How come no one has come up
+> with a good motivating example with independent Pre'Class predicates
+> on, say an interface and a concrete ancestor type in this discussion?
+
+I'm of two minds on this.
+
+Mind one says that we have to have preconditions on interfaces because the
+alternative is that interfaces are second-class citizens. A dispatching call
+through one of its primitives would not have a known precondition, and thus we
+either would have to adopt a special rule for them (using the preconditions of
+the concrete operation) or require all such operations to have no precondition.
+The first is the bad old "no analysis" case again; it should be obvious that the
+second is really limiting. Neither seems acceptable to me.
+
+Mind two says that "weakening" which happens when you combine preconditions is
+almost never going to be what you want. Using the lousy "Is_Green" example, the
+precondition ends up as "Is_Valid or Is_Green", which is definitely not what you
+want (unless "Valid" and "Green" end up being defined as the same thing).
+
+The net effect is that I cannot imagine any rules that would make preconditions
+on interfaces both useful and able to be analyzed. This is where I have the same
+lack of imagination that you have -- except it is worse: I can't really imagine
+enough uses for interfaces where they would actually gain anything in practice
+to even bother having them, much less make them work.
+
+So I don't care what the rules for interfaces are, so long as they don't screw
+up the language. And screwing up the language would be treating dispatching
+calls differently depending on what sort of routine is involved. Or preventing
+any static analysis of dispatching calls forever (because if we adopt a run-time
+only rule, there will never be any chance to fix it).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 28, 2011 3:34 PM
+
+> Speaking of outlawing things, please remind me why we don't want to
+> outlaw pre/post/invariant on (ops of) interfaces.
+> These features seem useful on interfaces, so we shouldn't outlaw them,
+> but I'm having trouble articulating exactly why...
+
+I think we did outlaw them on abstract subprograms. And as far as allowing them
+on null procedures of interfaces, I think we at least talked about disallowing
+them there as well.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 3:50 PM
+
+I thought Bob was talking about the classwide versions.
+
+The specific versions are banned on abstract subprograms and null procedures
+because the former can never be called, and the latter have problems with
+equivalence - we don't require overriding null procedures, and if there are two
+null procedures with different Pres, whose Pre gets used??
+
+But the classwide versions need to exist so it is possible to reason about
+dispatching calls for classwide interfaces. Otherwise, they all have a
+precondition of True (and with weakening, that is likely to be trouble for the
+inherited bodies!!).
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March 28, 2011 5:19 PM
+
+> I thought Bob was talking about the classwide versions.
+
+Yes. Sorry for being unclear. My understanding is that Pre'Class and
+Post'Class are allowed on operations of interfaces, both abstract and null. And
+Invariant'Class is allowed on an interface. Is that correct?
+
+And I guess my question is either "Why are they allowed?" or "Why are they
+disallowed?", depending on the above.
+
+I think some of us (like me, but probably also Randy and Ed) are/were forgetting
+something: All this talk about inheriting a procedure from multiple ancestors
+(e.g. from the parent and also from an interface) is the unusual case. We have
+to define what it means, but the more common case is where you inherit P1, P2,
+P3 from your main parent, and you inherit totally unrelated Q1, Q2, Q3 from some
+interface. You probably override the Q's, and it's good to be bound by their
+Pre'Class, whether they were abstract or null.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 5:35 PM
+
+> Yes. Sorry for being unclear. My understanding is that Pre'Class and
+> Post'Class are allowed on operations of interfaces, both abstract and
+> null.
+> And Invariant'Class is allowed on an interface.
+> Is that correct?
+
+Yes.
+
+> And I guess my question is either "Why are they allowed?" or "Why are
+> they disallowed?", depending on the above.
+
+I answered that in one of my earlier messages. The short answer is that if we
+don't, then dispatching calls though interface values have no preconditions at
+all -- that would be bad.
+
+> I think some of us (like me, but probably also Randy and Ed) are/were
+> forgetting something: All this talk about inheriting a procedure from
+> multiple ancestors (e.g. from the parent and also from an interface)
+> is the unusual case. We have to define what it means, but the more
+> common case is where you inherit P1, P2, P3 from your main parent, and
+> you inherit totally unrelated Q1, Q2, Q3 from some interface.
+> You probably override the Q's, and it's good to be bound by their
+> Pre'Class, whether they were abstract or null.
+
+I agree (other than the "forgetting" part), except that I would go further and
+say that the use of interfaces -- at all -- is unusual. So by definition
+anything that happens with them is unusual. (Even if you disagree with me on the
+value of interfaces, you can't argue that most Ada OOP code is Ada 95 code --
+for the simple reason that most Ada compilers only are Ada 95 compilers.)
+
+But even if they are unusual, we have to have a proper definition for them.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 28, 2011 5:55 PM
+
+> I agree (other than the "forgetting" part), except that I would go
+> further and say that the use of interfaces -- at all -- is unusual.
+
+Having used languages with interfaces, my experience is that they eventually get
+used a lot, so I think you are generalizing from inadequate experience.
+
+> ... So by definition
+> anything that happens with them is unusual. (Even if you disagree with
+> me on the value of interfaces, you can't argue that most Ada OOP code
+> is Ada 95 code -- for the simple reason that most Ada compilers only
+> are Ada 95
+> compilers.)
+
+True, but we are designing Ada 2012, not Ada 96.
+
+> But even if they are unusual, we have to have a proper definition for them.
+
+Agreed.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 28, 2011 5:43 PM
+
+> Like some others, I am overwhelmed by the details of the discussion on
+> the exact semantics of Pre'Class and Post'Class. I am concerned about
+> the difficulties of presenting this to users in an intuitive fashion.
+> I am also concerned that with different rules for Pre'Class and Pre
+> the danger is that once again (as Erhard remarked in connection with
+> aspects vs. attributes) the perception will be that Ada always offers
+> two ways of doing roughly the same thing. This perception may be
+> misguided but the complications are plenty real. So here is a timid
+> suggestion: we agree that Pre and Post by themselves are little more
+> that assert statements, and the real meat is in the inheritable and
+> combinable aspects. So what about renaming Pre'Class and Post'Class as
+> Pre and Post, and ditch the non- inheritable versions? For those
+> timid souls that shy away from complex inheritance patterns things
+> will work as they expect, and the others will have to understand how
+> the RM faithfully matches LSP and all is well.
+
+I really do NOT like this suggestion, Pre and Post have a lot of advantages over
+assertions (appear in the spec, can reference 'Old and 'Result, etc), and work
+in a clear and intuitive fashion.
+
+I don't like the whole business of Or'ing for Pre'Class, and having that as the
+ONLY mechanism seems a huge step backwards to me.
+
+If you want to kill anything, kill the Pre'Class and Post'Class.
+
+But I think it is just fine to have both Pre and Pre'Class if you agree they are
+separate, Pre has no inheritance stuff, and Pre'Class is the inherting version
+with weakening.
+
+I would not mind a rule forbidding both Pre and Pre'Class to apply to the same
+function, but I don't think this is necessary.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 28, 2011 5:53 PM
+
+> I remember a long debate with Cyrille at AdaCore, and the conclusion
+> was that it was important to provide both inheritable and a
+> non-inheritable preconditions. I don't believe we should back down on
+> that (despite the legitimate concern about two different ways to do
+> the same thing).
+
+For me it's definitely not the same thing, I agree with the next paragraph
+entirely.
+
+> The fact is Pre and Pre'Class are really two different things, in the
+> same way that T and T'Class are different. Admittedly Ada is unusual
+> among OOP languages in making the distinction between T and T'Class,
+> but I think it was one of the better choices we made in our OOP model.
+> I feel Pre and Pre'Class go hand in hand with the T and T'Class
+> distinction.
+>
+> Getting the right answer is not trivial, but we shouldn't be
+> frightened by the length of the road, but rather be focused on the end
+> result. If we don't like the end result, that is fine (and I
+> understand and appreciate your concern about the "two ways" issue).
+
+There are often good reasons for having two forms for the same thing, we don't
+abandon if statements because they are redundant wrt
+
+ case Bool is
+ when True => ...
+ when False => ...
+ end case
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 28, 2011 5:57 PM
+
+> From your previous paragraph, this does not seem like such a big loss.
+> Either we want inheritance all along, and then we should call it with
+> the shorter name anyway, or else inheritance is a minor convenience
+> and we can drop it. Tuck indicates that Pre'Class is indispensable,
+> but you seem to say that in practice it is only useful at the root of
+> a hierarchy. ???
+
+there is a real divergence here between people who think the Eiffel style
+weakening is essential, and people who see it as useless.
+
+I don't see any hope for a consensus for removing Pre in favor of Pre'Class or
+Pre'Class in favor of Pre.
+
+The only thing that will fly IMO is to have both and keep them separated.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 28, 2011 6:06 PM
+
+> ... There is a lot of OOP stuff that makes sense in theory but never
+> actually happens in practice. Needing to "weaken" the precondition
+> seems to me like there was a bug in the original definition of the
+> precondition (most likely, the boolean functions that make it up are
+> not defined properly). But I am willing to believe that I am wrong --
+> but to do that I'd need to see an example for which the weaker
+> precondition makes sense.
+
+I just don't get the weakening at all. If you have a type extension, then you
+may want preconditions that hold on the extension, which is obviously impossible
+with weakening.
+
+Anyway, I don't mind it being there, even if I don't understand it, but please
+don't take away simple preconditions, which I
+
+(a) understand
+(b) am sure I need
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, March 28, 2011 6:18 PM
+
+> If you have a type extension,
+> then you may want preconditions that hold on the extension, which is
+> obviously impossible with weakening.
+>
+
+I think the way this is usually done is with a dispatching call in your
+precondition (e.g., a dispatching call to Is_Valid).
+
+> I don't see any hope for a consensus for removing Pre in favor of
+> Pre'Class or Pre'Class in favor of Pre.
+>
+> The only thing that will fly IMO is to have both and keep them
+> separated.
+
+I agree.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 6:26 PM
+
+> The only thing that will fly IMO is to have both and keep them
+> separated.
+
+I agree. Keeping them separated is new, in that the previously approved rules
+did not do that. But I do think that is a clear improvement over the older
+rules.
+
+I've been trying to keep these changes to "minor tweaks" to the rules, and while
+we've expanded the changes somewhat beyond that, the changes are almost totally
+focused on improving the semantics dispatching calls. Very little is changed
+about the handling of non-dispatching calls.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 6:21 PM
+
+> > ... The "overdraw" example is better. But I still don't think that
+> > these examples are likely to occur often in practice. Maybe the
+> > people who think everything in the world should be written by OOP
+> > would run into them, but those people are nuts. :-)
+>
+> Why do people use inheritance at all? One reason is because they have
+> hierarchies of abstractions of increasing complexity.
+
+Those are the people that are nuts. ;-) [Please note the smiley faces here...]
+
+I use inheritance in order to share implementation (and to a lesser extent
+usage) of closely related abstractions. Any "hierarchy" beyond the first level
+is often a complete accident and is rarely planned.
+
+Aside: This emphasis on implementation sharing is one of the reasons that I find
+interfaces to not be that valuable. Since they cannot have any implementation,
+there is nothing that can be shared. Regular abstract types can implement the
+parts of the abstraction that are common to all of the entities, and that is
+much more valuable IMHO. I also note that all forms of abstract types interfere
+with the agile-like development process that I've always used, as you have to
+provide implementations of all of the routines before you can compile any. In
+extreme cases such as the Claw Builder, it can take several days of work to get
+even a framework compliable, which increases the possibility for programming
+into dead-ends all that much more. End aside.
+
+I realize that there are all these fancy theories about hierarchies of
+abstractions, but such things tend not to appear in practice. (At least not in
+*my* practice!) Most of the examples show much smaller increments of
+functionality than would make sense in practice. So I remain dubious about the
+true value of these things.
+
+> I think we should be very wary of trying to predict exactly how people
+> will use these capabilities.
+
+I agree with this. I don't buy the "weakening" arguments that much, but what I
+do buy is the need to support interfaces in some consistent way (given the fact
+that we have them). And that appears to require "weakening", because the other
+choices don't make any sense.
+
+> Bob and I came up
+> with a few examples, and could almost certainly come up with more and
+> better examples if we felt the need, but at some point, you have to
+> agree that OOP involves hierarchies where what changes as you go down
+> the hierarchy is very much application specific. If we start saying
+> that this or that abstraction is a "bad idea," we are going out on a
+> pretty fragile limb in my view.
+
+And if you take remarks made with smiley faces following them as serious
+pronouncements, you are already at the end of that limb...
+
+As far as your original "extensible array" example, I was specifically saying
+that that example itself is a "bad idea". Specifically, the idea of a data
+structure that automatically expands on writes is a *bad idea*, irrespective of
+how that is accomplished. Writes to the wrong places need to be detected, not
+covered up by a data structure. If you want to expand your data structure, it is
+very important that you do that explicitly (as in Ada.Containers.Vectors).
+
+Because the example itself is a lousy idea, the example did not do much for me
+as an example of "weakening" of preconditions (or an example of anything else,
+for that matter). That does not say anything about whether "weakening" of
+preconditions is useful or not, or whether there are similar examples that are
+not related to an obviously bad idea (there probably are).
+
+I'm pretty much of the opinion that this is truly a case-by-case situation.
+Let me show you the example that I have been thinking about where "weakening" is
+exactly wrong. Probably there is something wrong with my OOP design, but I can't
+quite imagine what it would be.
+
+ package Root is
+ type Root_Window is limited tagged private;
+
+ function Exists (W : in Root_Window) return Boolean;
+
+ procedure Draw (W : in Root_Window; What : Drawing)
+ with Pre'Class => Exists (W));
+ end Root;
+
+ with Root; use Root;
+ package Visible is
+ type Visible_Window is new Root_Window with private;
+
+ function Is_Visible (W : in Visible_Window) return Boolean;
+
+ procedure Show (W : in Visible_Window)
+ with Pre'Class => Exists (W),
+ Post'Class => Is_Visible (W);
+
+ procedure Draw (W : in Visible_Window; What : Drawing)
+ with Pre'Class => Is_Visible (W);
+ end Visible;
+
+Assume that Visible.Draw is only supported for Visible windows.
+
+The added precondition is Is_Visible (W) does not have the right effect: it
+gives Draw a precondition of Exists (W) or Is_Visible (W), while we really want
+Exists (W) and Is_Visible (W).
+
+So we either have to use Pre instead of Pre'Class (meaning that the precondition
+is not inherited by any later extensions; it might be forgotten or incorrectly
+copied), or we have to flatten out the hierarchy. There is no way to fix the
+precondition in Root, because it simply does not know about this property of a
+window; there is nothing we can write there that would include the Visible
+property. Nor can we change the meaning of Exists, as the precondition of Show
+notes (it would be wrong if Exists included visibility).
+
+It seems to me that something like this can happen anytime an extension adds a
+property to a type. And that seems like something that is common, especially
+when interfaces are used. It surely is application-dependent as to how those new
+properties affect the existing inherited routines, and it might even differ from
+routine to routine.
+
+The net effect is that I don't find "weakening" very compelling, but I do
+realize that the logic of dispatching calls does not allow anything else. Thus I
+think most of the time in practice, we will be requiring an unchanged class-wide
+precondition. I think that is what book authors should concentrate on, not these
+bizarre corner cases where "weakening" actually works. But I am not going to
+argue too much about "weakening", either, because it will occasionally be useful
+(especially with interfaces).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 6:29 PM
+
+> I think the way this is usually done is with a dispatching call in
+> your precondition (e.g., a dispatching call to Is_Valid).
+
+Correct. I expect that to be common; but in that case the precondition is
+unchanged on the new routine.
+
+The next most common case is the one of additional new properties in the
+extension that need to be reflected in the precondition (see the message that
+crossed with yours), but that doesn't work with weakening.
+
+The least likely case (IMHO) is the one in which weakening will in fact work.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, March 28, 2011 6:33 PM
+
+> Assume that Visible.Draw is only supported for Visible windows.
+Well, there goes Liskov substitutability.
+
+I'm not saying that automatically makes this a bad design, but it shouldn't be a
+surprise if it doesn't work well with language constructs that were designed to
+support LSP.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 6:35 PM
+
+...
+> But I think it is just fine to have both Pre and Pre'Class if you
+> agree they are separate, Pre has no inheritance stuff, and Pre'Class
+> is the inherting version with weakening.
+>
+> I would not mind a rule forbidding both Pre and Pre'Class to apply to
+> the same function, but I don't think this is necessary.
+
+I had once made a suggestion to that effect, but I am no longer in favor of it.
+The reason that the rule was needed was to prevent "counterfeiting" from Pre
+being added to a descendant. But since we've separated the meaning of them, that
+is no longer a problem.
+
+And it would seem to be a usability annoyance. If you have a newly added
+property that you need to enforce on some descendant routine, you can use Pre to
+do that. It is not ideal, but at least statically bound calls will get the
+advantages of a proper precondition (dispatching calls will have the possibility
+of an assertion failure). If we disallowed having both, you'd have to use an
+assertion inside of the body. That would be a step backwards for a statically
+bound call.
+
+It doesn't seem to make much sense to have both types on a single subprogram,
+but it's not clear that added Legality Rules help anything, either. I'm sure
+AdaControl will have a reasonable set of policies for programmers to use.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 28, 2011 6:45 PM
+
+> I agree. Keeping them separated is new, in that the previously
+> approved rules did not do that. But I do think that is a clear
+> improvement over the older rules.
+
+I always assumed they should be separated, that's what we implemented in GNAT as
+far as I remember :-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 28, 2011 9:01 PM
+
+> > Assume that Visible.Draw is only supported for Visible windows.
+> Well, there goes Liskov substitutability.
+
+I suppose, but I don't much care about ivory-tower principles. If you have this
+problem (an added property affecting existing operations), you need a mechanism
+to solve it. That's especially true if you are extending an existing type whose
+specifications you can't change - I don't think there is any way to preverve the
+Liskov property in that case. (Raising some random exception rather than writing
+a proper precondition doesn't change anything.)
+
+> I'm not saying that automatically makes this a bad design, but it
+> shouldn't be a surprise if it doesn't work well with language
+> constructs that were designed to support LSP.
+
+OK, but I'm more concerned that there be a way to model whatever design that you
+need rather than worrying about whether we meet some abstract model which may or
+may not be appropriate.
+
+In any case, I'd rather depend on the rules that Ada currently uses to make
+Liskov work (the contract shall not change) than some rules that allow the
+contract to change a little bit, and in a way that is rarely of any use. That is
+more confusing than helpful, at least for my pea brain. :-) But I suppose
+education can help there, and I don't see much reason to diverge too far from
+existing practice in this area (that is, Eiffel).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, March 29, 2011 1:03 AM
+
+>> ... There is a lot of OOP stuff that makes sense in theory but never
+>> actually happens in practice. Needing to "weaken" the precondition
+>> seems to me like there was a bug in the original definition of the
+>> precondition (most likely, the boolean functions that make it up are
+>> not defined properly). But I am willing to believe that I am wrong --
+>> but to do that I'd need to see an example for which the weaker
+>> precondition makes sense.
+>
+> I just don't get the weakening at all. If you have a type extension,
+> then you may want preconditions that hold on the extension, which is
+> obviously impossible with weakening.
+
+Right. "Weakening" seems to be a consequence of strictly following the Liskov
+Substitutability Principle (LSP). But I've seen people writing for years that
+that "principle" has dubious effects. So I suspect that we're just having a
+corner of a debate about the appropriateness of LSP (only) as compared to a more
+general model. And Ada currently has a more general model, so cramming
+preconditions into an LSP-only model is confusing and frustrating.
+
+But there doesn't seem to be any alternative if we want some sort of
+analyzability for dispatching calls (in the absence of the complete source
+code). And not being able to analyze them means that people will have to make a
+choice between compile-time checked code and OOP with dispatching -- not the
+sort of choice that I think we want to forcing people to make.
+
+> Anyway, I don't mind it being there, even if I don't understand it,
+> but please don't take away simple preconditions, which I
+>
+> (a) understand
+> (b) am sure I need
+
+I agree. I think it is possible to make sense out of Pre'Class (Post'Class is
+works the way you'd expect, so nothing worrisome there) if you follow some
+simple rules:
+(1) Never mix Pre and Pre'Class on a single subprogram;
+(2) For new primitive routines, only use Pre'Class if at all possible (it's a
+ part of the contract of any overriding routine);
+(3) For overriding routines, only use Pre'Class if you are certain the
+ "weakening" works -- otherwise, use Pre;
+(4) The combination of interfaces, preconditions, and existing routines that
+ have preconditions is a disaster waiting to happen -- avoid any multiple
+ inheritance cases for primitive routines of interfaces.
+
+(4) is more a function of not having any idea of how to make these work usefully
+than any well-thought out reason; the problem is that "weakening" means that the
+weaker precondition (often "True") is the one that will be used, and that is
+hardly ever going to be what you want. It probably can only work if the
+preconditions are effectively the same. (Well, discounting the type of people
+that somehow writes everything to be compatible with LSP.)
+
+****************************************************************
+
Questions? Ask the ACAA Technical Agent