!standard 6.1.1(7/3) 14-11-19 AI12-0113-1/03 !standard 6.1.1(18/3) !standard 6.1.1(37/3) !standard 6.1.1(38/3) !class binding interpretation 14-05-15 !status Corrigendum 1-2012 14-11-19 !status WG9 Approved 15-06-26 !status ARG Approved 7-0-1 14-10-18 !status work item 14-05-15 !status received 14-04-25 !priority Medium !difficulty Hard !qualifier Omission !subject Class-wide preconditions and statically bound calls !summary Class-wide preconditions, postconditions, and type invariants are processed using the actual types for the parameters of type T (not always using T'Class). In particular, for a statically bound call, the calls within the Pre'Class expression are statically bound. !question 6.1.1(7.3) says that, a parameter having type T is interpreted as having type T'Class. That interpretation means that any call to a primitive operation of T is a dispatching call. Effectively, the parameter has an implicit conversion to T'Class. For a statically bound call when the tag of the parameter identifies a different type than its nominal type, this means that a different body would be executed than would be executed for the equivalent Pre. That means that Pre'Class is not quite equivalent to a set of identical Pre aspects with an additional guarentee for future overridden subprograms. But that was the intent: that Pre'Class be LSP-safe but otherwise be equivalent to putting the same Pre on every related subprogram. The implicit redispatching implied by 6.1.1(7/3) makes static analysis harder, as a tool cannot plug in the body of a subprogram called from Pre'Class even if the tool knows the contents of that body, because the call might dispatch to some other body. Should this be corrected somehow? (Yes.) !recommendation (See Summary.) !wording Modify 6.1.1(7/3): 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}. 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} [T'Class]. [Redundant: {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.} This ensures that the expression is well-defined for a primitive subprogram of [a]{any} type descended from T.] (In Static Semantics) Modify 6.1.1(18/3) as follows: 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} [the associated expression] also applies to the corresponding primitive subprogram {S} of each descendant of T. {The *corresponding expression* is constructed from the associated expression as follows: * References to formal parameters of S (or to S itself) are replaced with references to the corresponding formal parameters of the corresponding inherited or overriding subprogram S (or to the corresponding subprogram S itself).} AARM Reason: We have to define the corresponding expression this way as overriding routines are only required to be subtype conformant; in particular, the parameter names can be different. So we have to talk about corresponding parameters without mentioning any names. 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. AARM Reason: We allow illegal corresponding expressions on abstract subprograms as they could never be evaluated, and we need to allow such expressions to contain calls to abstract subprograms. (In Dynamic Semantics) Modify 6.1.1(37/3): For any subprogram or entry call {S} (including dispatching calls), the checks that are performed to verify specific precondition expressions and specific and class-wide postcondition expressions are determined by those for the subprogram or entry actually invoked. Note that the class-wide postcondition expressions verified by the postcondition check that is part of a call on a primitive subprogram of type T includes all class-wide postcondition expressions originating in any progenitor of T[Redundant:, even if the primitive subprogram called is inherited from a type T1 and some of the postcondition expressions do not apply to the corresponding primitive subprogram of T1]. {Any operations within a class-wide postcondition expression that were resolved as primitive operations of the (notional) formal derived type NT, are in the evaluation of the postcondition bound to the corresponding operations of the type identified by the controlling tag of the call on S. [Redundant: This applies to both dispatching and non-dispatching calls on S.]} Modify 6.1.1(38/3) as follows: The class-wide precondition check for a call to a subprogram or entry {S} consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily {to} the one that is invoked). {Any operations within such an expression that were resolved as primitive operations of the (notional) formal derived type NT, are in the evaluation of the precondition bound to the corresponding operations of the type identified by the controlling tag of the call on S. [Redundant: This applies to both dispatching and non-dispatching calls on S.]} !discussion Consider two nearly identical hierarchies of types. First: package P11 is type Root is abstract tagged private; function Is_Valid (P : in Root) return Boolean; procedure Proc (P : in Root) with Pre => Is_Valid(P); procedure Proc2 (P : in Root); private ... end P11; with P11; package P12 is type Child is new P11.Root with private; overriding function Is_Valid (P : in Child) return Boolean; overriding procedure Proc (P : in Child) with Pre => Is_Valid(P); -- Proc2 inherited. private ... end P12; with P12; package P13 is type GrandChild is new P12.Child with private; overriding function Is_Valid (P : in Grandchild) return Boolean; overriding procedure Proc (P : in Grandchild) with Pre => Is_Valid(P); -- Proc2 inherited. private ... end P13; and the second hierarchy is: package P21 is type Root is abstract tagged private; function Is_Valid (P : in Root) return Boolean; procedure Proc (P : in Root) with Pre'Class => Is_Valid(P); procedure Proc2 (P : in Root); private ... end P21; with P21; package P22 is type Child is new P21.Root with private; overriding function Is_Valid (P : in Child) return Boolean; overriding procedure Proc (P : in Child); -- Proc2 inherited. private ... end P22; with P22; package P23 is type GrandChild is new P22.Child with private; overriding function Is_Valid (P : in Grandchild) return Boolean; overriding procedure Proc (P : in Grandchild); -- Proc2 inherited. private ... end P23; The only difference between these hierarchies is that the first uses a specific Pre on each declaration of Proc, while the second uses a class-wide Pre on the first declaration of Proc and allows it to be inherited on the others. Our intent is that these behave identically at runtime, with the only difference being that there is an additional guarantee that a new descendant of P21.Root will also have the Pre'Class expression (that has to be manually added in the other hierarchy). The additional guarantee allows analyzing dispatching calls without knowing the exact body that they will reach, as we know that all bodies will have the precondition Pre'Class. Such analysis can only be done for the P11 hierarchy via full program analysis. --- We define the meaning of Pre'Class in terms of a nominal formal derived type in order that only primitive operations of the type can be used in the expression. The original Ada 2012 definition of the types as T'Class also has a runtime effect that we do not want (as noted above). In addition, defining the parameters as having T'Class introduces other problems. For instance, with a global variable: type T is tagged ...; G : T'Class := ...; function Is_Valid_2 (A, B : T) return Boolean; procedure Proc (X : T) with Pre'Class => Is_Valid_2 (X, G); If X is considered to have T'Class, this expression is legal (both operands being dynamically tagged). But this doesn't make sense for an inherited type: type T1 is new T with ...; -- inherits Is_Valid_2 (A, B : T1) return Boolean; -- inherits Proc (X : T) -- with Pre'Class => Is_Valid_2 (X, G); But this Pre'Class makes no sense, as G does not match type T1. If we simply left the parameters having type T, then non-primitive operations of the type could be used in Pre'Class -- but descendant types have no such operations. We could have rechecked the Pre'Class for each later subprogram, but that causes problems if visibility has changed somehow (especially for class-wide operations). On the other hand, a formal derived type has just the operations that we want to allow (primitive operations) but no others. In particular, G in the example above does not match the NT type, so the above problem can't happen. --- We have to recheck the legality of the corresponding expression, just like in a generic instantiation. In particular, a call to a primitive subprogram could be illegal because it is abstract: package Pkg3 is type T is abstract tagged null record; function Is_Ok (X : T) return Boolean is abstract; procedure Proc (X : T) with Pre'Class => Is_Ok (X); -- Illegal. end Pkg3; (Note that Proc could be called in a statically bound call with a type conversion of some object to T.) We can't just check this once, because whether a routine is abstract can be changed when deriving: package Pkg4 is type T is tagged null record; function Is_Ok (X : T) return Boolean; procedure Proc (X : T) with Pre'Class => Is_Ok (X); -- OK. end Pkg4; with Pkg4; package Pkg5 is type NT is abstract new Pkg4.T null record; function Is_Ok (X : NT) return Boolean is abstract; -- inherits Proc, Pre'Class => Is_Ok (X); -- Illegal. end Pkg5; We don't check this for abstract routines, since a statically bound call is illegal, and there cannot be objects with the tag of an abstract type, so there can't be any dispatching calls that land there, either. Note carefully that resolution is not redone (again like a generic instantiation); only the legality checks. The resolution of global variables and the like is unchanged from the original expression. --- We've added a mention that even the implicit Pre'Class of True is inherited. That follows from the Liskov Substitution Principle -- the precondition of an overridden routine has to be the same or weaker than that of the parent routine. There is nothing weaker than True, so if a routine does not have an explicit Pre'Class, it can't usefully be given a Pre'Class later in the derivation tree. This topic is further explored in AI12-0131-1. !corrigendum 6.1.1(7/3) @drepl Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram of a tagged type @i, a name that denotes a formal parameter of type @i is interpreted as having type @i'Class. Similarly, a name that denotes a formal access parameter of type access-to-@i is interpreted as having type access-to-@i'Class. This ensures that the expression is well-defined for a primitive subprogram of a type descended from @i. @dby Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram @i of a tagged type @i, a @fa that denotes a formal parameter (or @i'Result) of type @i is interpreted as though it had a (notional) type @i that is a formal derived type whose ancestor type is @i, with directly visible primitive operations. Similarly, a @fa that denotes a formal access parameter (or @i'Result) of type access-to-@i is interpreted as having type access-to-@i. The result of this interpretation is that the only operations that can be applied to such @fas are those defined for such a formal derived type. This ensures that the expression is well-defined for any primitive subprogram of a type descended from @i. !corrigendum 6.1.1(18/3) @drepl If a Pre'Class or Post'Class aspect is specified for a primitive subprogram of a tagged type @i, then the associated expression also applies to the corresponding primitive subprogram of each descendant of @i. @dby If a Pre'Class or Post'Class aspect is specified for a primitive subprogram @i of a tagged type @i, or such an aspect defaults to True, then a corresponding expression also applies to the corresponding primitive subprogram @i of each descendant of @i. The @i is constructed from the associated expression as follows: @xbullet (or to @i itself) are replaced with references to the corresponding formal parameters of the corresponding inherited or overriding subprogram @i (or to the corresponding subprogram @i itself).> The primitive subprogram @i is illegal if it is not abstract and the corresponding expression for a Pre'Class or Post'Class aspect would be illegal. !corrigendum 6.1.1(37/3) @drepl For any subprogram or entry call (including dispatching calls), the checks that are performed to verify specific precondition expressions and specific and class-wide postcondition expressions are determined by those for the subprogram or entry actually invoked. Note that the class-wide postcondition expressions verified by the postcondition check that is part of a call on a primitive subprogram of type @i includes all class-wide postcondition expressions originating in any progenitor of @i, even if the primitive subprogram called is inherited from a type @i and some of the postcondition expressions do not apply to the corresponding primitive subprogram of @i. @dby For any subprogram or entry call @i (including dispatching calls), the checks that are performed to verify specific precondition expressions and specific and class-wide postcondition expressions are determined by those for the subprogram or entry actually invoked. Note that the class-wide postcondition expressions verified by the postcondition check that is part of a call on a primitive subprogram of type @i includes all class-wide postcondition expressions originating in any progenitor of @i, even if the primitive subprogram called is inherited from a type @i and some of the postcondition expressions do not apply to the corresponding primitive subprogram of @i. Any operations within a class-wide postcondition expression that were resolved as primitive operations of the (notional) formal derived type @i, are in the evaluation of the postcondition bound to the corresponding operations of the type identified by the controlling tag of the call on @i. This applies to both dispatching and non-dispatching calls on @i. !corrigendum 6.1.1(38/3) @drepl The class-wide precondition check for a call to a subprogram or entry consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily the one that is invoked). @dby The class-wide precondition check for a call to a subprogram or entry @i consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily to the one that is invoked). Any operations within such an expression that were resolved as primitive operations of the (notional) formal derived type @i, are in the evaluation of the precondition bound to the corresponding operations of the type identified by the controlling tag of the call on @i. This applies to both dispatching and non-dispatching calls on @i. !ASIS No ASIS effect. !ACATS test An ACATS C-Test ought to ensure that no redispatching occurs in statically bound calls. !appendix From: Randy Brukardt Sent: Friday, April 25, 2014 6:43 PM This is an issue that has been bothering me for a long time. Originally, I noticed it in thinking about an ARG discussion toward the end of the Ada 2012 work. I didn't want to hold up completion of the standard to fix this, so I kept it to myself. Since, I think I've mentioned it in conversation periodically, but I don't think we've ever opened an AI to address it. So let me bore you to tears^H^H^H^H^H^H^H^H^H^H^H explain in detail this issue. (The issue also occurs for Post'Class and probably for Type_Invariant'Class but I'm not going to explain those here.) Consider the two nearly identical hierarchies of types. First: package P11 is type Root is abstract tagged private; function Is_Valid (P : in Root) return Boolean; procedure Proc (P : in Root) with Pre => Is_Valid(P); procedure Proc2 (P : in Root); private ... end P11; with P11; package P12 is type Child is new P11.Root with private; overriding function Is_Valid (P : in Child) return Boolean; overriding procedure Proc (P : in Child) with Pre => Is_Valid(P); -- Proc2 inherited. private ... end P12; with P12; package P13 is type GrandChild is new P11.Child with private; overriding function Is_Valid (P : in Grandchild) return Boolean; overriding procedure Proc (P : in Grandchild) with Pre => Is_Valid(P); -- Proc2 inherited. private ... end P13; and the second hierarchy is: package P21 is type Root is abstract tagged private; function Is_Valid (P : in Root) return Boolean; procedure Proc (P : in Root) with Pre'Class => Is_Valid(P); procedure Proc2 (P : in Root); private ... end P21; with P21; package P22 is type Child is new P21.Root with private; overriding function Is_Valid (P : in Child) return Boolean; overriding procedure Proc (P : in Child); -- Proc2 inherited. private ... end P22; with P22; package P23 is type GrandChild is new P21.Child with private; overriding function Is_Valid (P : in Grandchild) return Boolean; overriding procedure Proc (P : in Grandchild); -- Proc2 inherited. private ... end P23; The only difference between these hierarchies is that the first uses a specific Pre on each declaration of Proc, while the second uses a class-wide Pre on the first declaration of Proc and allows it to be inherited on the others. Note that while the expression appears to be the same for P11.Proc'Pre and P21.Proc'Pre'Class, there is a difference that stems from 6.1.1(7/3). That says that in Pre'Class, a parameter (P in this case) having type T (Root in this case) is interpreted as having type T'Class (Root'Class). That interpretation means that any call to a primitive operation of T (in this case, the call to Is_Valid) is a dispatching call. Effectively, the parameter P is has an implicit conversion to type Root'Class, so the expression is effectively Is_Valid(Root'Class(P)). Now, my understanding of the intent of this feature is that Pre'Class works just like specifying the Pre'Class expression as the Pre of each of the corresponding subprograms for each descendant type. The effect is that the P11 hierarchy and the P21 hierarchy act the same. But Pre'Class also provides a guarantee that any future descendants will also have that precondition; the P11 has no such guarantee. Consider the effect on a dispatching call to Proc. For the P11 hierarchy, the Pre expression will be evaluated after dispatching, appropriately for the actual body dispatched to. But since there is no guarantee that these are the same, we know nothing useful about the precondition at the call site of the dispatching call. (Even if they are all the same, as in this example, a future extension could change that, so making any assumptions is dangerous absent full program analysis.) OTOH, in the case of Pre'Class, we know that any possible body will have the Pre'Class applied, so we know at least that much of the precondition at the call site. One can confidently use that knowledge in program analysis (be it manual or via a program). To get this additional knowledge and confidence is the point of Pre'Class. Note that for a dispatching call, the effect is identical for the P11 and the P21 hierarchies. If we have an object Obj of type Root'Class with a tag of type T, the call Proc(Obj) in the P11 hierarchy will dispatch to the body for T, which will evaluate the Pre expression for T: (Note: I'm prefixing operations with "T'" to describe operations of the specific type T.) Proc(Obj) ==> T'Proc(Obj) ==> T'Pre(Obj) then T'Proc'Body(Obj) ==> T'Is_Valid(Obj) then T'Proc'Body(Obj) For the hierarchy P21 we get (remembering the implicit conversion to T'Class) in Pre'Class and evaluating Pre'Class at the call site): Proc(Obj) ==> T'Pre'Class(Obj) then T'Proc(Obj) ==> Is_Valid(Root'Class(Obj)) then T'Proc'Body(Obj) ==> T'Is_Valid(Obj) then T'Proc'Body(Obj) Note that the effect is ultimately the same either way, in large part because all of the dispatching operations dispatch on the same tag. However, that's not true for a statically bound call. For instance, imagine that within the body of P11.Proc2 and P21.Proc2, we have the call Proc(P). This is a statically bound call for type Root. Using the same notation as above, the call in P11.Proc2 expands to: Proc(P) ==> Root'Proc(P) ==> Root'Pre(P) then Root'Proc'Body(P) ==> Root'Is_Valid(P) then Root'Proc'Body(P) The call in P21.Proc2 expands to: Proc(P) ==> Root'Pre'Class(P) then Root'Proc(P) ==> Is_Valid(Root'Class(P)) then Root'Proc'Body(Obj) Note that here we're redispatching to the tag of P, so we can't say which body is called at runtime. This of course has no negative effect if the tag is actually that of Root (but since Root is abstract here, that's not possible). But if the tag is something else (which is likely, as Proc2 is inherited for the descendant types - the tag would never be Root in any of those inherited bodies), we're going to call a different body of Is_Valid. That means that our initial intent of making these hierarchies act identically is not met for a statically bound call. Moreover, it means that using Pre'Class damages our ability to statically analyze a statically bound call when it enhances our ability to statically analyze a dispatching call -- a trade-off that we don't want to be making. (Imagine, for instance, that the bodies of all of the Is_Valid functions are expression functions. In that case, a static analyzer would know the exact details of the precondition for the P11 hierarchy, but know only that some Is_Valid is called for the P21 hierarchy.) I think it is pretty clear that we don't want this to happen. And the problem is pretty clearly the implicit re-dispatch in the Pre'Class expression. We need to eliminate that (while it would still be possible to explicitly introduce re-dispatch into Pre and Pre'Class if that is desired, it certainly should not be the default behavior). Without the implicit redispatch, these two hierarchies are completely identical (which also shows that such a change is implementable - since we all agree that P11 is implementable). And the only difference is the guarantee that future descendants will also have the Pre'Class expression (which allows more analysis on dispatching calls without making assumptions about the future or having to rely solely on full-program analysis). Lastly, I want to look at how we might accomplish eliminating the implicit redispatch. The first possibility is to just say that it isn't there in the first place. That is, 6.1.1(7/3) is just a name resolution rule, it does not have the effect that it appears to have on the dynamic semantics. We could probably even do that with a To Be Honest note. However, in that case, I'm not sure what the need is to even specify the type to be T'Class. I presume we want the dynamically tagged vs. statically tagged rules to apply at compile-time, and so on. So I think this would be weird. An alternative would be to craft a rule that says that Pre'Class expressions bind just like the call that they are a part of (static binding if the call is statically bound, dispatching if the call is dispatching, and so forth). The problem here is to ensure that we don't affect calls that aren't primitive on the right type. But perhaps the best solution is to combine these and add a rule to say that the type of the name resolution is merely a placeholder and that the expression is evaluated for a particular call using the actual types of the parameters. The name resolution provides identification of the subprograms involved, but how those subprograms are called dynamically depends on the actual types. I'm not quite sure how to word any of these ideas, so I think I'll stop here. I'm sure we can figure this out in Paris over a glass (tumbler??) of Beaujolias. :-) *************************************************************** From: Steve Baird Sent: Monday, July 21, 2014 6:37 PM This is a summary of some internal AdaCore discussions (mostly between Tuck and me) about a possible approach to the problem that Randy identified in AI12-0113 (Class-wide preconditions and statically bound calls). The dynamic semantics of Pre'Class/Post'Class evaluation for a primitive operation of a tagged type T in the case of a non-dispatching (i.e., statically bound) call to Foo could be changed as follows: If a controlling formal parameter of Foo is used as a controlling operand of a call within the Pre'Class expression or the Post'Class expression, then for purposes of determining the controlling tag of that call the (dynamic) tag of the parameter is considered to be T'Tag. Note that the name resolution rules of 6.1.1 are unaffected by this change. At least as stated above, this is purely a dynamic semantics change (but see below). This is, in some sense, the worst kind of incompatible change (i.e., a dynamic semantics change where neither the old nor the new behavior necessarily raises an exception), but there seems to be agreement that the language is broken here and a fix is needed. A couple of corner-case issues have been identified. 1) We don't want a rule like "the controlling tag of the call is T'Tag" because we don't want to bypass the tag equality check in the case where there are multiple controlling operands. Details available upon request. 2) Oddness is possible if the tagged type T in question is abstract. Consider a statically bound call to the following procedure: package Pkg is type T is abstract tagged null record; function Is_Ok (X : T) return Boolean is abstract; procedure Proc (X : T) with Pre'Class => Is_Ok (X); end Pkg; The point is that Proc is not abstract but Is_Ok is. If we are not careful, we end up trying to execute the "body" of an abstract function. One approach to this problem is to view it as an unimportant corner case so that behavior in this situation only needs to be well-defined (as opposed to being useful). Taking this approach, we can just state that the proposed dynamic semantics change doesn't apply if the tagged type T in question is abstract; program behavior in this case is then unaffected by the changes of this AI. A cleaner (but messier at the level of RM wording) approach would be to make such a statically bound call illegal. With the proposed new dynamic semantics, such a call would be equivalent to an illegal construct (i.e., to a non-dispatching call to an abstract subprogram), so by this reasoning it should be illegal. Unfortunately, it would be possible to construct violations of this rule which occur in expanded instance bodies (which are not subject to legality checking) so we would also need a special dynamic semantics rule (presumably Program_Error would be raised) to handle this corner case of a corner case. This comes down to a question of whether capturing this approach in the RM is worth all the verbiage that would be required. Opinions? *************************************************************** From: Tucker Taft Sent: Monday, July 21, 2014 6:49 PM >... 2) Oddness is possible if the tagged type T in question is abstract. > > Consider a statically bound call to the following procedure: > > package Pkg is > type T is abstract tagged null record; > function Is_Ok (X : T) return Boolean is abstract; > procedure Proc (X : T) with Pre'Class => Is_Ok (X); > end Pkg; > > The point is that Proc is not abstract but Is_Ok is. > ... > Opinions? As Steve knows, my opinion is that it is very important that the tag used for calling the subprogram matches the tag used for evaluating the class-wide precondition. Hence, if Pre'Class involves a call on an abstract subprogram, Program_Error is raised. An alternative would be to require that the Pre'Class aspect not include a call on an abstract function if the associated subprogram is non-abstract. Presumably a similar rule could apply to Post'Class. *************************************************************** From: Bob Duff Sent: Tuesday, July 22, 2014 11:15 AM > As Steve knows, my opinion is that it is very important that the tag > used for calling the subprogram matches the tag used for evaluating > the class-wide precondition. Hence, if Pre'Class involves a call on an > abstract subprogram, Program_Error is raised. > > An alternative would be to require that the Pre'Class aspect not > include a call on an abstract function if the associated subprogram is > non-abstract. Presumably a similar rule could apply to Post'Class. Well, we normally try to prevent calls to abstract subprograms via compile-time rules. If you want a run-time check, you declare a concrete subprogram, and write a body that says "raise P_E;", and hopefully override that body whereever appropriate. *************************************************************** From: Randy Brukardt Sent: Tuesday, July 22, 2014 8:08 PM > This is a summary of some internal AdaCore discussions (mostly between > Tuck and me) about a possible approach to the problem that Randy > identified in AI12-0113 (Class-wide preconditions and statically bound > calls). > > The dynamic semantics of Pre'Class/Post'Class evaluation for a > primitive operation of a tagged type T in the case of a > non-dispatching (i.e., statically bound) call to Foo could be changed > as follows: > > If a controlling formal parameter of Foo is used as a > controlling operand of a call within the Pre'Class expression > or the Post'Class expression, then for purposes of determining > the controlling tag of that call the (dynamic) tag of the > parameter is considered to be T'Tag. > > Note that the name resolution rules of 6.1.1 are unaffected by this > change. I think this was one of the ideas I had as a possible solution. It seemed clunky at the time, but it definitely has the right semantics. Tucker seemed to think there was a more elegant way of describing this, but I guess he no longer thinks that? (BTW, this AI is assigned to Tucker and I, so I have an interest in figuring out what a rewrite ought to look like.) > At least as stated above, this is purely a dynamic semantics change > (but see below). This is, in some sense, the worst kind of > incompatible change (i.e., a dynamic semantics change where neither > the old nor the new behavior necessarily raises an exception), but > there seems to be agreement that the language is broken here and a fix > is needed. Right. It's insane that a body can make essentially no assumptions about a Pre'Class precondition, and in particular, the Pre'Class that it knows about may not even be true. Similarly, a body might be subject to Post'Class postconditions that it doesn't know about, causing them to fail. These seemed like an especial problem when they occurred for a call to a parent operation in the implementation of a child operation. The whole point of the child operation would be to ensure those Post'Class conditions; it makes perfect sense that they wouldn't be met at the point of the parent call. An interesting question is whether Type_Invariant'Class has a similar problem. I didn't try to work that out, but it seemed like it might (given the correspondence between postconditions and type invariants). > A couple of corner-case issues have been identified. > > 1) We don't want a rule like "the controlling tag of the call is > T'Tag" because we don't want to bypass the tag equality > check in the case where there are multiple controlling operands. > Details available upon request. That's the other example from the meeting, right? If one of the other parameters is controlling but does not get its tag from the parameters of the call that defines the precondition/postcondition, then it's likely that the tag check will fail. (This is a dumb thing to do in Pre'Class or Post'Class; the other choice would be to statically ban such a call -- since we're only talking about the top-level of calls anyway. But it's not clear that would simplify the wording enough to justify the extra compile-time check.) > 2) Oddness is possible if the tagged type T in question is abstract. > > Consider a statically bound call to the following procedure: > > package Pkg is > type T is abstract tagged null record; > function Is_Ok (X : T) return Boolean is abstract; > procedure Proc (X : T) with Pre'Class => Is_Ok (X); > end Pkg; > > The point is that Proc is not abstract but Is_Ok is. > > If we are not careful, we end up trying to execute the "body" > of an abstract function. > > One approach to this problem is to view it as an unimportant > corner case so that behavior in this situation only needs to be > well-defined (as opposed to being useful). What other approach would there be? A direct call to Is_OK in the body of Proc would be illegal: procedure Proc (X : T) is begin if Is_OK(T) then -- Illegal! Since a precondition is just making these preamble checks visible, such a precondition makes no sense from the get-go. > Taking this approach, we can just state that the proposed > dynamic semantics change doesn't apply if the tagged type T > in question is abstract; program behavior in this case is > then unaffected by the changes of this AI. "Just"? That seems like a massive pain in the neck to implement (having two different sets of code generation depending on whether the original type is abstract). It doesn't seem to work, either: package Pkg2 is type T is tagged null record; function Is_Ok (X : T) return Boolean; procedure Proc (X : T) with Pre'Class => Is_Ok (X); end Pkg2; with Pkg2; package Child2 is type NT is abstract new Pkg2.T with null record; function Is_Ok (X : NT) return Boolean is abstract; end Child2; It would be OK to make a statically bound call to Proc for type NT, but we still would be calling an abstract subprogram. > A cleaner (but messier at the level of RM wording) approach would be > to make such a statically bound call illegal. With the proposed new > dynamic semantics, such a call would be equivalent to an illegal > construct (i.e., to a non-dispatching call to an abstract > subprogram), so by this reasoning it should be illegal. > > Unfortunately, it would be possible to construct violations > of this rule which occur in expanded instance bodies (which are > not subject to legality checking) so we would also need a > special dynamic semantics rule (presumably Program_Error would > be raised) to handle this corner case of a corner case. > This comes down to a question of whether capturing this approach > in the RM is worth all the verbiage that would be required. My initial thought is that the precondition itself should be illegal, because a pure-within-the-body evaluation approach would call an abstract routine with a statically bound call -- which is always illegal. Specifically, a call to an abstract subprogram should not be allowed in Pre'Class or Post'Class IF the contract is on a nonabstract routine. (Unfortunately, "concrete" is not a technical term.) We don't need to look through calls for such a check, because the special tag rules only apply to the top-level of calls (the direct calls mentioned in the precondition/postcondition), so the only problems could be there. (Other places are already handled by the existing Ada rules.) I don't think that this could be a problem within a generic, as everything that can be abstract has to be declared as such in a generic, and then we have assume-the-worst in the body (the actual might not be abstract, but so what). [Besides, tagged extensions are illegal in a body anyway, so the problem could only happen in a specification, and we recheck there.] That's complicated by my Pkg2 example above; we could say that this check is repeated each time a subprogram is declared or inherited (and Pre'Class/Post'Class is involved). That would make the inherited Proc illegal. Not the most fun, but better than a dynamic rule for such a silly case. > Opinions? See above. Note that my suggestion for a legality rule is in-line with Bob's opinion that such things should be prevented at compile-time. If that doesn't fly, then I lean toward Tucker's "always raise Program_Error if one calls an abstract body" -- that's what we did for equality after all. A mixed version is just more work for something that only should happen in the warped mind of Steve Baird :-) [or by accident, of course]. Now it's your turn -- what's wrong with my suggested legality check this?? *************************************************************** From: Steve Baird Sent: Wednesday, July 23, 2014 1:16 PM > Specifically, a call to an abstract subprogram should not be allowed > in Pre'Class or Post'Class IF the contract is on a nonabstract routine. > (Unfortunately, "concrete" is not a technical term.) The objection I see to this approach is that it can impact a user who has no problematic statically bound calls. Language changes (either legality rules or dynamic semantics changes) which pertain only to such statically bound calls have no effect on such a user. This might be viewed as a problem even if we were defining the language from scratch, and it is certainly is a larger incompatibility than the statically-bound-call-based approaches. How much weight should be given to this objection? If the answer to this question is "not much", then I agree that the general approach of trying to deal with this issue via legality rules enforced at the point of the declaration of the Pre/Post'Class-bearing subprogram (perhaps including, as you point out, inherited subprograms) seems worth considering, >> Taking this approach, we can just state that the proposed >> dynamic semantics change doesn't apply if the tagged type T >> in question is abstract; program behavior in this case is >> then unaffected by the changes of this AI. > > It doesn't seem to work, either: > > package Pkg2 is > type T is tagged null record; > function Is_Ok (X : T) return Boolean; > procedure Proc (X : T) with Pre'Class => Is_Ok (X); > end Pkg2; > > with Pkg2; > package Child2 is > type NT is abstract new Pkg2.T with null record; > function Is_Ok (X : NT) return Boolean is abstract; > end Child2; > > It would be OK to make a statically bound call to Proc for type NT, > but we still would be calling an abstract subprogram. A minor detail, but I disagree. I think the approach I outlined handles (in the sense that behavior is well-defined, although not necessarily useful) this case just fine. If we are making a statically bound call to Proc for type NT, then we would be making a statically bound call to a primitive of an abstract type and therefore we would revert to existing RM-defined behavior (which is well-defined, although perhaps not useful). Going off on a little bit of a tangent here, consider the case where we modify Child2 in the above example by making NT and Is_OK both non-abstract. Just to keep things simple, let's assume that nobody extends NT (so that any object whose nominal type is NT has a matching underlying tag). Now any call (statically or dynamically bound) to Child2.Proc will execute Pkg2's Proc but Child2's Is_Ok. This is true for the current RM wording and for any of the proposals we have been considering. Do we care about this mismatch? *************************************************************** From: Randy Brukardt Sent: Wednesday, July 23, 2014 2:05 PM > > Specifically, a call to an abstract subprogram should not be allowed > > in Pre'Class or Post'Class IF the contract is on a nonabstract routine. > > (Unfortunately, "concrete" is not a technical term.) > > The objection I see to this approach is that it can impact a user who > has no problematic statically bound calls. Language changes (either > legality rules or dynamic semantics changes) which pertain only to > such statically bound calls have no effect on such a user. A user without statically bound calls is highly unusual. Moreover, it's bizarre to write a precondition that can't be evaluated for some of the subprograms to which it applies. That seems like a bug to me, not a feature. And of course, the user can always make the call into an explicitly dispatching one, in which case the error goes away. > This might be viewed as a problem even if we were defining the > language from scratch, and it is certainly is a larger incompatibility > than the statically-bound-call-based approaches. > > How much weight should be given to this objection? Roughly that of a feather of a hummingbird. :-) > If the answer to this question is "not much", then I agree that the > general approach of trying to deal with this issue via legality rules > enforced at the point of the declaration of the Pre/Post'Class-bearing > subprogram (perhaps including, as you point out, inherited > subprograms) seems worth considering, OK. > >> Taking this approach, we can just state that the proposed > >> dynamic semantics change doesn't apply if the tagged type T > >> in question is abstract; program behavior in this case is > >> then unaffected by the changes of this AI. > > > > It doesn't seem to work, either: > > > > package Pkg2 is > > type T is tagged null record; > > function Is_Ok (X : T) return Boolean; > > procedure Proc (X : T) with Pre'Class => Is_Ok (X); > > end Pkg2; > > > > with Pkg2; > > package Child2 is > > type NT is abstract new Pkg2.T with null record; > > function Is_Ok (X : NT) return Boolean is abstract; > > end Child2; > > > > It would be OK to make a statically bound call to Proc for type NT, > > but we still would be calling an abstract subprogram. > > A minor detail, but I disagree. I think the approach I outlined > handles (in the sense that behavior is well-defined, although not > necessarily useful) this case just fine. > If we are making a statically bound call to Proc for type NT, then we > would be making a statically bound call to a primitive of an abstract > type and therefore we would revert to existing RM-defined behavior > (which is well-defined, although perhaps not useful). The basic approach you are advocating is that the dynamic semantics are completely different if somehow an abstract subprogram gets involved. While this "works" in the sense that the behavior is defined in all cases, it's completely insane. For one thing, it makes a maintenance hazard (if someone adds "abstract" in the wrong place, the results silently change, not even an exception is raised). Second, it adds distributed overhead to all class-wide preconditions if they are evaluated out-of-line (in a thunk or within the subprogram - a reasonable implementation, IMHO). In such a case, one would pass the appropriate tag and dispatch appropriately (either the statically determined tag or the dynamically determined one, depending on which is right). Reverting to redispatching would require some additional mechanism associated with every tag lookup to deal with the abstract case. This would be a distributed overhead. Note that Janus/Ada does this for all calls to subprograms of formal types in a generic unit (it's how generic code sharing works for tagged types). Also note that anyone can write the behavior you are asking for explicitly, by type converting to a class-wide type (making the call explicitly dispatching). I think it is better to have it explicitly in the code rather than implicit in some way. > Going off on a little bit of a tangent here, consider the case where > we modify Child2 in the above example by making NT and Is_OK both > non-abstract. Just to keep things simple, let's assume that nobody > extends NT (so that any object whose nominal type is NT has a matching > underlying tag). > Now any call (statically or dynamically bound) to Child2.Proc will > execute Pkg2's Proc but Child2's Is_Ok. > This is true for the current RM wording and for any of the proposals > we have been considering. > Do we care about this mismatch? Interesting. One could argue that we do, as it violates what I consider the overriding principle here: that Pre'Class is behaves the same as the same expression written as Pre on each subprogram, with some additional guarantees. That argues that all subprograms with Pre'Class should require overriding. (Moreover, similar cases of "counterfeiting" of Pre'Class by interfaces require overriding). (We could try to formally define what cases cause problems, but it seems like a slippery slope to me, plus a wording nightmare because the obvious description isn't one allowed by the actual language wording.) The issue being that we don't want to allow any case where a body could be successfully called when precondition checking is on yet the precondition that the body knows about is False. OTOH, we've pretty much decided to allow various "mistakes" caused by inheritance. That would be OK for postconditions, but not so much for preconditions. (At least if we are following the current thinking.) Somehow, I get the feeling that you don't want to fix these, just leaving them completely useless for their intended purpose (allowing analysis, including static analysis, of all calls to primitive operations of tagged types, no matter what kind of call it turns out to be, and of course on both sides of the call). Do we just forget that they ever existed? Or do we just admit that we didn't understand these well enough initially and they need correction? (That's been true of almost every kind of contract, we've changed predicates and invariants incompatibly, why is this case different?) *************************************************************** From: Tucker Taft Sent: Wednesday, July 23, 2014 2:31 PM >> Specifically, a call to an abstract subprogram should not be allowed >> in Pre'Class or Post'Class IF the contract is on a nonabstract routine. >> (Unfortunately, "concrete" is not a technical term.) > > The objection I see to this approach is that it can impact a user who > has no problematic statically bound calls. Language changes (either > legality rules or dynamic semantics changes) which pertain only to > such statically bound calls have no effect on such a user. It seems weird to write a "default" implementation for a subprogram, but no default for its precondition. I don't see this as having "no effect" on code with only dynamically-bound calls, because if you decide to inherit this subprogram and don't particularly want to figure out the details of its implementation, but just want to reuse it because it basically does the right thing, why do you have to puzzle out what precondition to apply to it? I remain firmly in the camp of requiring a match of tags used for body and precondition, and catching this at compile time (by disallowing an abstract precondition on a non-abstract subprogram) seems to be the better solution. *************************************************************** From: Tucker Taft Sent: Wednesday, July 23, 2014 5:22 PM >> ... package Pkg2 is >> type T is tagged null record; >> function Is_Ok (X : T) return Boolean; >> procedure Proc (X : T) with Pre'Class => Is_Ok (X); >> end Pkg2; >> >> with Pkg2; >> package Child2 is >> type NT is abstract new Pkg2.T with null record; >> function Is_Ok (X : NT) return Boolean is abstract; >> end Child2; >> >> It would be OK to make a statically bound call to Proc for type NT, >> but we still would be calling an abstract subprogram. > > ... > Going off on a little bit of a tangent here, consider the case where > we modify Child2 in the above example by making NT and Is_OK both > non-abstract. Just to keep things simple, let's assume that nobody > extends NT (so that any object whose nominal type is NT has a matching > underlying tag). > Now any call (statically or dynamically bound) to Child2.Proc will > execute Pkg2's Proc but Child2's Is_Ok. > This is true for the current RM wording and for any of the proposals > we have been considering. > Do we care about this mismatch? No, because the user is explicitly choosing to reuse the code for Proc with a (necessarily weaker) precondition. They must know something about the inner details of Proc such that they believe it can work even with this weaker precondition, and they presumably need this weaker precondition to make Proc useful for their purposes. So this really isn't a mismatch, it is an intentional choice by the definer of NT based presumably on detailed knowledge of T's implementation of Proc. *************************************************************** From: Steve Baird Sent: Wednesday, July 23, 2014 5:37 PM Randy Brukardt wrote: >A user without statically bound calls is highly unusual. In the case of an abstract type which happens to provide a non-abstract "default" implementation for some operation, I'd certainly claim that it isn't a weird corner case. Calls to a primitive operation of an abstract type will often be dispatching calls, even if the callee statically named in the call happens to be a non-abstract subprogram. You're right that an overriding operation often makes a statically bound call to the parent's operation, but the case where this isn't done is hardly a pathology. Tucker Taft wrote: > It seems weird to write a "default" implementation for a subprogram, > but no default for its precondition. Suppose you have package Pkg is type T is abstract tagged record ... end record; function Is_Ok_For_Op1 (X : T) return Boolean is abstract; procedure Op1 (X : T) is abstract with Pre'Class => Is_Ok_For_Op1 (X); procedure Op2 (Xx, Yy: T) with Pre'Class => Is_Ok_For_Op1 (Xx) and Is_Ok_For_Op1 (Yy); -- Op2 is not abstract; a "default" implementation is provided end; because the implementation of Op2 involves (dispatching) calls to Op1. This seems like a reasonable scenario to me (including the use of Pre'Class instead of Pre). My impression is that both Tuck and Randy would prefer to reject this example; please correct me if I am mistaken about either of your positions. I think the author of code like the above example might be surprised to learn that their code is no longer legal because the language has been "improved". Note that the "stick with the existing dynamic semantics in the case of a problematic statically-bound call" rule also works well with this example if somebody does make a statically bound call to Op2. *************************************************************** From: Randy Brukardt Sent: Wednesday, July 23, 2014 6:21 PM > > It seems weird to write a "default" implementation for a subprogram, > > but no default for its precondition. > > Suppose you have > > package Pkg is > type T is abstract tagged record ... end record; > function Is_Ok_For_Op1 (X : T) return Boolean is abstract; > procedure Op1 (X : T) is abstract with > Pre'Class => Is_Ok_For_Op1 (X); > procedure Op2 (Xx, Yy: T) with Pre'Class => > Is_Ok_For_Op1 (Xx) and Is_Ok_For_Op1 (Yy); > -- Op2 is not abstract; a "default" implementation is provided > end; > > because the implementation of Op2 involves (dispatching) calls to Op1. > > This seems like a reasonable scenario to me (including the use of > Pre'Class instead of Pre). > My impression is that both Tuck and Randy would prefer to reject this > example; please correct me if I am mistaken about either of your > positions. No, you've convinced me with this example that we can't have a Legality Rule. (This example looks suspiciously like the root types of Claw, and I certainly would like the option of having Pre'Class.) > I think the author of code like the above example might be surprised > to learn that their code is no longer legal because the language has > been "improved". > > Note that the "stick with the existing dynamic semantics in the case > of a problematic statically-bound call" rule also works well with this > example if somebody does make a statically bound call to Op2. Please forget this and think of something that is actually both implementable and sensible to users. This is neither. I'm not going to waste more time on this if you don't become reasonable. One last data point: We want the same rule to apply to both Pre'Class and Post'Class (and probably Type_Invariant'Class as well). But the latter two are going to be implemented as part of the body of the subprogram (that's where they can be optimized away, not at the call site). Consider a modification of your example above: package Pkg2 is type T is abstract tagged record ... end record; function Is_Mumble (X : T) return Boolean is abstract; procedure OpM (Xx : in out T) with Post'Class => Is_Mumble (Xx); -- OpM is not abstract; a "default" implementation is provided. end; package Pkg2.Child is type NT is new T with null record; function Is_Mumble (X : NT) return Boolean; -- Inherits the default OpM. end Pkg2.Child; You are requiring that Post'Class does different things in the bodies for OpM(T) and OpM(NT). That's going to be pretty hard to implement considering that they're the *same* body. You'd have to use a wrapper for every version of OpM, because you couldn't tell if there ever was going to be an extension with a different rule than the one you generated initially. That would be a form of distributed overhead because it would occur on every subprogram that has Post'Class. ---- The only reasonable solution I see at the moment is to raise Program_Error in the unlikely event that an abstract routine is called by Pre'Class or Post'Class. This isn't as ideal as a Legality Rule, but it's consistent with what we did for abstract untagged equality (4.5.2(24.1/3)) so it's not like it hasn't occurred before. (And this case seems similar to that in some ways.) A statically bound call to OpM(T) or Op2(T) in the examples above seems pretty weird since T is an abstract type -- in most cases, you can't even get an object of type T. *************************************************************** From: Tucker Taft Sent: Wednesday, July 23, 2014 9:44 PM > No, you've convinced me with this example that we can't have a > Legality Rule. ... I am not convinced. In a case like this which involves re-dispatching, what you really should write is: with Pre'Class => Is_Ok_For_Op1(T'Class(Xx)) and Is_Ok_For_Op1(T'Class(Yy)) because internally you are converting Xx and Yy to the class-wide type before invoking Op1. That should be revealed in the precondition. If you are expecting anything more about Xx or Yy before converting them to the class-wide type then that might require additional clauses in the Pre'Class without such a conversion. But for re-dispatching uses of Xx and Yy, the redispatching should be apparent in the Pre'Class as well. The legality rule we have suggested would be just what we want to inform the user that what they wrote in the Pre'Class didn't make sense, and didn't properly account for the semantics of re-dispatching. *************************************************************** From: Randy Brukardt Sent: Wednesday, July 23, 2014 10:25 PM > The legality rule we have suggested would be just what we want to > inform the user that what they wrote in the Pre'Class didn't make > sense, and didn't properly account for the semantics of > re-dispatching. You've kinda reconvinced me. Another factor that's reconvinced me is that you never, ever want (implicit) dispatching in a precondition or postcondition. We want to be able to implement these (especially postconditions) inside the body of the subprogram. For that to work sensibly, there shouldn't be any implicit dispatching. Even in the case of a dispatching call, one can think of what's going on as the tag being determined at the call site, and then dispatching to an appropriate (statically bound) precondition before dispatching to the actual body. After all, that's exactly what happens for Pre, and we want Pre'Class to operate as similarly as possible. But if an abstract routine is involved in a contract, it can only be legal if dispatching is involved. Everywhere else in Ada, we require users to make the dispatching explicit somehow -- that should be true in a contract as well. If it is true, then there is no reason to allow a call on an abstract routine in a Pre'Class (we certainly would not allow such a call in a Pre). A third factor that I've thought of since is that while Claw has a structure somewhat like Steve's example, one important difference exists. And that is the most of the routines with default implementations are query functions like Is_Valid (the validity flag being in the default portion of the record) -- it's the implementations of the operations that are abstract. Steve's example *could* happen, but it's not what occurs in my experience. (Especially as Op2 would normally be a class-wide routine in Claw; a routine that depends on other implementations generally does not allow overriding -- something we did to keep the size of the interface [the primitive routines and their containing package] managable. But a class-wide routine has to use Pre, not Pre'Class.) *************************************************************** From: Steve Baird Sent: Wednesday, July 23, 2014 11:39 PM > I am not convinced. In a case like this which involves > re-dispatching, what you really should write is: > > with Pre'Class => Is_Ok_For_Op1(T'Class(Xx)) and > Is_Ok_For_Op1(T'Class(Yy)) This brings up a topic which crossed my mind last night. The rule we have been considering (and we don't have real wording for this yet) says If a controlling formal parameter of Foo is used as a controlling operand of a call within the Pre'Class expression or the Post'Class expression, ... What does this mean if the controlling operand in question is something like a parenthesized expression or a type conversion which has the same associated object as a controlling formal parameter of Foo? Presumably we don't want slapping a pair of parens around a parameter to change the controlling tag of some call. What about a conditional expression where one of the dependent expressions has the same associated object? More relevant to today's question, what about a qualified expression? If we do make this change, I think it is important that we provide some way for users to get back to the old behavior in the (presumably less common) case where that's what is wanted. This could be accomplished by saying that the new dynamic semantics rule does not apply at least in the case of a redundant qualified expression (i.e., one where the type of the expression is the same class-wide type as that of the operand). We might need to do something similar with type conversions in order to handle cases where a variable view is needed. If we have something along these lines to provide a workaround when previously-legal code becomes illegal, then I think that would resolve my objections to the new legality rule we have been discussing. On the other hand, giving significant dynamic semantics to what would normally be a redundant qualified expression or type conversion (e.g., the qualified expressions in your example above) detracts from readability (and is simply ugly). We may want to just hold our noses and accept this because we don't have a better alternative. *************************************************************** From: Tucker Taft Sent: Thursday, July 24, 2014 1:08 PM >> I am not convinced. In a case like this which involves >> re-dispatching, what you really should write is: >> >> with Pre'Class => Is_Ok_For_Op1(T'Class(Xx)) and >> Is_Ok_For_Op1(T'Class(Yy)) > ... > If we do make this change, I think it is important that we provide > some way for users to get back to the old behavior in the (presumably > less common) case where that's what is wanted.... I believe that is exactly what is done above, namely, forcing the calls on Is_Ok_For_Op1 to do a dispatching call even when the caller of the associated subprogram is using static binding. (Or am I missing an subtle difference?) As I mentioned, this only does dispatching for the particular calls on Is_Ok_For_Op1. If there were other clauses in the precondition that used Xx or Yy without such a conversion-to-classwide, they would use static binding if static binding was used in the call on the associated subprogram. *************************************************************** From: Steve Baird Sent: Thursday, July 24, 2014 1:32 PM > (Or am I missing an subtle difference?) As I suggested in my previous message, what is missing are the precise rules for when the proposed "use the statically bound tag instead of the underlying dynamic tag" change kicks in. You seem to be assuming that the change applies in the case of X but not in the case of T'Class'(X) . That sounds like a good start to me. I think we are on track towards something we can agree on. *************************************************************** From: Tucker Taft Sent: Thursday, July 24, 2014 2:05 PM > You seem to be assuming that the change applies in the case of > X > but not in the case of > T'Class'(X) I wrote "T'Class(X)" -- i.e. a conversion, not a qualified_expression. > That sounds like a good start to me. I think we are on track towards > something we can agree on. No, I was presuming it applied to a *conversion*, not a qualified expression. A qualified expression shouldn't change the dynamic semantics, other than perhaps to insert a check. *************************************************************** From: Steve Baird Sent: Thursday, July 24, 2014 2:33 PM > I wrote "T'Class(X)" -- i.e. a conversion, not a qualified_expression. So what's a few pixels among friends? Ok, good point. Anyhow, my two main points remain: 1) I think we are on the right track here. 2) For each of the various cases where an actual parameter expression can have the same associated object as X (listed in 6.2(10/3)), we need to decide whether the new "use the statically bound tag" dynamic semantics rule applies. > A qualified expression shouldn't change the dynamic semantics, other > than perhaps to insert a check. That sounds good to me. Similarly, adding parens shouldn't change anything in this area. So does the change never apply in the case of any type conversion? That's a nice simple rule. The decision could depend on some properties of the target type of the conversion (e.g., class-wide vs. specific, ancestor/descendant/both/neither, abstract/concrete(, but I don't see any obvious reason to do anything like that. That leaves conditional expressions, something like with Pre'Class => Is_Ok ((if Blah then X else Something_Else)); I'd say keep things simple and say the new rule does not apply in this case. This breaks the dynamic equivalence between (X) and (if True then X else Something_Else) but I could live with that. *************************************************************** From: Tucker Taft Sent: Thursday, July 24, 2014 4:13 PM > That leaves conditional expressions, something like > > with Pre'Class => Is_Ok ((if Blah then X else Something_Else)); > > I'd say keep things simple and say the new rule does not apply in this > case. This breaks the dynamic equivalence between > (X) > and > (if True then X else Something_Else) but I could live with that. This seems bizarre to me. I would rather not talk about two different sets of rules. There should only be one rule, I would hope. The rule currently in the RM is broken, and we should come up with a new rule. The new rule should ensure that when inside the body of an operation that is *not* inherited and has a Pre'Class aspect, we know which precondition expressions were conceptually "or"ed together to make up the effective precondition, and we know which Post'Class expressions are going to be "anded" when we are done. If a body is inherited, while something used in the Pre'Class or Post'Class is overridden, we may need to recompile/reanalyze the body if any assumptions were made when compiling/analyzing it about what Pre'Class applied, and what Post'Class expressions needed to be proved. Let's assume we treat a non-inherited Pre'Class as roughly equivalent to a Pre when making a statically bound call, i.e. nothing special happens in terms of dispatching, etc. The next question is what happens to a Pre'Class when it is inherited? My initial cut would be to systematically replace each use of a formal parameter with the corresponding formal parameter of the subprogram in the descendant type, and similarly replace each statically-bound call on a primitive operation with a statically-bound call on the corresponding primitive in the descendant type. It is not clear that this would be easy to define formally, but I think this represents the "goal" semantics from my perspective. *************************************************************** From: Steve Baird Sent: Friday, July 25, 2014 2:41 PM Steve Baird wrote: > 2) For each of the various cases where an actual parameter expression > can have the same associated object as X (listed in > 6.2(10/3)), we need to decide whether the new > "use the statically bound tag" dynamic semantics rule > applies. Tucker Taft wrote: > This seems bizarre to me. I would rather not talk about two different > sets of rules. There should only be one rule, I would hope. I'm confused, I thought you were advocating treating with Pre'Class => Is_Ok (X) differently than with Pre'Class => Is_Ok (T'Class (X)) with respect to the "use the tag of the statically bound call" dynamic semantics rule. Is that what you mean by "two different sets of rules". If so, then I thought you were in favor of this. If not, then please elaborate. If we do introduce that distinction then we also have to decide which way to treat things like qualified expressions, parenthesized expressions, and conditional expressions. I don't anticipate that any of these would be controversial based on the discussion so far (in particular, I don't have strong feelings one way or the other about conditional expressions). The proposal I thought we were close to converging on is 1) The dynamic semantics change. 2) A legality check that change #1 does not cause us, in effect, to invoke the body of an abstract subprogram. 3) P_E is raised somewhere if #2 is violated in an expanded instance. You raise the question of statically bound calls to inherited subprograms. Could this be addressed by changing the originally proposed dynamic semantics change > The dynamic semantics of Pre'Class/Post'Class evaluation for a > primitive operation of a tagged type T in the case of a > non-dispatching (i.e., statically bound) call to Foo could be changed as > follows: > > If a controlling formal parameter of Foo is used as a > controlling operand of a call within the Pre'Class expression > or the Post'Class expression, then for purposes of determining > the controlling tag of that call the (dynamic) tag of the > parameter is considered to be T'Tag. so that instead using T'Tag we use the Tag of the ancestor of T for which the corresponding non-inherited subprogram is a primitive subprogram? [There might be some ugly corner cases involving interface types and null procedures]. *************************************************************** From: Randy Brukardt Sent: Friday, July 25, 2014 5:38 PM > Steve Baird wrote: > > 2) For each of the various cases where an actual parameter expression > > can have the same associated object as X (listed in > > 6.2(10/3)), we need to decide whether the new > > "use the statically bound tag" dynamic semantics rule > > applies. > > Tucker Taft wrote: > > This seems bizarre to me. I would rather not talk about two > > different sets of rules. There should only be one rule, I would hope. > > I'm confused, Yes, clearly. :-) > I thought you were advocating treating > with Pre'Class => Is_Ok (X) > differently than > with Pre'Class => Is_Ok (T'Class (X)) with respect to the "use the > tag of the statically bound call" > dynamic semantics rule. Is that what you mean by "two different sets > of rules". If so, then I thought you were in favor of this. If not, > then please elaborate. You're looking at this in completely the wrong way. If Pre'Class is given on a primitive of tagged type T: (1) For the purposes of resolution ONLY, X in the above is treated as a class-wide type (T'Class). This is done ONLY so that inherited Pre'Class expressions work (we don't want calls that would be illegal for some descendant of T, and we want dispatching to work.). [I'm not 100% certain that this step is even needed.] (2) For a call, Pre'Class is to be evaluated at the call site, based on the declaration that the call is resolved to. In this case, the type X is treated to be whatever type the dispatching type is resolved to be. That means Pre'Class might be evaluated using dispatching (for a dispatching call) or statically bound. (3) For all other purposes (these mainly are Post'Class and probably Type_Invariant'Class), X is treated to be of the specific type associated with the subprogram for whose declaration the Pre'Class is associated. That's some descendant of T (or T itself). This means any associated calls are always statically bound. (This is exactly how it would work if one used Post rather than Post'Class, manually adding a new Post for each overridden subprogram.) Note that for (2) and (3), it is only the type of X that changes. If you wrap X in a type conversion, then that type becomes irrelavant, just as it would if you wrote if Is_OK (T'Class (X)) then (2) and (3) have to be different because the way Pre'Class works is different than Post'Class. In particular, a call only evaluateds the Pre'Class it knows about -- this allows the precondition of a dispatching call to be known at the call-site. But to evaluate that at the call-site means it must be dispatching. Note that such a dispatching call is always equivalent to a statically bound call in the absence of an inherited body. For an inherited body, different versions of the functions that make up Pre'Class might be called [if they themselves are overridden] than those that would have been evaluated by the body. That would allow counterfeiting for an inherited body. Arguably, no inheritance should be allowed for subprograms with Pre'Class unless the functions that make up Pre'Class are themselves all inherited. But that's too strong (and complicated) of a restriction; counterfeiting can only happen when some routine that makes up the class-wide precondition is weakened. While that fits with LSP, useful weakening is rather rare. So I think that particular problem can be left behind. If any of the expressions evaluated by (2) or (3) are statically bound to an abstract subprogram, then of course the expression is illegal. We probably do need a rule to say this. If there is any case where that could occur in a generic body and the abstractness is, then we would need a Program_Error rule. However, I got the feeling Tucker wanted to stick with the rule I proposed earlier, which is that Pre'Class/Post'Class is illegal if it is used on a concrete routine such that any of the constituents is abstract. That never causes a generic problem (extensions are not allowed in bodies), and it only would provide a false positive for a Pre'Class for which every call in existence is dispatching. (It would NEVER be a false positive for Post'Class, since those are always statically bound, unless of course the body in question is never called anywhere [even after being inherited].) > If we do introduce that distinction then we also have to decide which > way to treat things like qualified expressions, parenthesized > expressions, and conditional expressions. I don't anticipate that any > of these would be controversial based on the discussion so far (in > particular, I don't have strong feelings one way or the other about > conditional expressions). There's no "distinction" here. This is just a normal expression with objects of a statically known tagged type. I realize this is somewhat of a different way to look at this than you were doing. But what you were doing was clearly leading nowhere (worring about the semantics of a parenthesized expression is my idea of "nowhere"!) *************************************************************** From: Tucker Taft Sent: Friday, July 25, 2014 7:05 PM > I'm confused, I thought you were advocating treating > with Pre'Class => Is_Ok (X) > differently than > with Pre'Class => Is_Ok (T'Class (X)) with respect to the "use the > tag of the statically bound call" > dynamic semantics rule. Is that what you mean by "two different sets > of rules". If so, then I thought you were in favor of this. If not, > then please elaborate. I don't see these as different rules, merely different consequences of a single rule, which is largely based on a static binding view unless the pre'class explicitly includes a conversion to class wide. In that case, the normal consequences arise and dispatching always occurs. I'll try to propose some wording at some point real soon now... *************************************************************** From: Steve Baird Sent: Friday, July 25, 2014 7:13 PM Sounds good. I think we are close. *************************************************************** From: Tucker Taft Sent: Sunday, August 2, 2014 3:46 PM I am on the hook to produce some new wording related to Pre'Class. Here is the current wording: Paragraph 6.1.1(7/3): (In Name Resolution) Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram of a tagged type T, a name that denotes a formal parameter of type T is interpreted as having type T'Class. Similarly, a name that denotes a formal access parameter of type access-to-T is interpreted as having type access-to-T'Class. [Redundant: This ensures that the expression is well-defined for a primitive subprogram of a type descended from T.] Paragraph 6.1.1(18/3): (In Static Semantics) If a Pre'Class or Post'Class aspect is specified for a primitive subprogram of a tagged type T, then the associated expression also applies to the corresponding primitive subprogram of each descendant of T. Paragaraph 6.1.1(33/3): (In Dynamic Semantics) The class-wide precondition check begins with the evaluation of any enabled class-wide precondition expressions that apply to the subprogram or entry. If and only if all the class-wide precondition expressions evaluate to False, Assertions.Assertion_Error is raised. Paragraph 6.1.1(38/3): (In Dynamic Semantics) The class-wide precondition check for a call to a subprogram or entry consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily the one that is invoked). --------- Here is an attempt at a re-write: Let's start by eliminating 6.1.1(7/3) and see if we can do all the magic in (18/3): (In Static Semantics) Revise (18/3) as follows: 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} [the associated expression] also applies to the corresponding primitive subprogram {S} of each descendant of T. {The *corresponding expression* is constructed from the associated expression as follows: * References to formal parameters or the result of S are replaced with references to the corresponding formal parameters or result of the inherited or overriding subprogram S; * Non-dispatching calls to primitive subprograms of T are replaced with non-dispatching calls to the corresponding primitive subprograms of the descendant of T, if the controlling tag of the call is determined by references to controlling parameters or results of the primitive subprogram S.} --- We need to add a legality rule somewhere: {A Pre'Class or Post'Class aspect for a primitive subprogram S of a tagged type T is illegal if it contains a non-dispatching call on a primitive subprogram of T, if the controlling tag of the call is determined by references to controlling parameters or results of the primitive subprogram S, as well to other operands that are not tag indeterminate and are not references to controlling parameters or results of S.} Revise (38/3) as follows: (In Dynamic Semantics) The class-wide precondition check for a call to a subprogram or entry {S} consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily the one that is invoked). {If the call is a dispatching call to S, then any non-dispatching calls within a Pre'Class expression associated with S, whose controlling tag is determined by references to controlling parameters or results of the subprogram S, become dispatching calls when the class-wide precondition is evaluated.} ---------- Fire away! *************************************************************** From: Tucker Taft Sent: Friday, August 8, 2014 6:55 PM I have had no feedback on this proposal. It is of high priority to the folks building SPARK 2014, so if this approach does or does not seem reasonable, please comment! *************************************************************** From: Randy Brukardt Sent: Friday, August 8, 2014 10:12 PM > I have had no feedback on this proposal. Jeez, it's summer. Some of us are trying to avoid unnecessary pain. ;-) > It is of high > priority to the folks building SPARK 2014, so if this approach does or > does not seem reasonable, please comment! Sigh. OK. (I'm on the hook with you for this AI anyway, as the original author, so I suppose...) > Here is an attempt at a re-write: > > Let's start by eliminating 6.1.1(7/3) and see if we can do all the > magic in (18/3): So "Delete 6.1.1(7/3)" is the first instruction in the AI. And you are not making any change to 6.1.1(33/3) [the AI doesn't need to mention it]. > (In Static Semantics) > > Revise (18/3) as follows: > > 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} [the associated expression] > also applies to the corresponding primitive subprogram {S} of each > descendant of T. {The *corresponding expression* is constructed > from the associated expression as follows: > > * References to formal parameters or the result of S are > replaced with references to the corresponding formal parameters or > result of the inherited or overriding subprogram S; > * Non-dispatching calls to primitive subprograms of T are > replaced with non-dispatching calls to the corresponding primitive > subprograms of the descendant of T, if the controlling tag of the > call is determined by references to controlling parameters or > results of the primitive subprogram S.} Humm. I'm not sure the second bullet is really needed. With 6.1.1(7/3) gone, the normal resolution rules apply. Or do you mean for the "corresponding expression" not to be resolved at all? Maybe I'm think of a different model than you are. I was thinking that the Pre'Class expression is duplicated for each subprogram, with the specified substitutions, with all of the other steps occurring afterwards. (That's how default expressions work, right?) In that case, the binding to subprograms takes place during the resolution. It seems necessary to re-resolve the expression because of the possible presence of non-primitive subprograms and the like (which won't resolve for descendants). Perhaps you are trying to resolve the expression only once. I'd guess that would be better in the sense that it ensures that the expression doesn't change because of visibility for the descendants, but it surely complicates the model. --- Less important: terminology. "Non-dispatching calls of primitive subprograms of T" is a mouthful. I guess it's formally correct (since 3.9.2(1/2) does define "dispatching call", but I think it would be better to follow 3.9.2 more closely. 3.9.2 says that all calls on primitive operations of T are "calls on dispatching operations". It then talks about the controlling tag being either statically tagged, dynamically tagged, or tag indeterminate. I think it would be better to talk about "calls on dispatching operations of T whose tag is statically determined" (using the terminology of 3.9.2(15)), because then you don't have to talk about primitive operations at all, avoiding the need to stick in a negative. (This also would mean that other kinds of dispatching calls, specifically to abstract formal subprograms, would be covered, if there is some way for them to get involved in a Pre'Class expression. If there is, we certainly would want them to work the same way as a primitive operation.) --- Since the only way to reference the result of S is via the Result attribute, it might be better to say that than to talk about the "result of S". It really confused me at first. Maybe two bullets would make more sense: * References to formal parameters of S are replaced with references to the corresponding formal parameters of the inherited or overriding subprogram S; * References to S'Result are replaced with references to S'Result of the inherited or overriding subprogram S; > --- > > We need to add a legality rule somewhere: > > {A Pre'Class or Post'Class aspect for a primitive subprogram S of > a tagged type T is illegal if it contains a non-dispatching call on > a primitive subprogram of T, if the controlling tag of the call is > determined by references to controlling parameters or results of the > primitive subprogram S, as well to other operands that are not tag > indeterminate and are not references to controlling parameters or > results of S.} This is your attempt to prevent the non-resolving descendant problem. But it's not enough: what about a call on a non-primitive subprogram having a parameter or result of T? package P1 is type T is ... package Inner is function Is_OK (A : T) return Boolean; end Inner; procedure Foo (A : in T) with Pre'Class => Is_OK(A); end P1; with P1; package P2 is type NT is new P1.T with ... procedure Foo (B : in NT); -- (1) end P2; (1) would have a Pre'Class of "Is_OK (B)"; but that doesn't make any sense because there is no Is_OK for type NT, so this would not resolve. Hopefully this is covered by the rules. > Revise (38/3) as follows: > > (In Dynamic Semantics) > > The class-wide precondition check for a call to a subprogram or > entry {S} consists solely of checking the class-wide precondition > expressions that apply to the denoted callable entity (not > necessarily the one that is invoked). {If the call is a dispatching > call to S, then any non-dispatching calls within a Pre'Class > expression associated with S, whose controlling tag is determined by > references to controlling parameters or results of the subprogram S, > become dispatching calls when the class-wide precondition is > evaluated.} Same here for the terminology: it would be better to say "calls to a dispatching operation within a Pre'Class expression associated with S, whose controlling tag is {statically} determined by references to controlling parameters or results of the subprogram S, become dispatching calls when the class-wide precondition is evaluated." Or something like that. --- I don't see an attempt to address the Baird problem of an abstract routine: package Pkg is type T is abstract tagged null record; function Is_Ok (X : T) return Boolean is abstract; procedure Proc (X : T) with Pre'Class => Is_Ok (X); end Pkg; with Pkg; package Pkg2 is type NT is new Pkg2.T with ... function Is_OK (X : NT) return Boolean; procedure Proc (X : NT); end Pkg2; package body Pkg2 is procedure Proc (X : NT) is begin -- Call parent operation: Proc (T(X)); -- (2) end Proc; ... end Pkg2; The precondition of call (2) is Is_OK (T), which is calling an abstract function. We had discussed making the precondition illegal for this case, or having it raise Program_Error (I prefer the former). But I don't see any rules that cover that. Note that this can happen "after the fact" -- any legality rule has to be rechecked after substitution for every Pre'Class and Post'Class expression. (That is, after every inheritance.) Checking just at the original definition isn't enough. For example: package Pkg3 is type T is tagged null record; function Is_Ok (X : T) return Boolean; procedure Proc (X : T) with Pre'Class => Is_Ok (X); end Pkg3; with Pkg3; package Pkg4 is type NT is abstract new Pkg3.T with ... function Is_OK (X : NT) return Boolean is abstract; procedure Proc (X : NT); end Pkg4; with Pkg4; package Pkg5 is type NNT is new Pkg4.NT with ... function Is_OK (X : NNT) return Boolean; procedure Proc (X : NNT); end Pkg5; package body Pkg5 is procedure Proc (X : NNT) is begin -- Call parent operation: Proc (NT(X)); -- (3) end Proc; ... end Pkg5; (3) has a statically bound precondition that calls an abstract routine. If we were to add a legality rule, it would have to reject Pkg4 as violating it (the contents of Pkg3 are fine, so it can't be purely a rule on the initial Pre'Class expression). We need to solve this here because it's a new problem introduced by the new static binding substitutions (it doesn't exist before, as there cannot be any objects of a abstract type, so you can't dispatch to them). This is one of the reasons I was thinking that the expression would be re-resolved (because that would automatically trigger the normal legality rules against calling an abstract subprogram). But that has other problems (one could make it so the expression didn't have the same effect in a descendant, which would defeat the purpose). *************************************************************** From: Tucker Taft Sent: Saturday, August 9, 2014 2:17 PM ... > Perhaps you are trying to resolve the expression only once. I'd guess > that would be better in the sense that it ensures that the expression > doesn't change because of visibility for the descendants, but it > surely complicates the model. I think re-resolving would open up a big can of worms. After all, this new expression is likely located in a different package, and so re-resolving names would be very much hit or miss. So I was imagining that all the names are resolved once, and now we are talking about substituting *entities*, not *names*. I think it is actually simpler, not more complicated, to do it that way. ... ... > (1) would have a Pre'Class of "Is_OK (B)"; but that doesn't make any sense > because there is no Is_OK for type NT, so this would not resolve. Hopefully > this is covered by the rules. I agree we need a more general legality rule that says the pre'class is illegal if, after making such a substitution, the actual type of an operand in a call would no longer match the corresponding formal type, or an operand used in some other context would no longer be legal. So we don't re-do name resolution, but we recheck the legality rules. This is somewhat similar to what happens in the spec of a generic instance. Perhaps we could create a closer analogy to generic instantiation, where the parameters and result of type T or access T of the original subprogram are treated as though they are of a formal extension type. E.g. function Foo(A : access T) return T with Pre'Class => Is_OK(A.all), Post'Class => Foo'Result > A.all; becomes, notionally: generic type NT is new T with private; function Foo(A : access NT) return NT with Pre'Class => Is_OK(A.all), Post'Class => Foo'Result > A.all; So rather than treating these operands as being of type T'Class, which was the original approach, we instead treat them as being of a type NT that is a formal extension of T, and so "constructing" the corresponding Pre'Class or Post'Class expression becomes essentially a generic instantiation. T > ... I don't see an attempt to address the Baird problem of an abstract routine: > > package Pkg is > type T is abstract tagged null record; > function Is_Ok (X : T) return Boolean is abstract; > procedure Proc (X : T) with Pre'Class => Is_Ok (X); > end Pkg; Perhaps the "formal type extension" model might help here as well. If the subprogram with the Pre'Class or Post'Class aspect is not abstract, then the generic must be legal when the formal extension is instantiated with type T itself. *************************************************************** From: Jeff Cousins Sent: Thursday, August 14, 2014 3:32 AM My pennyworth's. Randy's re-wordings generally seem clearer. The proposed legality rule takes the form: ... is illegal if ... T, if ... S, as well ... S. I would have expected another "and" or "or" somewhere. *************************************************************** From: Tucker Taft Sent: Thursday, August 14, 2014 3:55 PM If we go with the formal type extension model, then I think the legality rules will be significantly simplified. I'll try to propose something concrete using the formal type extension model. I think it is a better fit to the problem than our original T'Class approach, and feels a bit more intuitive (to me, at least!). *************************************************************** From: Randy Brukardt Sent: Thursday, August 21, 2014 8:17 PM In filing this mail, I had some additional thoughts... Tucker Taft writes: > If we go with the formal type extension model, then I think the > legality rules will be significantly simplified. > > I'll try to propose something concrete using the formal type extension > model. I think it is a better fit to the problem than our original > T'Class approach, and feels a bit more intuitive (to me, at least!). Yes, but be careful to deal with non-primitive operations sensibly. You had written: > This is somewhat similar to what happens in the spec of a generic instance. Perhaps we > could create a closer analogy to generic instantiation, where the parameters and result of > type T or access T of the original subprogram are treated as though they are of a formal > extension type. E.g. > > function Foo(A : access T) return T > with Pre'Class => Is_OK(A.all), > Post'Class => Foo'Result > A.all; > >becomes, notionally: > > generic > type NT is new T with private; > function Foo(A : access NT) return NT > with Pre'Class => Is_OK(A.all), > Post'Class => Foo'Result > A.all; I'm presuming that the idea is that this is resolved when the Pre'Class is initially compiled (that corresponds to compiling the generic for a generic unit), and then the substitutions are done for each individual subprogram (that corresponds to the instantiation). This is very clean for operations of T, since non-primitives that happen to take a T are not imported into the notional generic and thus would not (initially) compile (operations that aren't visible clearly won't resolve). But that doesn't seem to work so well for other non-primitives, since they aren't imported into the generic, either. If Is_OK was class-wide: function Is_OK (A : in T'Class) return Boolean; it should be usable in the Pre'Class expression (as it would properly work in any inherited subprogram). Similarly, a global function should work. If we had: function Bar(A : T) return Natural with Pre'Class => Is_OK(A) and Database_is_Ready; [ignore for the moment that it would probably be better to fold "Database_is_Ready" into the Is_OK function, because not every design is "better"; we need to support anything reasonable, not just those that are best.] Your notional generic would be: generic type NT is new T with private; function Bar(A : T) return Natural with Pre'Class => Is_OK(A) and Database_is_Ready; which would not compile unless Database_is_Ready is imported somehow. *************************************************************** From: Tucker Taft Sent: Friday, August 22, 2014 1:15 AM Sent from my iPhone > ... > > Your notional generic would be: > > generic > type NT is new T with private; > function Bar(A : T) return Natural > with Pre'Class => Is_OK(A) and Database_is_Ready; > > which would not compile unless Database_is_Ready is imported somehow. The "notional" generic would be resolved in the same visibility context as the Pre'class aspect specification, augmented with the notional generic formals. So I am not sure globals require any special processing. ***************************************************************