!standard 6.1.1(7/4) 15-06-17 AI05-0170-1/01 !standard 6.1.1(18.2/4) !standard 7.3.2(5/4) !class binding interpretation 15-06-17 !status work item 15-06-17 !status received 15-06-15 !priority Low !difficulty Medium !qualifier Clarification !subject Abstract subprogram calls in class-wide precondition expressions !summary ** TBD. !question Consider: package Pkg is type Ifc is interface; function F1 (X : Ifc) return Boolean is abstract; function F2 (Y : Ifc) return Boolean is abstract with Pre'Class => F1 (Y); end Pkg; Does the call to F1 violate the rule against non-dispatching calls to abstract subprograms? (Surely, there are no exceptions to this rule. ;-) Recall that any type is a descendant of itself. So 6.1.1(18.2/4) which applies to primitive operations of descendants of a type T The primitive subprogram S is illegal if it is not abstract and the corresponding expression for a Pre'Class or Post'Class aspect would be illegal. also applies to the original operation of T itself. This makes the example legal, but it would allow all sorts of things that we would not want to allow. So clearly that is not the intent. !recommendation (See Summary.) !wording Modify 6.1.1(7/4): Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram S of a tagged type T, a name that denotes a formal parameter (or S'Result) of type T is interpreted as though it had a (notional) {nonabstract} type NT that is a formal derived type whose ancestor type is T, with directly visible primitive operations. Similarly, a name that denotes a formal access parameter (or S'Result) of type access-to-T is interpreted as having type access-to-NT. The result of this interpretation is that the only operations that can be applied to such names are those defined for such a formal derived type. Modify 6.1.1(18/4): If a Pre'Class or Post'Class aspect is specified for a primitive subprogram S of a tagged type T, or such an aspect defaults to True, then a corresponding expression also applies to the corresponding primitive subprogram S of each descendant of T {(other than T itself)}. The corresponding expression is constructed from the associated expression as follows: Modify 7.3.2(5/4): Within an invariant expression, the identifier of the first subtype of the associated type denotes the current instance of the type. Within an invariant expression for the Type_Invariant aspect of a type T, the type of this current instance is T. Within an invariant expression for the Type_Invariant'Class aspect of a type T, the type of this current instance is interpreted as though it had a (notional) type NT that is a visible formal derived type whose ancestor type is T. The effect of this interpretation is that the only operations that can be applied to this current instance are those defined for such a formal derived type. !discussion 6.1.1(18-18.2/4) was intended to apply only to operations of actual descendants and not to the original operation. 6.1.1(18.1/4) doesn't make much sense otherwise, and one cannot daisy-pick readings that they like for individual phrases. Even so, we clarify the wording. We also clarify 6.1.1(7/4) (and the similar 7.3.2(5/4)) to make it clear that the notional type NT is not abstract, since we want the expression to work in non-abstract contexts. Having done this, the original question is easy to answer: no, the call is not legal. However, that seems weird because such an expression makes sense. Note, however, that other expressions that "make sense" have never been allowed in Ada. For instance, consider: package Pkg2 is type T is interface; function Empty return T is abstract; procedure Init (X : out T; Value : T := Empty) is abstract; end Pkg2; Empty is clearly illegal here, because it is not a dispatching call; it violates 3.9.3(7). (That rule is not conditional on the context.) It's tempting to think this was a mistake, but it should be obvious that such a call only works in calls where the controlling tag comes from somewhere else. Most such expressions could never have a legal call: package Pkg3 is type T is interface; function Empty return T is abstract; function Length (Value : T := Empty) return Integer is abstract; end Pkg3; A call of Length using the default parameter would end up statically bound to T, which is not a call we want to allow. Since this has been true since Ada 95 (replace "interface" with "abstract tagged null record" and you have Ada 95 code), and all Ada 95 compilers tested reject this, we leave well-enough alone. (It seems unlikely that this is important, as if it was we would have heard about it by now - it's been 20 years since Ada 95 was approved and 8 years since Ada 2005 was approved.) [Editor's note: I tried the Ada 95 example on both GNAT and Janus/Ada; both rejected the call of "Empty". I suspect that there is an ACATS test that requires this. Changing something here strikes me as answering a question not asked. Why make work for implementers?] ** TBD. [Editor's note: I have no solution for the original question. The problem here is that an abstract function has to be called in a dispatching call, but Pre'Class (post AI12-0113-1) expressions are usually statically bound. On top of which, 3.9.3(7) is not context dependent. Declaring that NT is abstract in this case does not help - 3.9.3(7) still applies. The only way that I can see to do this is to make an exception for 3.9.3(7) in the case when the expression is used directly in some expression of an abstract operation ("some expression" = precondition, postcondition, default expression of a parameter of an abstract type, more???). But then there has to be some recheck on a call, else nonsense like the Length call above or its Pre'Class counterpart would be allowed. For instance, we can't allow: package Pkg4 is type Ifc is interface; function Empty return IFc is abstract; function Length (Value : IFc) return Integer is abstract; function F3 (Y : Ifc) return Boolean is abstract with Pre'Class => Length(Empty) /= 0; end Pkg4; if F3 (Ifc'Class(Some_Obj)) then The call to F3 here would call the abstract Empty and Length, because the tag indeterminant call to Empty would use the tag of its specific type (as there is no other controlling tag to use). That we cannot allow. Rechecking legality rules for defaults and pre/post on a call is a new concept; we don't do that currently, and it would seem to be a major headache to implement. Thus I lean toward not fixing the problem at all. The code can be made legal by explicitly forcing the calls to be dispatching -- and any other solution looks worlds worse. Specifically: package Pkg5 is type Ifc is interface; function F1 (X : Ifc) return Boolean is abstract; function F2 (Y : Ifc) return Boolean is abstract with Pre'Class => F1 (Ifc'Class(Y)); end Pkg5; !ASIS No ASIS effect. !ACATS test !appendix From: Steve Baird Sent: Monday, June 15, 2015 3:06 PM In some internal discussions at AdaCore, we've been looking at this example: package Pkg is type Ifc is interface; function F1 (X : Ifc) return Boolean is abstract; function F2 (Y : Ifc) return Boolean is abstract with Pre'Class => F1 (Y); end; and the question is whether the call to F1 violates the rule against non-dispatching calls to abstract subprograms. I believe AI12-0113's authors/approvers intended that this example should be legal. Does the wording of the AI correctly capture this intent? Recall that any type is a descendant of itself. So the new 6.1.1 rule about primitive operations of descendants of a type T The primitive subprogram S is illegal if it is not abstract and the corresponding expression for a Pre'Class or Post'Class aspect would be illegal. also applies to the original operation of T itself. That suggests that the function declaration F2 is legal (because it is abstract) and all is well. But couldn't the same reasoning be used to justify all sorts of things that we don't want to allow, such as procedure P3 (Z : Ifc) is abstract with Pre'Class => (Some_Function_With_An_In_Out_Parameter (Some_Constant)); ? Do we need to more precisely specify the set of "normally illegal" constructs that are legal in the Pre'Class or Post'Class aspect of an abstract subprogram? Tuck suggested another approach: > I always interpreted 18/4-18.2/4 to only apply to inherited > interpretations, where "descendant of T" should have been "descendant of T > (other than T itself)". As Tuck pointed out, stating that intent explicitly solves the problem with accepting the P3 example (which we want to reject) but it also takes us back to rejecting the original F2 example (which we want to accept). So consider following wording (also introduced in AI12-0113): Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram {S} of a tagged type T, a name that denotes a formal parameter {(or S'Result)} of type T is interpreted as [having type T'Class] {though it had a (notional) type NT that is a formal derived type whose ancestor type is T, with directly visible primitive operations} We never say anything one way or the other about the abstractness of this notional derived type and of its primitive operations; this seems like a hole in any case. If we stated explicitly that these notional guys are never abstract and also incorporated Tuck's suggestion, then perhaps that would get us to where we want to be. Thoughts? Tuck also suggested that an another case where we might consider the status of the usual "no non-dispatching calls to abstract subprograms" rule is a default expression for a controlling formal parameter of an abstract subprogram, as in package Pkg2 is type T is interface; function Empty return T is abstract; procedure Init(X : out T; Value : T := Empty) is abstract; end; . Is the call to Empty currently legal? Do we want it to be legal? **************************************************************** From: Tucker Taft Sent: Monday, June 15, 2015 4:06 PM > So consider following wording (also introduced in AI12-0113): > > Within the expression for a Pre'Class or Post'Class aspect for a > primitive subprogram {S} of a tagged type T, a name that denotes a > formal parameter {(or S'Result)} of type T is interpreted as [having > type T'Class] {though it had a (notional) type NT that is a formal > derived type whose ancestor type is T, with directly visible > primitive operations} > > We never say anything one way or the other about the abstractness of > this notional derived type and of its primitive operations; this seems > like a hole in any case. If we stated explicitly that these notional > guys are never abstract and also incorporated Tuck's suggestion, then > perhaps that would get us to where we want to be. I would have said "of course the notional derived type is non abstract" but I guess we really should say that explicitly! ... > . Is the call to Empty currently legal? Do we want it to be legal? I believe Empty ought to be legal in this case **************************************************************** From: Randy Brukardt Sent: Monday, June 15, 2015 4:49 PM > In some internal discussions at AdaCore, we've been looking at this > example: > > package Pkg is > type Ifc is interface; > > function F1 (X : Ifc) return Boolean is abstract; > > function F2 (Y : Ifc) return Boolean is abstract > with Pre'Class => F1 (Y); > end; > > and the question is whether the call to F1 violates the rule against > non-dispatching calls to abstract subprograms. > > I believe AI12-0113's authors/approvers intended that this example > should be legal. As Tucker points out, this never was legal in Ada for default expressions (at least if one follows the letter of the wording), which is similar to the uses for preconditions/postconditions (as we noted last month for protected operations). So this example has nothing to do with AI12-0113-1, but rather is a more general bug in Ada. > Does the wording of the AI correctly capture this intent? > > Recall that any type is a descendant of itself. > > So the new 6.1.1 rule about primitive operations of descendants of a > type T > > The primitive subprogram S is illegal if it is not abstract and > the > corresponding expression for a Pre'Class or Post'Class aspect > would > be illegal. > > also applies to the original operation of T itself. I agree with Tucker that it doesn't mean that; it only applies to inherited Pre'Class/Post'Class operations. Probably we need to add the parenthetical remark "(other than T itself)" -- this mistake we make often because my "descendant"s do not typically include me (so the use is a bit off compared to the English meaning of the word). ... > As Tuck pointed out, stating that intent explicitly solves the problem > with accepting the P3 example (which we want to > reject) but it also takes us back to rejecting the original > F2 example (which we want to accept). The original example *is* illegal; there is no provision in Ada to allow that anywhere. Hacking preconditions for this doesn't solve anything; we need to fix the underlying problem (or leave it unchanged). > So consider following wording (also introduced in AI12-0113): > > Within the expression for a Pre'Class or Post'Class aspect for a > primitive subprogram {S} of a tagged type T, a name that denotes a > formal parameter {(or S'Result)} of type T is interpreted as [having > type T'Class] {though it had a (notional) type NT that is a formal > derived type whose ancestor type is T, with directly visible > primitive operations} > > We never say anything one way or the other about the abstractness of > this notional derived type and of its primitive operations; this seems > like a hole in any case. If we stated explicitly that these notional > guys are never abstract and also incorporated Tuck's suggestion, then > perhaps that would get us to where we want to be. I'm not sure what the effect of not considering these objects abstract is. I fear that you'll come up with lots of interesting anomolies in that case. > Tuck also suggested that an another case where we might consider the > status of the usual "no non-dispatching calls to abstract subprograms" > rule is a default expression for a controlling formal parameter of an > abstract subprogram, as in > > package Pkg2 is > type T is interface; > > function Empty return T is abstract; > procedure Init(X : out T; Value : T := Empty) is abstract; > end; > > . Is the call to Empty currently legal? Do we want it to be legal? No. Seems like the answer should be Yes. I suggest we fix these two problems the same way, because they're really the same problem. Preferably by adjusting the root rule and not by hacking around with special cases (because we'll never remember all of them). ****************************************************************