!standard 4.1.3(9/3) 13-07-17 AI12-0032-1/07 !standard 6.1.1(22/3) !standard 6.1.1(26/3) !standard 6.1.1(35/3) !class binding interpretation 13-05-09 !status Corrigendum 2015 13-07-17 !status WG9 Approved 13-11-15 !status ARG Approved 7-0-0 13-06-16 !status work item 12-06-06 !status received 12-05-29 !priority Low !difficulty Medium !subject Questions on 'Old !summary (1) The accessibility level of X'Old is that of the associated implied constant declaration. (2) If X has an anonymous access type, the implied constant associated with X'Old has an anonymous access type with the same designated type or profile. (3) The nominal subtype of X'Old is defined to be that of X. (4) X'Old is legal for an abstract type, as X'Old has the same underlying runtime tag as X (which necessarily cannot be abstract). (5) If X is tagged, X'Old has the same underlying runtime tag as X. (6) X'Old is well defined if X is of a universal type. (7) In the case of an entry or a protected subprogram with a postcondition the events listed below occur in the following order: - any postcondition checks are performed; then - any constants associated with 'Old occurrences are finalized; then - the rendezvous or protected action is ended. !question 1) X'Old denotes a (constant) object. The accessibility level of that object does not seem to be defined by the current wording of the Standard. Should it be? (It's OK as is.) 2) X and X'Old are defined to have the same type, even if that type is anonymous. That's usually good. We want to allow: Table : array (1 .. 3) of Integer; procedure Foo with Post (Table = Table'Old); If, however, X is of an anonymous access type, then things get odd. What does it mean to say that a standalone constant has the same type as, say, an access discriminant? This makes no sense. Even if X itself is a standalone object, having two such objects sharing the same type leads to problems (for example, does the accessibility level of the type of X'Old then depend on the value most recently assigned to X?). Should we define the type of the constant to be an anonymous access with the same designated type? (Yes.) 3) Should the nominal subtype of X'Old be defined? (Yes and it is.) It currently isn't, meaning we fall back to 4.1.4(9/3), which says it is the base subtype of the type. That means that the following is illegal: procedure Old_Test is procedure Foo (X : in out Natural) with Post => X = (case X'Old is when 0 => 0, when Positive => X'Old - 1); procedure Foo (X : in out Natural) is begin if X > 0 then X := X - 1; end if; end; begin null; end; because the case expression doesn't cover all values of the subtype of the case expression. 4) What should happen if X'Old has an abstract type? (X'Old has the same runtime tag as X.) A direct application of the model would imply that it should be illegal, because we'd be declaring a constant of an abstract type. But it seems odd that X'Old should be illegal even if X is legal. 5) If T is a specific tagged type, the runtime tags of X and X'Old may not match, which can affect (among other things) the body executed by a dispatching call. That's because the implicit constant declaration of: X'Old : constant T := X; always has the tag of T, while X may have some other tag because of type conversions. This affects (re)dispatching and equality, among other things. Should this be fixed somehow? (Yes.) 6) What is the meaning of Named_Number'Old? (See summary.) This is something that can't easily be declared (there are no objects of a universal type), and it's useless as a named number has to be constant anyway. 7) An occurrence of X'Old in a postcondition is evaluated before the associated implicitly declared constant is finalized. In the case of an entry or protected subprogram, does this mean that postcondition checking is peformed within the rendezvous or protected action? (Yes.) !recommendation (See summary.) !wording In 4.1.4(9/3), prepend to the second sentence: "Unless explicitly specified otherwise, " and lower-case the "For" that formerly began the sentence. Add after 6.1.1(22/3): * the predicate of a quantified_expression; Replace 6.1.1(26/3) with X'Old Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement. The implicitly declared entity denoted by each occurrence of X'Old is declared as follows: - If X is of an anonymous access defined by an access_definition A then : constant A := X; - If X is of a specific tagged type T then : constant T'Class := T'Class (X); : T renames T (); where the name X'Old denotes the object renaming. AARM Ramification: This means that the underlying tag associated with X'Old is that of X and not that of the nominal type of X. - Otherwise : constant S := X; where S is the nominal subtype of X. Redundant[This includes the case where the type of S is an anonymous array type or a universal type.] The nominal subtype of X'Old is as implied by the above definitions. The expected type of the prefix of an Old attribute is that of the attribute. Similarly, if an Old attribute shall resolve to be of some type, then the prefix of the attribute shall resolve to be of that type. AARM Ramification: An accept statement for a task entry with enabled postconditions such as accept E do exception end; behaves (at runtime) as follows: accept E do declare begin begin exception end; end; end; Preconditions are checked by the caller before the rendezvous begins. Postcondition expressions might, of course, reference 'Old constants. In the case of a protected operation with enabled postconditions, 'Old constant declarations (if any) are elaborated after the start of the protected action. Postcondition checks (which might reference these constants) are performed before the end of the protected action as described below. Append to AARM 6.1.1(27.d(3)): Similarly, the implicit constant declaration defines the accessibility level of X'Old. Add after 6.1.1(35/3): For a call to a task entry, the postcondition check is performed before the end of the rendezvous; for a call to a protected operation, the postcondition check is performed before the end of the protected action of the call. The postcondition check for any call is performed before the finalization of any implicitly-declared constants associated (as described above) with Old attribute_references but after the finalization of any other entities whose accessibility level is that of the execution of the callable construct. AARM Reason: If a postcondition references the implicitly-declared constant associated with an Old attribute, the postcondition must be evaluated before the constant is finalized. One way to think of this is to imagine declaring a controlled object between any implicit "'Old" constant declarations and any explicit declarations, then performing postcondition checks during the finalization of this object. !discussion 'Old constants are declared "at the beginning of the subprogram body, entry body, or accept statement". This means that, in the case of an entry or a protected subprogram, they are declared after the start of the associated rendezvous or protected action. Since such constants can only be usefully referenced before they are finalized, postcondition checks (which need to be able to reference these constants) must be performed before, not after, the end of the rendezvous or protected action. We add quantified_expressions to expressions that are potentially unevaluated, because the compiler cannot know how many times (if at all) the predicate is evaluated. 6.1.1(27/3) makes (for I in 1 .. 10 => A(I)'Old = A(I)) illegal, but we also need (for I in 1 .. F(...) => A(F(N)'Old)) to be illegal. !corrigendum 4.1.4(9/3) @drepl An @fa denotes a value, an object, a subprogram, or some other kind of program entity. For an @fa that denotes a value or an object, if its type is scalar, then its nominal subtype is the base subtype of the type; if its type is tagged, its nominal subtype is the first subtype of the type; otherwise, its nominal subtype is a subtype of the type without any constraint or @fa. Similarly, unless explicitly specified otherwise, for an @fa that denotes a function, when its result type is scalar, its result subtype is the base subtype of the type, when its result type is tagged, the result subtype is the first subtype of the type, and when the result type is some other type, the result subtype is a subtype of the type without any constraint or @fa. @dby An @fa denotes a value, an object, a subprogram, or some other kind of program entity. Unless explicitly specified otherwise, for an @fa that denotes a value or an object, if its type is scalar, then its nominal subtype is the base subtype of the type; if its type is tagged, its nominal subtype is the first subtype of the type; otherwise, its nominal subtype is a subtype of the type without any constraint or @fa. Similarly, unless explicitly specified otherwise, for an @fa that denotes a function, when its result type is scalar, its result subtype is the base subtype of the type, when its result type is tagged, the result subtype is the first subtype of the type, and when the result type is some other type, the result subtype is a subtype of the type without any constraint or @fa. !corrigendum 6.1.1(22/3) @dinsa @xbullet@fa of a @fa;> @dinst @xbullet of a @fa;> !corrigendum 6.1.1(26/3) @drepl @xhang<@xterm For each X'Old in a postcondition expression that is enabled, a constant is implicitly declared at the beginning of the subprogram or entry. The constant is of the type of X and is initialized to the result of evaluating X (as an expression) at the point of the constant declaration. The value of X'Old in the postcondition expression is the value of this constant; the type of X'Old is the type of X. These implicit constant declarations occur in an arbitrary order.> @dby @xhang<@xterm Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement.> @xindent @xinbull @i then@hr @fc<@i : @b @i := X;>> @xinbull then@hr @fc<@i<@ft> : @b @i'Class := @i'Class (X);@hr @i : @i @b @i(@i<@ft>);>@hr where the name X'Old denotes the object renaming.> @xinbull : @b @i := X;>@hr where @i is the nominal subtype of X. This includes the case where the type of @i is an anonymous array type or a universal type.> @xindent !corrigendum 6.1.1(35/3) @dinsa The precondition checks are performed in an arbitrary order, and if any of the class-wide precondition expressions evaluate to True, it is not specified whether the other class-wide precondition expressions are evaluated. The precondition checks and any check for elaboration of the subprogram body are performed in an arbitrary order. It is not specified whether in a call on a protected operation, the checks are performed before or after starting the protected action. For an entry call, the checks are performed prior to checking whether the entry is open. @dinst For a call to a task entry, the postcondition check is performed before the end of the rendezvous; for a call to a protected operation, the postcondition check is performed before the end of the protected action of the call. The postcondition check for any call is performed before the finalization of any implicitly-declared constants associated (as described above) with Old @fas but after the finalization of any other entities whose accessibility level is that of the execution of the callable construct. !ASIS Might affect the results returned by some functions, but no new subprograms are needed. !ACATS test Create ACATS C-Test(s) to check that the effect of X'Old is as described by these rules. !appendix From: Steve Baird Sent: Tuesday, May 29, 2012 2:26 PM 1) X'Old denotes a (constant) object. I don't believe the accessibility level of that object is defined by the current RM wording, although the intent seems clear. Not a big deal, but I think some wording is missing here. 2) X and X'Old are defined to have the same type, even if that type is anonymous. That's usually good. We want (I think) to allow Table : array (1 .. 3) of Integer; procedure Foo with Post (Table = Table'Old); If, however, X is of an anonymous access type, then things get odd. What does it mean to say that a standalone constant has the same type as, say, an access discriminant? This makes no sense. Even if X itself is a standalone object, having two such objects sharing the same type leads to problems (e.g., does the accessibility level of the type of X'Old then depend on the value most recently assigned to X?). I see two choices: A) Disallow X'Old if X is of an anonymous access type. B) If X is of an anonymous access type, define X'Old to be a standalone constant of an anonymous access type having the same designated subtype as the type of X. X'Old then follows the usual accessibility rules for such a constant. Opinions? **************************************************************** From: Bob Duff Sent: Tuesday, May 29, 2012 2:36 PM > 1) X'Old denotes a (constant) object. I don't believe the > accessibility level of that object is > defined by the current RM wording, although > the intent seems clear. Not a big deal, but > I think some wording is missing here. Isn't that covered by saying where the object is declared? > 2) X and X'Old are defined to have the same type, > even if that type is anonymous. > > That's usually good. We want (I think) to allow > > Table : array (1 .. 3) of Integer; > > procedure Foo > with Post (Table = Table'Old); > > If, however, X is of an anonymous access type, > then things get odd. What does it mean to say that > a standalone constant has the same type as, say, > an access discriminant? This makes no sense. Agreed. > Even if X itself is a standalone object, having > two such objects sharing the same type leads to > problems (e.g., does the accessibility level of the > type of X'Old then depend on the value most recently > assigned to X?). > > I see two choices: > A) Disallow X'Old if X is of an anonymous access type. > B) If X is of an anonymous access type, define X'Old > to be a standalone constant of an anonymous access > type having the same designated subtype as the type > of X. X'Old then follows the usual accessibility rules > for such a constant. > > Opinions? B), I think. A) seems like an arbitrary restriction related to arcane language-lawyerly mumbo jumbo that could never be explained to normal programmers. B) is what you'd get if you just wrote the code by hand in the natural way. **************************************************************** From: Ed Schonberg Sent: Tuesday, May 29, 2012 2:44 PM > I see two choices: > A) Disallow X'Old if X is of an anonymous access type. > B) If X is of an anonymous access type, define X'Old > to be a standalone constant of an anonymous access > type having the same designated subtype as the type > of X. X'Old then follows the usual accessibility rules > for such a constant. > > Opinions? B) seems preferable. It is what a user would intuitively expect, and it does not require yet another exception to some RM rule. **************************************************************** From: Steve Baird Sent: Tuesday, May 29, 2012 3:08 PM >> 1) X'Old denotes a (constant) object. I don't believe the >> accessibility level of that object is >> defined by the current RM wording, although >> the intent seems clear. Not a big deal, but >> I think some wording is missing here. > > Isn't that covered by saying where the object is declared? > Maybe you are right. We did decide that we wanted an AARM note about finalization (6.1.1(27.d)) in what seems like an analogous situation. Maybe that is all we need here (or perhaps not even that). Speaking very (probably excessively) strictly, all we have is The value of X'Old in the postcondition expression is the value of this constant; the type of X'Old is the type of X. as opposed to something like X'Old is a name that denotes this constant. , which would clearly settle the issue. If folks think no changes are needed here, I'm ok with that. >> Opinions? > > B), I think. > > A) seems like an arbitrary restriction related to arcane > language-lawyerly mumbo jumbo that could never be explained to normal > programmers. > > B) is what you'd get if you just wrote the code by hand in the natural > way. I agree. I think the best argument for A over B is an assertion that this is a totally unimportant case that nobody cares about; yes, it should be well-defined, but nobody cares what that definition is. Choice A requires less RM wording, so let's go with that. But as you point out, choice B is more regular even if it requires more RM wording. Choice A only makes sense if this is a case we don't care about; if we don't care about it, then why would we want to introduce a special-case rule for it? **************************************************************** From: Tucker Taft Sent: Tuesday, May 29, 2012 3:34 PM I agree with the others that we want to allow references to objects of an anonymous access type. In most cases these are constants anyway, but in the rare case where they might change, I can't imagine justifying a restriction against referring to their 'Old value. A "TBH" rule sounds just about right. No one other than an implementor could even imagine there is a problem. **************************************************************** From: Randy Brukardt Sent: Wednesday, June 6, 2012 10:46 PM You're right. But your last sentence is way too broad. It should read: "No one other than Steve Baird (and maybe Adam Beneschan) could even imagine there is a problem." ;-) **************************************************************** From: Steve Baird Sent: Thursday, June 7, 2012 2:45 PM Is the following example legal? I think it should be, but I also think it isn't. procedure Old_Test is procedure Foo (X : in out Natural) with Post => X = (case X'Old is when 0 => 0, when Positive => X'Old - 1); procedure Foo (X : in out Natural) is begin if X > 0 then X := X - 1; end if; end; begin null; end; 6.1.1 says nothing about the nominal subtype of X'Old, which leaves us with only 4.1.4(9/3): For an attribute_reference that denotes a value or an object, if its type is scalar, then its nominal subtype is the base subtype of the type; I'd like to consider defining the nominal subtype of X'Old to be that of X. Presumably wording for this would go in 6.1.1, not 4.1.4, but that's a detail. The strongest argument I can see against doing this is an assertion that this is "insufficiently broken"; it just doesn't matter, so no change is needed. Opinions? **************************************************************** From: Tucker Taft Sent: Thursday, June 7, 2012 2:52 PM > .. I'd like to consider defining the nominal subtype of X'Old to be > that of X. That makes sense. **************************************************************** From: Bob Duff Sent: Thursday, June 7, 2012 3:13 PM > Is the following example legal? > I think it should be, but I also think it isn't. I agree with both. > I'd like to consider defining the nominal subtype of X'Old to be that > of X. Yes. >... Presumably wording for this would go in 6.1.1, not 4.1.4, but >that's a detail. Agreed. **************************************************************** From: Steve Baird Sent: Thursday, June 7, 2012 12:08 PM 6.1.1(26/3) says: the type of X'Old is the type of X This means that, for example, for a formal parameter X of type T, the implicitly declared constant referenced by a use of X'Old behaves as though it were declared by : constant T := X; There are two problems with this in the case where T is a specific tagged type: 1) If T is abstract, we are declaring an object of an abstract type. 2) Even if T is not abstract, the runtime tags of X and X'Old may not match, which can affect (among other things) the body executed by a dispatching call. Given procedure P (X : in out Some_Specific_Tagged_Type) with Post => Some_Func_That_Does_Redispatching (X, X'Old); subtype Sstt is Some_Specific_Tagged_Type; , I'm arguing that the implicit declaration that X'Old denotes should behave as though it were declared via something like : constant Sstt'Class := Sstt'Class (X); : Sstt renames Sstt (); -- rename of a view conversion where the use of X'Old should refer to the rename, . This is only a change in dynamic semantics. The static semantics of X'Old (e.g., anything involving type or name resolution) would be unaffected by this change. Dynamically, however, this means that X'Tag = X'Old'Tag (speaking loosely here - more precisely, Sstt'Class (X)'Tag = Sstt'Class (X'Old)'Tag). Note that problem #1 is "must fix" hole in the language, but it could be solved more simply by a rule that the prefix of an Old attribute shall not be of an abstract type. This would not help with problem #2 and would take away arguably useful functionality. Problem #2 is more of usability issue. The language is well-defined int hsi case, but this definition is not what users want and expect. If we view that problem #2 is an unimportant corner case that nobody cares about, then the simpler solution that solves only problem #1 might make sense. I think the "fix the dynamic semantics" solution that I am proposing would not require adding a lot of complexity to the RM. Perhaps just a note saying X'Old has the same runtime tag as X and an AARM note showing the view conversion given above. Do folks prefer a) the legality rule that addresses only the abstract type problem b) the dynamic semantics change that addresses the full problem c) none of the above ? **************************************************************** From: Tucker Taft Sent: Thursday, June 7, 2012 12:23 PM > 6.1.1(26/3) says: > the type of X'Old is the type of X > ... > I think the "fix the dynamic semantics" solution that I am proposing > would not require adding a lot of complexity to the RM. > Perhaps just a note saying X'Old has the same runtime tag as X and an > AARM note showing the view conversion given above. I agree with this approach. No need to make 'Old illegal if we fix the dynamic semantics. **************************************************************** From: Edmond Schonberg Sent: Thursday, June 7, 2012 12:54 PM > Do folks prefer > a) the legality rule that addresses only the abstract type problem > b) the dynamic semantics change that addresses the full problem > c) none of the above > ? Strongly prefer b). **************************************************************** From: Gary Dismukes Sent: Thursday, June 7, 2012 1:01 PM > I agree with this approach. No need to make 'Old illegal if > we fix the dynamic semantics. I agree as well (with choice b), since it seems easy enough to handle these cases right in both the RM and implementations. **************************************************************** From: Tullio Vardanega Sent: Thursday, June 7, 2012 1:23 PM > Do folks prefer > a) the legality rule that addresses only the abstract type problem > b) the dynamic semantics change that addresses the full problem > c) none of the above > ? b) for me. **************************************************************** From: Robert Dewar Sent: Thursday, June 7, 2012 4:54 PM > I agree with this approach. No need to make'Old illegal if > we fix the dynamic semantics. I agree, this does make the best sense **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 1:04 AM > 6.1.1(26/3) says: > the type of X'Old is the type of X > > This means that, for example, for a formal parameter X of type T, the > implicitly declared constant referenced by a use of X'Old behaves as > though it were declared by > : constant T := X; Right. Indeed, I prefer to say that it *is* declared by X'Old : constant T := X; which is an implicit declaration given at the start of the subprogram. At the risk of stepping in front of what appears to be a speeding freight train, I'm going to disagree with everyone else's conclusions of Steve's various issues. The above is the model of X'Old, and we've been very careful to follow this model exactly. We chose this for two reasons: (1) To have a very simple model in which we did not have to explain all of the semantic ramifications. Indeed, we've explained the consequences in AARM notes, and not in normative wording (which might conflict with the way that this model works). (2) To match what users would have written had this feature not existed. That is, if they needed the effect of X'Old in an Assertion, they almost certainly would have written something like: X_Old : constant T := X; ... pragma Assert (X = X_Old + 1); We ought to be *very* careful about deviating from this model. > There are two problems with this in the case where T is a specific > tagged type: > 1) If T is abstract, we are declaring an object of an abstract type. Well, given that we're following the model exactly, the constant declaration is clearly illegal (because writing it explicitly would be illegal). QED. More specifically, the current wording says that "a constant is declared" and that it is "of the type of X". Such a declaration is illegal if the type of X is abstract. This is the same sort of conclusion that we've reached for many other questions on X'Old, and documented them in AARM notes, so I don't see why you think this one is different. Moreover, I think this should be true irregardless of how any other issues are decided. For one thing, it's virtually impossible to write such an object in a useful way. The only way to give such a type to an object is via a type conversion. While Abstr(Obj)'Old may be syntactically allowed, it's a pretty silly thing to write. There are no (specific) abstract components or objects. So that pretty much leaves parameters. If the parameter is a controlling operand, the rules banning Post for abstract and null routines mean that the postconditions have to be Post'Class. In which case Param (and thus Param'Old) have type Abstr'Class. If the parameter is not a controlling parameter, it's next to useless and should have been illegal from the beginning (the only way to pass something as a specific abstract type is via a type conversion -- which is nasty to the users and almost always represents a bug -- such parameters should be Abstr'Class). Since the parameter should never have been written in this case, I cannot care about Param'Old. Thus I don't see any cases in which anyone *should* care about Param'Old where Param has a specific abstract type. So why corrupt the model to make it legal?? > 2) Even if T is not abstract, the runtime tags of X and X'Old may > not match, which can affect (among other things) the body > executed by a dispatching call. Are you sure? I believe that you are saying that given: X_Old : constant Sstt := X; X_Old and X might have different tags. I don't see how you come to that conclusion based on the Standard. 3.3.1(17) says "If the object_declaration includes an initialization expression, the (explicit) initial value is obtained by evaluating the expression and converting it to the nominal subtype (which might raise Constraint_Error - see 4.6)." That subtype conversion is a view conversion, so the tag is preserved as it is for parameter passing. I vaguely remember something like what you describe, but I can't find anything in the standard that says that this declaration gets some specific tag. Maybe it should, but I don't see anything that says that. > Given > procedure P (X : in out Some_Specific_Tagged_Type) > with Post => Some_Func_That_Does_Redispatching (X, X'Old); > > subtype Sstt is Some_Specific_Tagged_Type; > > , I'm arguing that the implicit declaration that X'Old denotes should > behave as though it were declared via something like > > : constant Sstt'Class := Sstt'Class (X); > : Sstt renames Sstt (); > -- rename of a view conversion > > where the use of X'Old should refer to the rename, . This is insane. You are completely dumping the "simple model", as this violates both of the principles which guided it: (1) is dead because the semantics is no longer implicit in a simple declaration; it will have to be explained in detail. (And then we will have to explain *all* of the semantics in detail, for all types, because it would be very confusing to have a detail explanation in one case and handwaving in all other cases -- on top of which, we could no longer justify the "TBH" for anonymous access types and would have explain that case in detail as well. And (2) is violated because absolutely *no* programmer would ever write the above! They'd almost always just write X_Old : constant Sstt := X; as they probably don't care about redispatching. (In many cases, redispatching is evil and causes significant trouble with program logic.) And if they *do* care about redispatching, they probably would have written X_Old : constant Sstt'Class := Sstt'Class(X); > This is only a change in dynamic semantics. The static semantics of > X'Old (e.g., anything involving type or name > resolution) would be unaffected by this change. Dynamically, however, > this means that X'Tag = X'Old'Tag (speaking loosely here - more > precisely, Sstt'Class (X)'Tag = Sstt'Class (X'Old)'Tag). This is madness. You now are saying the static semantics and dynamic semantics are different than for any other object in the Ada standard. This almost certainly going to cause other anomolies by having the nominal subtype differing in this way. I can't wait for Adam (normally I'd say Steve, but since you're Steve, that probably won't work) to show us all of the problems. > Note that problem #1 is "must fix" hole in the language, but it could > be solved more simply by a rule that the prefix of an Old attribute > shall not be of an abstract type. There is no fix needed for #1; it already follows from the existing model. Maybe we need another TBH, but that's all that's necessary to fix this. > This would > not help with problem #2 and would take away arguably useful > functionality. I'm still dubious that there is any real problem here. Since redispatching is usually evil, it's unlikely that anyone will care what the tag of X'Old is. > Problem #2 is more of usability issue. The language is well-defined > int hsi case, but this definition is not what users want and expect. I doubt that users will care in the vast majority of cases. The only time they ought to care is in a Post'Class, but in that case Param'Old has a class-wide type and the tag will be preserved for that reason. Redispatching in a Post expression is almost certainly going to be evil; it would certainly prevent most static analysis and could cause all sorts of logic problems. About the only time it would make sense is if the procedure itself was evil and used redispatching. > If we view that problem #2 is an unimportant corner case that nobody > cares about, then the simpler solution that solves only problem #1 > might make sense. Which is to do nothing at all (my suggestion). > I think the "fix the dynamic semantics" solution that I am proposing > would not require adding a lot of complexity to the RM. > Perhaps just a note saying X'Old has the same runtime tag as X and an > AARM note showing the view conversion given above. I *strongly* disagree with this. This is totally abandoning the "simple model" of a standard constant declaration, because currently we expect *everything* (finalization, accessibility, checking, etc.) to be implied by that model. As soon as you start modifying parts of that model ("it's everything but X and Y and Z") you have lost the ability to ignore the details. And then we have to define all of the details we've been trying to ignore. I especially disagree with the notion that "a note" could be used to describe such a major deviation from the simple model (presuming your original premise is correct, which I cannot verify). This will require detailed normative wording. And once you add that for this case, we have to do the same for anonymous access. Finally, to accomplish what you are recommending for abstract types, you need to add another violation of the simple model to *allow* abstract constants. I cannot see any way to justify that within the current wording, at least without losing all of the existing ramifications. (That is, if we declare that this "declaration" is not an "object_declaration", then we no longer have defined semantics for checking, finalization, and the like, because it is now some new kind of declaration not covered by the current wording.) > Do folks prefer > a) the legality rule that addresses only the abstract type problem > b) the dynamic semantics change that addresses the full problem > c) none of the above > ? I prefer doing nothing at all, because the "legality rule" is implied by the simple model (I suppose an AARM note pointing out the Ramification would be a good idea). I'm dubious that anyone will care about either of these "problems" in practice. Do we have any evidence that either of these "problems" matters in real applications? (Steve, like Adam and the ACATS, is good at causing "priority inversion", causing unimportant problems to be worked on.) The other reason that I would prefer doing nothing is that Steve has been finding a problem a week in X'Old for the last month or so. I don't see any reason to think that this is the *last* problem that he or anyone else is going to find. Perhaps one of those new problems will require more radical solutions, and if so, I'd hate to spend a lot of effort writing wording to fix this particular problem. (AARM notes are *not* sufficient if you want to change the object's tag or make abstract objects legal.) I've already spent two hours writing an AI to address the previous issues; that is completely wasted time if we junk our dependence on the "simple model" and I'm not looking forward to spending an hour tomorrow throwing that work away to replace it with TBDs. I can easily believe that in a couple of years that we may want to revisit how X'Old is defined, but I'm dubious that now is the time. Let's figure out what's important before we decide to turn two sentences into two pages of RM wording. **************************************************************** From: Robert Dewar Sent: Friday, June 8, 2012 5:07 AM I must say that reading Randy's note on this subject, I have changed my mind, and 100% agree with him. **************************************************************** From: Tucker Taft Sent: Friday, June 8, 2012 12:21 PM I understand your point Randy, but I believe the user view is that "X'Old" is a way to refer to the value of "X" on entry. It should look and feel as much as possible like "X" rather than an imperfect copy of X. Yes, there are limitations to how perfect can be the copy of X, but the requirement that the redispatching properties be the same seems reasonable and is clearly implementable. All we are saying is that both the compile-time type and the run-time tag should match between X and X'Old. That doesn't seem very radical. Unfortunately, a simple-minded X_Old : constant T := X; does not accomplish that, if X is a "view" of an actual object whose type is some descendant of T. Note that any time you inherit a dispatching operation, the controlling parameter ends up being such a view when that inherited operation's body is invoked. This happens for abstract types as well, when the abstract type has any "default" implementations of its operations. Since postconditions generally involve parameters, any postcondition on a dispatching operation, if inherited, will introduce this issue. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 1:19 PM > Indeed, I prefer to say that it *is* declared by > > X'Old : constant T := X; > I agree. I don't like the existing wording: The value of X'Old in the postcondition expression is the value of this constant; the type of X'Old is the type of X. I'd rather say that the name X'Old denotes this constant. Then, once we have precisely described the implicit constant declaration, we wouldn't have to talk about properties of the attribute (e.g., accessibility level). > At the risk of stepping in front of what appears to be a speeding > freight train, I'm going to disagree with everyone else's conclusions > of Steve's various issues. > > The above is the model of X'Old, and we've been very careful to follow > this model exactly. Generally true, although wouldn't you agree that we need to deviate from this model in the case of an anonymous access type? > We chose this for two reasons: > (1) To have a very simple model in which we did not have to explain > all of the semantic ramifications. Indeed, we've explained the > consequences in AARM notes, and not in normative wording (which might > conflict with the way that this model works). I agree with respect to dynamic semantics. With respect to legality rules, I disagree. If we decide, for example, to disallow X'Old in the case where X is of an abstract type, then I think we should say so. Leaving this as an implicit consequence of the constant declaration rules seems confusing at best; I don't think it is obvious what legality rules apply to such an implicit declaration. > (2) To match what users would have written had this feature not existed. > That is, if they needed the effect of X'Old in an Assertion, they > almost certainly would have written something like: > > X_Old : constant T := X; > > ... > > pragma Assert (X = X_Old + 1); I think that here you are assuming the conclusion that you are trying to prove. If a user wants X_Old to be of the same type as X but also wants X_Old to behave the same way as X when used as a controlling operand in a dispatching call, then the user would "almost certainly" not declare X_Old in the way you describe. > We ought to be *very* careful about deviating from this model. I think the model we need to be very careful about deviating from is that X'Old *completely* captures the value of X at the point of the subprogram declaration (tag and all). >> There are two problems with this in the case where T is a specific >> tagged type: >> 1) If T is abstract, we are declaring an object of an abstract type. > > Well, given that we're following the model exactly, the constant > declaration is clearly illegal (because writing it explicitly would be > illegal). QED. As noted above, I think this is bogus. If we want to reject this, we should say so explicitly. > Moreover, I think this should be true irregardless of how any other > issues are decided. For one thing, it's virtually impossible to write > such an object in a useful way. The only way to give such a type to an > object is via a type conversion. While Abstr(Obj)'Old may be > syntactically allowed, it's a pretty silly thing to write. > > There are no (specific) abstract components or objects. So that pretty > much leaves parameters. If the parameter is a controlling operand, the > rules banning Post for abstract and null routines mean that the > postconditions have to be Post'Class. In which case Param (and thus > Param'Old) have type Abstr'Class. > > If the parameter is not a controlling parameter, it's next to useless > and should have been illegal from the beginning (the only way to pass > something as a specific abstract type is via a type conversion -- > which is nasty to the users and almost always represents a bug -- such > parameters should be Abstr'Class). Since the parameter should never > have been written in this case, I cannot care about Param'Old. > > Thus I don't see any cases in which anyone *should* care about > Param'Old where Param has a specific abstract type. So why corrupt the > model to make it legal?? What about package Pkg is type T is abstract tagged null record; function Count (X : T) return Natural is abstract; end Pkg; use Pkg; procedure P (X : in out T) with Post => Count (T'Class (X)) <= Count (T'Class (X'Old)); ? Do you view this as a pathological corner case because the parameter type is T, not T'Class? I don't. >> 2) Even if T is not abstract, the runtime tags of X and X'Old may >> not match, which can affect (among other things) the body >> executed by a dispatching call. > > Are you sure? I believe that you are saying that given: > > X_Old : constant Sstt := X; > > X_Old and X might have different tags. I don't see how you come to > that conclusion based on the Standard. Yes, certainly X_Old and X might have different tags. I think you are confused here. If an object is declared to be of a specific tagged type, then its tag does not come from its initial value. > 3.3.1(17) says "If the object_declaration includes an initialization > expression, the (explicit) initial value is obtained by evaluating the > expression and converting it to the nominal subtype (which might raise > Constraint_Error - see 4.6)." That subtype conversion is a view > conversion, so the tag is preserved as it is for parameter passing. I > vaguely remember something like what you describe, but I can't find > anything in the standard that says that this declaration gets some > specific tag. Maybe it should, but I don't see anything that says that. Let me get back to you with RM justification, but the Gnat compiler (which I believe is correct here) generates code for this example with Text_IO; use Text_IO; procedure old_test is package Pkg is type T1 is tagged null record; procedure Foo (X : T1); type T2 is new T1 with record F1, F2 : Integer; end record; Overriding procedure Foo (X : T2); end Pkg; package body Pkg is procedure Foo (X : T1) is begin Put_Line ("called T1's Foo"); end; procedure Foo (X : T2) is begin Put_Line ("called T2's Foo"); end; end Pkg; use PKg; procedure P (X : T1) is X_Copy : constant T1 := X; begin Foo (T1'Class (X)); Foo (T1'Class (X_Copy)); end P; Y : T2; begin P (T1 (Y)); end; which produces the following output called T2's Foo called T1's Foo I udnerstand that this is not the same as providing RM chapter and verse to justify my position, but I don't think it is very likely that Gnat would be wrong on such a fundamental point. >> Given >> procedure P (X : in out Some_Specific_Tagged_Type) >> with Post => Some_Func_That_Does_Redispatching (X, X'Old); >> >> subtype Sstt is Some_Specific_Tagged_Type; >> >> , I'm arguing that the implicit declaration that X'Old denotes should >> behave as though it were declared via something like >> >> : constant Sstt'Class := Sstt'Class (X); >> : Sstt renames Sstt (); >> -- rename of a view conversion >> >> where the use of X'Old should refer to the rename, . > > This is insane. You are completely dumping the "simple model", Not at all. The "simple model" that matters, I believe, is that X'Old captures the *complete* value of X. That's what users expect. > as this > violates both of the principles which guided it: (1) is dead because > the semantics is no longer implicit in a simple declaration; it will > have to be explained in detail. (And then we will have to explain > *all* of the semantics in detail, for all types, because it would be > very confusing to have a detail explanation in one case and handwaving > in all other cases -- on top of which, we could no longer justify the > "TBH" for anonymous access types and would have explain that case in detail as > well. > > And (2) is violated because absolutely *no* programmer would ever > write the above! They'd almost always just write > X_Old : constant Sstt := X; > as they probably don't care about redispatching. (In many cases, > redispatching is evil and causes significant trouble with program > logic.) Again, you are assuming what you are trying to prove. > And if they *do* care about redispatching, they probably would have written > X_Old : constant Sstt'Class := Sstt'Class(X); > That's a stronger argument, but I don't think we want to change the rule that X and X'Old have the same type. My proposal reconciles the two requirements. I agree that a simpler solution would be possible if we were willing to give up on either - X and X'Old must statically have the same type - X'Old must dynamically capture the complete value of X at the point where the implicit constant is declared >> This is only a change in dynamic semantics. The static semantics of >> X'Old (e.g., anything involving type or name >> resolution) would be unaffected by this change. Dynamically, however, >> this means that X'Tag = X'Old'Tag (speaking loosely here - more >> precisely, Sstt'Class (X)'Tag = Sstt'Class (X'Old)'Tag). > > This is madness. You now are saying the static semantics and dynamic > semantics are different than for any other object in the Ada standard. > This almost certainly going to cause other anomolies by having the > nominal subtype differing in this way. I can't wait for Adam (normally > I'd say Steve, but since you're Steve, that probably won't work) to > show us all of the problems. > As noted above, I think you are confused about where an object gets its tag from in the case of an object declaration of a specific tagged type. Unless I misunderstand you (which is actually fairly likely), I think this is what leads you to conclude that I am suggesting semantics "different than for any other object in the Ada standard". I agree that a rename of a view conversion isn't a common construct, but it is "in the Ada standard". Furthermore, it is very similar to a much more common construct, parameter passing where the actual's runtime tag differs from that of the type of the formal (see the call to P in the example above). >> Note that problem #1 is "must fix" hole in the language, but it >> could be solved more simply by a rule that the prefix of an Old >> attribute shall not be of an abstract type. > > There is no fix needed for #1; it already follows from the existing model. > Maybe we need another TBH, but that's all that's necessary to fix this. > I would prefer more than a TBH, but I could live with just a TBH if we decide to ban this construct. As I have stated, I think this construct should be allowed but, if it is to be rejected, I strongly think the RM should mention this explicitly. >> ... >> I think the "fix the dynamic semantics" solution that I am proposing >> would not require adding a lot of complexity to the RM. >> Perhaps just a note saying X'Old has the same runtime tag as X and an >> AARM note showing the view conversion given above. > > I *strongly* disagree with this. This is totally abandoning the > "simple model" of a standard constant declaration, because currently > we expect > *everything* (finalization, accessibility, checking, etc.) to be > implied by that model. As soon as you start modifying parts of that > model ("it's everything but X and Y and Z") you have lost the ability > to ignore the details. And then we have to define all of the details > we've been trying to ignore. Put up or shut up? I guess the ball is in my court to come up with wording that doesn't seem excessively complicated (at least to me). > The other reason that I would prefer doing nothing is that Steve has > been finding a problem a week in X'Old for the last month or so. I > don't see any reason to think that this is the *last* problem that he > or anyone else is going to find. Perhaps one of those new problems > will require more radical solutions, and if so, I'd hate to spend a > lot of effort writing wording to fix this particular problem. (AARM > notes are *not* sufficient if you want to change the object's tag or > make abstract objects legal.) I've already spent two hours writing an > AI to address the previous issues; that is completely wasted time if > we junk our dependence on the "simple model" and I'm not looking > forward to spending an hour tomorrow throwing that work away to replace it with TBDs. FUD. > I can easily believe that in a couple of years that we may want to > revisit how X'Old is defined, but I'm dubious that now is the time. > Let's figure out what's important before we decide to turn two > sentences into two pages of RM wording. I'd like to get confirmation from the group that there is a general consensus from the group that the approach I'm suggesting is at least worth investigating. I don't want to spend effort on the details without that much encouragement. Assuming that, it sounds like the ball is in my court as noted above. **************************************************************** From: Bob Duff Sent: Friday, June 8, 2012 1:43 AM > As noted above, I think this is bogus. If we want to reject this, we > should say so explicitly. Yes, and whoever wrote the existing wording took that approach -- in particular, it explicitly forbids limited types, as opposed to just letting people deduce that from the fact that the declaration would be illegal if limited. I wouldn't mind if the RM said (explicitly), "If that declaration would be illegal, then the attribute_reference is illegal." (and then in the AARM list the consequences -- can't be limited, can't be abstract, ...). But anyway, I prefer the approach you outlined, which doesn't make the abstract case illegal. > I'd like to get confirmation from the group that there is a general > consensus from the group that the approach I'm suggesting is at least > worth investigating. I think it's worth investigating. **************************************************************** From: Tucker Taft Sent: Friday, June 8, 2012 1:51 PM > I'd like to get confirmation from the group that there is a general > consensus from the group that the approach I'm suggesting is at least > worth investigating. I don't want to spend effort on the details > without that much encouragement. Assuming that, it sounds like the > ball is in my court as noted above. As is implied by my earlier response, I agree with you that the run-time tag of X'Old should match that of X. My main justification is: ... Since postconditions generally involve parameters, any postcondition on a dispatching operation, if inherited, will introduce this issue. **************************************************************** From: Edmond Schonberg Sent: Friday, June 8, 2012 2:15 PM ... which produces the following output called T2's Foo called T1's Foo I udnerstand that this is not the same as providing RM chapter and verse to justify my position, but I don't think it is very likely that Gnat would be wrong on such a fundamental point. Possible verses: 3.3.1 (17) says that the initialization expression is converted to the nominal subtype; 4.6 5/1) says that if both target and operand types are tagged then a conversion is a view conversion 4.6 (52) describes the properties of the view. so X_Copy has type T1 and its viewable components are those in the T1 part of X. X_Copy will dispatch to a primitive of T1. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 2:21 PM > I think the model we need to be very careful about deviating from is > that X'Old *completely* captures the value of X at the point of the > subprogram declaration (tag and all). Typo: "subprogram declaration" => "constant declaration". > If an object is declared to be of a specific tagged type, then its tag > does not come from its initial value. > ... > Let me get back to you with RM justification 3.9(19-20). Bob Duff wrote: > I wouldn't mind if the RM said (explicitly), "If that declaration > would be illegal, then the attribute_reference is illegal." (and then > in the AARM list the consequences -- can't be limited, can't be abstract, > ...). Interestingly, that approach would allow limited prefixes which meet the conditions of 7.5(2.1/3): aggreggates, function calls, etc. **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 2:41 PM ... > > Thus I don't see any cases in which anyone *should* care about > > Param'Old where Param has a specific abstract type. So why corrupt > > the model to make it legal?? > > > > What about > > package Pkg is > type T is abstract tagged null record; > function Count (X : T) return Natural is abstract; > end Pkg; > use Pkg; > > procedure P (X : in out T) with Post => > Count (T'Class (X)) <= Count (T'Class (X'Old)); > > ? > > Do you view this as a pathological corner case because the parameter > type is T, not T'Class? I don't. Yes, it is almost always wrong to declare a non-primitive subprogram with a specific parameter of some tagged type. It means that the subprogram breaks in the face of extension, which is the entire point of using tagged types in the first place. It's not quite wrong enough to have made it illegal, but it's close. (Our style guide requires justification documentation for any such subprogram.) It's even worse for an abstract tagged type, because there cannot be any objects of that type and thus it's necessary (somewhere) to have a type conversion to even call the subprogram. Moreover, the primary legitimate reason to use such a subprogram (because you have some operation that only makes sense on a specific type) does not apply here, as there can be no objects of this type. Thus the subprogram has a usability problem *and* always is unnecessarily restrictive. If it wasn't too late, I would have suggested that any such parameter be illegal. Thus I cannot care about the semantics of X'Old on a procedure that should never have been written in the first place. ... > I udnerstand that this is not the same as providing RM chapter and > verse to justify my position, but I don't think it is very likely that > Gnat would be wrong on such a fundamental point. I believe you, I just wanted to find out what the actual requirement was and I couldn't find any reason for this behavior that we all assume. ... > > This is insane. You are completely dumping the "simple model", > > Not at all. The "simple model" that matters, I believe, is that X'Old > captures the *complete* value of X. That's what users expect. Maybe, but that's *not* the "simple model" that we've been using to justify not changing the current wording and presuming that everything falls out. If you really want to make this change, then we need to be explicit about it, and that means completely rewording this part of the definition of X'Old. (Aside: This currently is all inside the definition of the attribute. I think expanding this wording much more means that we need to find some way to separate it from the attribute definition, which otherwise will become unwieldy - in part because of the heavily indented formatting that is required.) ... > > And (2) is violated because absolutely *no* programmer would ever > > write the above! They'd almost always just write > > X_Old : constant Sstt := X; as they probably don't care > > about redispatching. (In many cases, redispatching is evil and > > causes significant trouble with program > > logic.) > > Again, you are assuming what you are trying to prove. Huh? Absolutely *no* programmer is going to write two declarations for this case. What they would do is determine which of the two possibilities makes sense for their application and use that. I'd be surprised if anyone *ever* has written the rename you gave, in any context. ... > Unless I misunderstand you (which is actually fairly likely), I think > this is what leads you to conclude that I am suggesting semantics > "different than for any other object in the Ada standard". > > I agree that a rename of a view conversion isn't a common construct, > but it is "in the Ada standard". > Furthermore, it is very similar to a much more common construct, > parameter passing where the actual's runtime tag differs from that of > the type of the formal (see the call to P in the example above). You cannot write an object_declaration which has the semantics that you want. I suppose we could formally define the specific tagged case with the two declaration model that you gave above, but that is wildly more complex. > >> ... > >> I think the "fix the dynamic semantics" solution that I am > >> proposing would not require adding a lot of complexity to the RM. > >> Perhaps just a note saying X'Old has the same runtime tag as X and > >> an AARM note showing the view conversion given above. > > > > I *strongly* disagree with this. This is totally abandoning the > > "simple model" of a standard constant declaration, because currently > > we expect *everything* (finalization, accessibility, checking, etc.) > > to be > > implied by that model. As soon as you start modifying parts of that > > model ("it's everything but X and Y and Z") you have lost the > > ability to ignore the details. And then we have to define all of the > > details we've been trying to ignore. > > Put up or shut up? > I guess the ball is in my court to come up with wording that doesn't > seem excessively complicated (at least to me). Right now it doesn't matter, because the deadline for adding things to the Stockholm AIs is right now. (I'm finalizing the agenda and AIs this afternoon.) I suppose it is OK to bring something to the meeting proper, but it isn't going to be in the filed AIs. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 3:30 PM >> Do you view this as a pathological corner case because the parameter >> type is T, not T'Class? I don't. > > Yes, Ok, we agree to disagree. >>> This is insane. You are completely dumping the "simple model", >> Not at all. The "simple model" that matters, I believe, is that X'Old >> captures the *complete* value of X. That's what users expect. > > Maybe, but that's *not* the "simple model" that we've been using to > justify not changing the current wording and presuming that everything falls > out. Yes, you are right. > If you really want to make this change, then we need to be explicit > about it, and that means completely rewording this part of the definition of > X'Old. I'm working on it. > (Aside: This currently is all inside the definition of the attribute. > I think expanding this wording much more means that we need to find > some way to separate it from the attribute definition, which otherwise > will become unwieldy - in part because of the heavily indented > formatting that is > required.) We'll see. Attribute definitions in general are a case where the RM's usual distinctions between static semantics, legality rules, and dynamic semantics break down, so there is precedent for lumping everything together. I already hear you saying "If Johnny jumped off a cliff, would you jump too because now there is precedent?". > Huh? Absolutely *no* programmer is going to write two declarations for > this case. What they would do is determine which of the two > possibilities makes sense for their application and use that. I'd be > surprised if anyone *ever* has written the rename you gave, in any context. But they certainly have done the same sort of thing (implicitly, possibly without even thinking about it) via parameter passing. If we really wanted to (and believe me, I'm not advocating this), we could get rid of the rename and instead introduce a post-condition checking procedure which has a formal parameter of the specific type; the constant is then declared to be of the class-wide type and is passed as an actual parameter to the procedure. The desired semantics can be expressed in terms of "familiar" constructs; I just thought the rename of a view conversion was cleaner. > ... > > You cannot write an object_declaration which has the semantics that > you want. I suppose we could formally define the specific tagged case > with the two declaration model that you gave above, but that is wildly more complex. You may be right that I need to mention the two declarations, and that this isn't as tidy as always using one. We'll see how bad it gets. > I suppose it is OK to bring something to the meeting proper, but it > isn't going to be in the filed AIs. That's fine. **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 4:11 PM > >> Do you view this as a pathological corner case because the parameter > >> type is T, not T'Class? I don't. > > > > Yes, > > Ok, we agree to disagree. I should point out that that I don't consider it "pathological" because it's easy to write and everyone has done so, but rather that writing it is wrong in virtually every case. Thus I don't care what happens. The fact that Ada allows it at all is a bug in Ada. ... > > (Aside: This currently is all inside the definition of the attribute. > > I think expanding this wording much more means that we need to find > > some way to separate it from the attribute definition, which > > otherwise will become unwieldy - in part because of the heavily > > indented formatting that is > > required.) > > > > We'll see. Attribute definitions in general are a case where the RM's > usual distinctions between static semantics, legality rules, and > dynamic semantics break down, so there is precedent for lumping > everything together. I already hear you saying "If Johnny jumped off a > cliff, would you jump too because now there is precedent?". My objection here isn't the mixing so much as the large size of the definition. Attributes should never take more than a couple of paragraphs to define, anything longer than that should be split out somehow. You're going turn two sentences into 5 paragraphs (or maybe more): If the type of X'Old is: * a specific tagged type, then ... . X'Old designates this renames. * an anonymous access type, then ... . X'Old designates this constant declaration. . I think this is too long to put inside an attribute declaration, especially if the <> text turns out to require multiple paragraphs. In particular, note how the stream attributes are defined. I think this one will need some similar organization if we do a significant rewrite. > > Huh? Absolutely *no* programmer is going to write two declarations > > for this case. What they would do is determine which of the two > > possibilities makes sense for their application and use that. I'd be > > surprised if anyone *ever* has written the rename you gave, in any > > context. > > But they certainly have done the same sort of thing (implicitly, > possibly without even thinking about it) via parameter passing. What in heavens name does that have to do with declaring by hand X_Old for use in an Assert pragma? That's what part (2) is about; how you would write this by hand in Ada 95 (or even Ada 2012 if you didn't have X'Old). I don't see any way to get parameter passing involved in that case. > If we really wanted to (and believe me, I'm not advocating this), we > could get rid of the rename and instead introduce a post-condition > checking procedure which has a formal parameter of the specific type; > the constant is then declared to be of the class-wide type and is > passed as an actual parameter to the procedure. The desired semantics > can be expressed in terms of "familiar" constructs; I just thought the > rename of a view conversion was cleaner. I agree the rename is cleaner, all I'm saying is that no one would ever write that if they were writing an Ada 95 block to emulate the effect of X'Old. And that's what the "simple model" is about: X'Old works the same as what you would have written by hand. Now it's probably true that you *can't* write by hand what you really want if you thought about it at the language-lawyer level. But that seems like a general problem with Ada rather than anything having to do with this particular problem. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 4:13 PM Here is a first attempt. ==== Replace 6.1.1(26/3) with X'Old Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram or entry. The constant has the same type and subtype as X, except in the case where X is of an anonymous access type; in that case, the constant is a stand-alone object of an anonymous access type having the designated subtype or profile of the type of X. The constant is initialized to the result of evaluating X (as an expression) at the point of the constant declaration. If X is tagged, then the tag associated with the constant is that of X. AARM: If X is of a specific tagged type T, then the implicit declaration for an occurrence of X'Old is equivalent to the following: : constant T'Class := T'Class (X); : T renames T (); , where the name X'Old denotes the rename, not the constant. This means that statically X'Old has the same type as X and dynamically X'Old has the same tag as X (which might not be T'Tag if, for example, X is a formal parameter). Prepend (append?) to 27.d(3): The implicit constant declaration defines the nominal subtype and accessibility level of X'Old. **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 4:28 PM > Replace 6.1.1(26/3) with > > X'Old > Each X'Old in a postcondition expression that is enabled denotes > a constant that is implicitly declared at the beginning of the > subprogram or entry. The constant has the same type and subtype > as X, except in the case where X is of an anonymous access type; > in that case, the constant is a stand-alone object of an anonymous > access type having the designated subtype or profile of the type > of X. The constant is initialized to the result of evaluating X > (as an expression) at the point of the constant declaration. If X > is tagged, then the tag associated with the constant is that of X. I don't buy this last sentence, since it contradicts the notion that this is a normal constant declared with the normal rules. Especially when you then follow it with an AARM note that says that it is all a lie. As I suggested in the mail that crossed with this one, I think you need to treat these three cases separately (hopefully the rest of it can be shared). > AARM: > If X is of a specific tagged type T, then the implicit declaration > for an occurrence of X'Old is equivalent to the following: > : constant T'Class := T'Class (X); > : T renames T (); > , where the name X'Old denotes the rename, not the constant. > This means that statically X'Old has the same type as X and > dynamically X'Old has the same tag as X (which might not be T'Tag > if, for example, X is a formal parameter). > > Prepend (append?) to 27.d(3): > The implicit constant declaration defines the nominal subtype and > accessibility level of X'Old. If we're rewriting this anyway, I think it would be better that we normatively say that the nominal subtype is defined this way, simply so that it shows up in the index and thus no one would think that 4.1.4(9/3) applies. It's only one more sentence. (I *don't* think this for accessibility, as there is no "default" that needs clear overriding as there is with "nominal subtype". Indeed, the "default" is probably what we want for accessibility, so only people with devious minds ;-) could be confused.) **************************************************************** From: Robert Dewar Sent: Friday, June 8, 2012 4:33 PM >> X'Old >> Each X'Old in a postcondition expression that is enabled denotes >> a constant that is implicitly declared at the beginning of the >> subprogram or entry. The constant has the same type and subtype >> as X, except in the case where X is of an anonymous access type; >> in that case, the constant is a stand-alone object of an anonymous >> access type having the designated subtype or profile of the type >> of X. The constant is initialized to the result of evaluating X >> (as an expression) at the point of the constant declaration. If X >> is tagged, then the tag associated with the constant is that of X. > > I don't buy this last sentence, since it contradicts the notion that > this is a normal constant declared with the normal rules. Especially > when you then follow it with an AARM note that says that it is all a lie. I think that Randy is being too pedantic here, and that the above paragraph is just fine as it is from a users point of view, which is all I really care about. You can add a TBH to the AARM which has all the unnecessary detail below :-) To quote Randy from later on in the message, I think only language lawyers with devious minds would be confused by the above. After all informally an assignment just copies bits from the RHS to the LHS, but we know that it doesn't work this way with tagged stuff. **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 4:50 PM > I think that Randy is being too pedantic here, and that the above > paragraph is just fine as it is from a users point of view, which is > all I really care about. You can add a TBH to the AARM which has all > the unnecessary detail below :-) Perhaps, but I must say that I am not a fan of TBHs, in particular when the topic that they address is important. (And I'm presuming from the amount of discussion on this that this is important.) I'd prefer to see an attempt at real normative wording here, rather than just more hand-waving. (After all, the RM is written for language-lawyers first, any value to users is clearly secondary.) If that's too lengthy or confusing, then perhaps a simpler version is better. But giving up without trying seems wrong, especially as we have about 7 years to get this wording right. > To quote Randy from later on in the message, I think only language > lawyers with devious minds would be confused by the above. After all > informally an assignment just copies bits from the RHS to the LHS, but > we know that it doesn't work this way with tagged stuff. You mean language-lawyers (sometimes) know. Ordinary users are often surprised that for a parameter Param : T Param'Tag doesn't have to equal T'Tag. I'm getting convinced that we need to make a change here (mainly because X'Old /= X when X is not changed by the procedure is annoying), but I would like to make it right. I don't want to get into the habit of the Baird message of the month on 'Old. **************************************************************** From: Tucker Taft Sent: Friday, June 8, 2012 4:44 PM >> What about >> >> package Pkg is >> type T is abstract tagged null record; >> function Count (X : T) return Natural is abstract; >> end Pkg; >> use Pkg; >> >> procedure P (X : in out T) with Post => >> Count (T'Class (X))<= Count (T'Class (X'Old)); >> >> ? >> >> Do you view this as a pathological corner case because the parameter >> type is T, not T'Class? I don't. > > Yes, it is almost always wrong to declare a non-primitive subprogram > with a specific parameter of some tagged type.... I might have missed your response, but for me, the more important case is inheriting a dispatching operation: package P0 is type T0 is abstract tagged private; function Count (X : T0) return Natural; -- The default implementation merely returns X.Count procedure P(X : in out T0) with Post => Count (T0'Class(X)) <= Count (T0'Class (X'Old)); -- Note that P is not abstract, even though T0 is. -- Apparently there is a reasonable default for what P does. -- "P" might use redispatching internally if there are -- other operations of T0. ... private type T0 is abstract tagged record Count : Natural := 0; end record; end P0; package P1 is type T1 is new P0.T0 with ... -- Default implementation of P is inherited -- along with its postcondition function Count (X : T1) return Natural; -- Count is overridden ... end P1; It seems clear we want to call the "same" Count on X and X'Old. Here the redispatching is directly in the postcondition. Alternatively, the redispatching might be buried in a function called from the postcondition. **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 5:08 PM >> Replace 6.1.1(26/3) with >> >> X'Old >> Each X'Old in a postcondition expression that is enabled denotes >> a constant that is implicitly declared at the beginning of the >> subprogram or entry. BTW, I think that we ought to somehow say here that this is an implicit object_declaration. That's because without the "object_declaration" term, there are many rules that don't apply, and we don't need to get into a morass because something is not defined. We had to do something like this for formal parameters of mode in; I see they say that they are a "full constant declaration", perhaps that would be better for this purpose. Note that once you do that, you'd have to treat the renames separately in the specific tagged case, which is one of many reasons why I expected we'd have to separate the three cases. **************************************************************** From: Robert Dewar Sent: Friday, June 8, 2012 5:07 PM > (After all, > the RM is written for language-lawyers first, any value to users is > clearly secondary. Well you know I disagree pretty fundamentally with that point of view. I thought it a wonderful achievment that for the first time since Algol-60, Ada-83 was a language where programmers used the standard as a standard reference source :-) :-) Later versions of Ada not so much so, though I think most Ada programmers at least try to read at least some sections of the RM (which is not true for other languages today, so we are still ahead). So I am always trying to achieve a balance :-) **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 5:38 PM I don't necessarily disagree with this point of view - we always should be striving to improve the clarity of the RM text. But clarity cannot be at the expense of correctness or completeness (as in the case at hand). That's especially true for those users that only read the RM; it can't be the case that we write text that only makes sense when interpreted by the AARM or AIs. (And of course, nothing in those other documents is normative, so people are free to come up with any other wild interpretations that they want.) **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 5:08 PM >> Replace 6.1.1(26/3) with >> >> X'Old >> Each X'Old in a postcondition expression that is enabled denotes >> a constant that is implicitly declared at the beginning of the >> subprogram or entry. BTW, I think that we ought to somehow say here that this is an implicit object_declaration. That's because without the "object_declaration" term, there are many rules that don't apply, and we don't need to get into a morass because something is not defined. We had to do something like this for formal parameters of mode in; I see they say that they are a "full constant declaration", perhaps that would be better for this purpose. Note that once you do that, you'd have to treat the renames separately in the specific tagged case, which is one of many reasons why I expected we'd have to separate the three cases. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 5:17 PM > If we're rewriting this anyway, I think it would be better that we > normatively say that the nominal subtype is defined this way, simply > so that it shows up in the index and thus no one would think that > 4.1.4(9/3) applies. It's only one more sentence. > Good point. I agree. > (I *don't* think this for accessibility, as there is no "default" that > needs clear overriding as there is with "nominal subtype". Agreed. Robert Dewar wrote: > I think that Randy is being too pedantic here, and that the above > paragraph is just fine as it is from a users point of view, which is > all I really care about. Obviously, I agree. I agree with Randy that we are playing slightly fast and loose here, saying that X'Old denotes a constant and then "clarifying" this to say that it denotes a rename (more precisely, it is "equivalent to" denoting a rename). But I agree with Robert that this is ok in this case. This is a judgment call and I can certainly see merit in Randy's position. Here is version #2, incorporating the portion of Randy's comments that I agree with. The 4.1.4 change described below grammatically reminds me of playing Blockhead (for those unfamiliar with the game, it is like Jenga except that new items are added to the tower instead of repositioning existing items). ==== Replace 6.1.1(26/3) with X'Old Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram or entry. The constant has the same type and subtype as X, except in the case where X is of an anonymous access type; in that case, the constant is a stand-alone object of an anonymous access type having the designated subtype or profile of the type of X. The constant is initialized to the result of evaluating X (as an expression) at the point of the constant declaration. If X is tagged, then the tag associated with the constant is that of X. The nominal subtype of X'Old is that of X. AARM: If X is of a specific tagged type T, then the implicit declaration for an occurrence of X'Old is equivalent to the following: : constant T'Class := T'Class (X); : T renames T (); , where the name X'Old denotes the rename, not the constant. This means that statically X'Old has the same type as X and dynamically X'Old has the same tag as X (which might not be T'Tag if, for example, X is a formal parameter). Prepend (append?) to 27.d(3): The implicit constant declaration defines the accessibility level of X'Old. In 4.1.4(9/3), prepend to the second sentence: "Unless explicitly specified otherwise, " and lower-case the "For" that formerly began the sentence. Note that this follows the existing wording for the third sentence. If a more explicit "Unless explicitly specified otherwise for a particular attribute" is preferred, should we change the third sentence too? **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 5:36 PM > > If we're rewriting this anyway, I think it would be better that we > > normatively say that the nominal subtype is defined this way, simply > > so that it shows up in the index and thus no one would think that > > 4.1.4(9/3) applies. It's only one more sentence. > > Good point. I agree. But I don't see the term "nominal subtype" in your proposed wording. You mentioned "subtype", but that's not quite the same thing. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 5:46 PM Randy Brukardt wrote: > But I don't see the term "nominal subtype" in your proposed wording. Steve Baird wrote: > The nominal subtype of X'Old is that of X. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 5:54 PM I missed that sentence completely. I was confused by the "same type and subtype" wording, which seems to say the same thing in a different way. I wonder if those can be consolidated somehow. **************************************************************** From: Robert Dewar Sent: Friday, June 8, 2012 5:20 PM > BTW, I think that we ought to somehow say here that this is an > implicit object_declaration. Perhaps we can just say it's equivalent to that object declaration (in the RM equivalent is a technical term, meaning "similar to, but not identical to" :-) :-)) **************************************************************** From: Robert Dewar Sent: Friday, June 8, 2012 5:44 PM BTW, I actually think Steve's original paragraph was clearer to most users than Randy's replacement, which requires more technical understanding to realize what the import of the renames is! **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 5:56 PM ... > BTW, I actually think Steve's original paragraph was clearer to most > users than Randy's replacement, which requires more technical > understanding to realize what the import of the renames is! Given that I never suggested a replacement, it's hard to say how you can say this with certainity. :-) I asked Steve to try to remove the contradictions in the text, and he refused to do so, so no one has attempted to write text in this way. It's possible that such text would be clearer than the original proposal. In any case, this wording should be left for the meeting or after. The constant chatter is preventing me from closing up the book for the current meeting and I have other things I need to do before I leave. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 6:13 PM > BTW, I think that we ought to somehow say here that this is an > implicit object_declaration. That's because without the > "object_declaration" term, there are many rules that don't apply, and > we don't need to get into a morass because something is not defined. Could you give an example where this makes a difference? > We had to do something like this > for formal parameters of mode in; I see they say that they are a "full > constant declaration", perhaps that would be better for this purpose. I assume you are talking about AI95-00269. This was all about staticness, so it doesn't help provide relevant examples. I wouldn't mind a requirement that the prefix of an Old attribute must not be a static expression; that would spare us from having to contemplate Named_Number'Old . **************************************************************** From: Randy Brukardt Sent: Friday, June 8, 2012 6:31 PM > > BTW, I think that we ought to somehow say here that this is an > > implicit object_declaration. That's because without the > > "object_declaration" term, there are many rules that don't > apply, and > > we don't need to get into a morass because something is not defined. > > Could you give an example where this makes a difference? That depends on how much handwaving you're willing to tolerate. For instance, we need to know how this implicit constant is initialized. That's defined in 3.3.1 for object_declarations (evaluate, convert, assign); for other things it wouldn't be defined. I thought masters might have this problem, but I see the "Heart of Darkness" only talks about declarations, so that's OK. I think there were some other cases where I saw that, but I can't remember them at this moment and I don't want to spend an hour tracking them down (there are 33 clauses that contain "object_declaration" in the Standard). We can revisit during the meeting or afterwards. > > We had to do something like this > > for formal parameters of mode in; I see they say that they > are a "full > > constant declaration", perhaps that would be better for > this purpose. > > I assume you are talking about AI95-00269. > > This was all about staticness, so it doesn't help provide relevant > examples. I suppose that could matter, but only in pathological cases. > I wouldn't mind a requirement that the prefix of an Old attribute must > not be a static expression; that would spare us from having to > contemplate Named_Number'Old . Perhaps a good idea, but a bit weird. **************************************************************** From: Steve Baird Sent: Friday, June 8, 2012 6:40 PM > That depends on how much handwaving you're willing to tolerate. For > instance, we need to know how this implicit constant is initialized. > That's defined in 3.3.1 for object_declarations (evaluate, convert, > assign); for other things it wouldn't be defined. > That one example is enough to give me something to think about. Thanks. >> I wouldn't mind a requirement that the prefix of an Old attribute >> must not be a static expression; that would spare us from having to >> contemplate Named_Number'Old . > > Perhaps a good idea, but a bit weird. Probably a bad idea, but it would spare us from having to deal with silly questions like whether Static_Constant'Old is static. **************************************************************** From: Steve Baird Sent: Friday, July 6, 2012 4:44 PM As part of my Stockholm homework I am looking at AI12-0032, the 'Old AI. The current wording about the point of the implicit constant declaration for a use of 'Old doesn't handle task entries clearly: "... a constant is implicitly declared at the beginning of the subprogram or entry." I don't think anybody even thought about what "the beginning of the ... entry" means in the case of a task entry. Intuitively, one might assume that it means "the beginning of the rendezvous". The problem with that model is that postcondition checks are performed after the rendezvous is over and the called task has gone on to other things. At least that is how I interpret the words "Upon successful return" in 6.1.1(35/3). Since the postcondition checks are where this constant is referenced, the constant has to outlive the rendezvous. And with interface types and 'Post'Class, you pretty much have to do things this way since there may be 'Old constants whose existence the called task is unaware of. Am I right in thinking that we therefore want a 'Old constant elaborated immediately after precondition checking (which occurs immediately after parameter evaluation)? For example, for a conditional entry call which is never accepted, the constant will still be declared; right? I'd like to be clear on what intent I am trying to capture before attempting wording. **************************************************************** From: Tucker Taft Sent: Sunday, July 8, 2012 10:54 AM ... > Intuitively, one might assume that it means "the beginning of the > rendezvous". The problem with that model is that postcondition checks > are performed after the rendezvous is over and the called task has > gone on to other things. At least that is how I interpret the words > "Upon successful return" > in 6.1.1(35/3). Since the postcondition checks are where this constant > is referenced, the constant has to outlive the rendezvous. > And with interface types and 'Post'Class, you pretty much have to do > things this way since there may be 'Old constants whose existence the > called task is unaware of. I certainly didn't have that model in my mind, though I'll admit I hadn't really thought about it deeply. It seems that protected entries face the same problem. Are postconditions checked as part of the protected action, after finalizing but before leaving the entry body, or are they checked at the place where the call is. I would have expected postconditions to be enforced just before leaving the entry body, and I would expect accept statements to work the same way. I would interpret "upon successful return" to mean "only if the entry body/accept statement/subprogram body is completing normally." I would not interpret it to mean that it happens at the call site, potentially long after the entry body or rendezvous finish. > Am I right in thinking that we therefore want a 'Old constant > elaborated immediately after precondition checking (which occurs > immediately after parameter evaluation)? For example, for a > conditional entry call which is never accepted, the constant will > still be declared; right? No, I don't have this model. I think it should be inside the entry body/accept statement. **************************************************************** From: Edmond Schonberg Sent: Sunday, July 8, 2012 2:29 PM I fully agree, and find Tuck's response reassuring. I found Steve's reading of the semantics of 'Old somewhere between "ingenious" and "perverse". I have always thought that the entry body is treated like a subprogram, and the postcondition is evaluated just before returning from that subprogram, i.e. immediately before completing the rendez-vous. **************************************************************** From: Randy Brukardt Sent: Sunday, July 8, 2012 6:20 PM ... > > And with interface types and 'Post'Class, you pretty much have to do > > things this way since there may be 'Old constants whose existence > > the called task is unaware of. This can't happen, because you can't derive a from (concrete) task or protected type. So there is no way to "add" an interface to an existing task or protected type. OTOH, Brad keeps complaining about that restriction (it really causes problems in his task-safe reusable types), so I wouldn't be surprised if we at least consider lifting it. In which case depending on it might be less appealing. > I certainly didn't have that model in my mind, though I'll admit I > hadn't really thought about it deeply. It seems that protected > entries face the same problem. Are postconditions checked as part of > the protected action, after finalizing but before leaving the entry > body, or are they checked at the place where the call is. I would > have expected postconditions to be enforced just before leaving the > entry body, and I would expect accept statements to work the same way. Keep in mind that the "official" model is that preconditions and postconditions are checked at the call site, not in the body. We then have a variety of permissions that allow implementing them (especially postconditions) in the body. Steve seems to have identified a problem with that "official" model, and I think we need to be careful with dismissing this out-of-hand. > I would interpret "upon successful return" to mean "only if the entry > body/accept statement/subprogram body is completing normally." I > would not interpret it to mean that it happens at the call site, > potentially long after the entry body or rendezvous finish. Well, I would! Specifically, when we wrote this wording, we meant that everything was canonically checked at the call site. And we then tried to make it possible to implement it inside the body. But that seems backwards for 'Old. (EVERYTHING seems wrong about 'Old; it's unfortunate, because it *seems* so obvious.) > > Am I right in thinking that we therefore want a 'Old constant > > elaborated immediately after precondition checking (which occurs > > immediately after parameter evaluation)? For example, for a > > conditional entry call which is never accepted, the constant will > > still be declared; right? > > No, I don't have this model. I think it should be inside the entry > body/accept statement. I agree that's the model we have for 'Old. But the model for postconditions is that they are logically evaluated at the call site. So those models inherently conflict. I now think that there is *nothing* right about the model for 'Old (the evaluation happens inside the subprogram, which no longer exists when the postcondition check is evaluated). I'm beginning to feel that 'Old is yet another coextension - a language feature that seems easy but is next to impossible to get right (and thus isn't worth the trouble). **************************************************************** From: Bob Duff Sent: Sunday, July 8, 2012 6:40 PM > Keep in mind that the "official" model is that preconditions and > postconditions are checked at the call site, ... I think the right model is that preconditions are checked at the call site, but postconditions are checked in the body. **************************************************************** From: Randy Brukardt Sent: Sunday, July 8, 2012 6:52 PM Maybe, but that's not what we wrote, and I'm not thrilled about starting over with this wording. And in any case, we wanted implementations to be able to do the evaluations in either place -- I'd definitely be against changing the model such that we're required to evaluate postconditions in the body. **************************************************************** From: Tucker Taft Sent: Monday, July 9, 2012 10:19 AM I think you can allow it to be done either place when there is no synchronization involved. But for synchronizing operations, I believe we will have to choose one, and I think the metarule Bob described is the correct one, namely that preconditions are conceptually checked before you "wait" for an entry barrier, and postconditions are checked before you give up control on completion of the entry body/rendezvous. **************************************************************** From: Edmond Schonberg Sent: Monday, July 9, 2012 10:38 AM > I think you can allow it to be done either place when there is no > synchronization involved. But for synchronizing operations, I believe > we will have to choose one, and I think the metarule Bob described is > the correct one, namely that preconditions are conceptually checked > before you "wait" for an entry barrier, So the check is not synchronous with the execution of the synchronized operation, but rather with the evaluation of the barrier? > and postconditions > are checked before you give up control on completion of the entry > body/rendezvous. Does it mean that Tasking_Error is raised in the caller if the postcondition fails, or is the failure happening outside of the task body in some way? **************************************************************** From: Steve Baird Sent: Monday, July 9, 2012 10:57 AM > ... >>> And with interface types and 'Post'Class, you pretty much have to do >>> things this way since there may be 'Old constants whose existence >>> the called task is unaware of. > > This can't happen, because you can't derive from a (concrete) task or > protected type. So there is no way to "add" an interface to an existing > task or protected type. Thank you. This misconception is what led me to think the cleaner, simpler, more intuitive model didn't work. I now think that you are right and that the "do everything within the rendezvous" model can work. > And in any case, we wanted implementations to be able to do the > evaluations in either place -- I'd definitely be against changing the > model such that we're required to evaluate postconditions in the body. In the particular case of task entries (which were not previously given much thought) there is a very big portability issue between the two approaches which is not present for other callable entities: does the callee also see the exception in the event of a pre/post-condition failure or not? I really dislike the idea of leaving this implementation-dependent in the case of a task entry. I prefer the easy-to-implement idea of wrapping an implementation-generated block around the handled sequence of statements for an accept and then performing ppc checks and 'Old constant elaborations in this block, as in accept E do Precondition_Checks; declare ... 'Old constants ... begin begin Source_Stmts; exception Source_Handlers; end; Postcondition_Checks; end; end; This also nails down the question about when the precondition checks are performed (and, for example, whether they are performed at all in the case of a conditional entry call that is never accepted). I agree that te current wording doesn't nail this stuff down; I just think it should and that the current state of affairs was not the result of a conscious decision - nobody thought about tasks. If we go with this model, it would be more consistent for protected actions to require that precondition checks (and 'Old constant elaborations) not be performed until after the protected action has begun, but that's a separate question. Again, there are portability issues here in the case of a precondition expression which performs a potentially blocking operation (and, in particular, an external call to the same protected record object). Suppose you have a belt-and-suspenders programmer who calls a protected entry and has a precondition which duplicates the barrier expression. For example, he wants to pop an element off of a protected stack and has a precondition that the stack isn't empty as well as a similar barrier expression for the Pop entry. Is this supposed to fail if the stack is empty at the time of the call, or is it supposed to block and then perform the precondition check after the barrier condition has been satisfied? And what if the precondition involves external calls to the protected object - do we have 9.5.1(15) bounded errors? Allowing internal calls from within the pre/postcondition expressions of a protected operation would be a bigger change. I don't like the idea that all this is left up to the implementation; it seems like a real portability issue. Note that we have explicit wording that says It is not specified whether in a call on a protected operation, the checks are performed before or after starting the protected action. I think this may have been written with only protected procedures and functions in mind, as opposed to entries. Even in that restricted case, it seems like this introduces portability issues. **************************************************************** From: Steve Baird Sent: Monday, July 9, 2012 11:00 AM > I think you can allow it to be done either place when there is no > synchronization involved. But for synchronizing operations, I believe > we will have to choose one, and I think the metarule Bob described is > the correct one, namely that preconditions are conceptually checked > before you "wait" for an entry barrier, and postconditions are checked > before you give up control on completion of the entry body/rendezvous. That would be fine with me. My main point is that it should be specified one way or the other. **************************************************************** From: Jean-Pierre Rosen Sent: Monday, July 9, 2012 11:25 AM > I think you can allow it to be done either place when there is no > synchronization involved. But for synchronizing operations, I believe > we will have to choose one, and I think the metarule Bob described is > the correct one, namely that preconditions are conceptually checked > before you "wait" for an entry barrier, and postconditions are checked > before you give up control on completion of the entry body/rendezvous. Agreed. If a condition does not hold, the exception is raised in the context of the one who is doing bad things. In the case of a rendezvous, this means that Assertion_Error is propagated to both - which seems logical: the caller has to know that the postcondition does not hold, and the task has to be punished for bad behaviour. **************************************************************** From: Jean-Pierre Rosen Sent: Monday, July 9, 2012 11:31 AM > I prefer the easy-to-implement idea of wrapping an > implementation-generated block around the handled sequence of > statements for an accept and then performing ppc checks and 'Old > constant elaborations in this block, as in > > accept E do > Precondition_Checks; > declare > ... 'Old constants ... > begin > begin > Source_Stmts; > exception > Source_Handlers; > end; > Postcondition_Checks; > end; > end; But with this model, if a precondition fails, the exception is propagated to the callee - violating the principle that a server should no be disturbed by any misbehaviour of the client. **************************************************************** From: Steve Baird Sent: Monday, July 9, 2012 11:45 AM > But with this model, if a precondition fails, the exception is > propagated to the callee - violating the principle that a server > should no be disturbed by any misbehaviour of the client. I sent a second message two minutes after the message that you replied to. For reasons unknown, it hasn't shown up yet. Tuck outlined the model where pre=condition checks are performed at the time of the call (so that, for example, they are performed in the case of a conditional call which is never accepted). I'll repeat my reply: > That would be fine with me. > > My main point is that it should be specified one way > or the other. **************************************************************** From: Jean-Pierre Rosen Sent: Monday, July 9, 2012 12:20 PM Fine with me too. **************************************************************** From: Randy Brukardt Sent: Monday, July 9, 2012 1:10 PM It's necessary for precondition checks to be at point of call else dispatching preconditions don't work right. **************************************************************** From: Steve Baird Sent: Monday, July 9, 2012 1:37 PM Good point. Sounds like everyone is in agreement then. Thanks. **************************************************************** From: Steve Baird Sent: Wednesday, November 28, 2012 6:11 PM The current wording in 6.1.1: Upon successful return from a call of the subprogram or entry, prior to copying back any by-copy in out or out parameters, the postcondition check is performed. Consider a call to procedure Foo with Post => Some_Predicate (Controlled_Object'Old, ...) is Local_Var : Some_Controlled_Type; begin ... end; Should postcondition checking take place after Local_Var has been finalized but before the implicitly-declared 'Old constant has been finalized? I think so. Note that (at least things stand currently) Local_Var and the 'Old constant have the same master. This means that postcondition checking needs to be performed in the middle of finalizing that master. I think a rule along these lines would be OK, but I want to be sure that there is consensus on this point before working further on formulating such a rule. Opinions? **************************************************************** From: Tucker Taft Sent: Wednesday, November 28, 2012 7:02 PM > Note that (at least things stand currently) Local_Var and the 'Old > constant have the same master. I think we have always allowed implementations to introduce extra levels of masters for temporary variables. I see 'Old as a temp, and so we should not be too concerned with exactly where it is finalized, so long as it gets finalized after its last use, and before we start the next statement at the call point. > This means that postcondition checking needs to be performed in the > middle of finalizing that master. Or you create another level. It is conceivable that the finalization of a local variable will have some side-effect (e.g., free some resource), and I believe the postcondition should be evaluated *after* that side-effect has occurred (e.g. after the resource has been freed). > I think a rule along these lines would be OK, but I want to be sure > that there is consensus on this point before working further on > formulating such a rule. > > Opinions? I can't imagine any other rule that would make as much sense as the one you have suggested. **************************************************************** From: Randy Brukardt Sent: Friday, November 30, 2012 9:40 PM ... > > Note that (at least things stand currently) Local_Var and the 'Old > > constant have the same master. > > I think we have always allowed implementations to introduce extra > levels of masters for temporary variables. For the record (I don't think it affects anything), I don't believe this. There is some wiggle room as to exactly where temporaries are finalized in some cases, but I don't think anything so significant as extra masters is allowed. (Of course, if no sane program can tell the difference, it's OK by the normal equivalence rules -- but remember that it is really easy to depend on finalization at a specific point, and we've generally agreed that this is not unreasonable in most of the examples we've had.) ... > I see 'Old as a temp, and so we should be too concerned with exactly > where it is finalized, so long as it gets finalized after its last > use, and before we start the next statement at the call point. I do agree with this, of course. I do think we ought to be slightly more liberal with all objects (allowing early finalization if they are sufficiently dead), but I've never successfully gotten that into the RM. (There are a lot of objects that are required to live long after they have no possible use, and it's easy to build abstractions that break if they are finalized early.) **************************************************************** From: Steve Baird Sent: Friday, November 30, 2012 7:07 PM Thanks to Randy for much useful discussion on this one. [Following was the !wording section for version /03 of the AI.] **************************************************************** From: Randy Brukardt Sent: Friday, November 30, 2012 9:57 PM > Thanks to Randy for much useful discussion on this one. It would have been nice, ahem, to have gotten updates to the !question (I think you added some questions, specifically the question about the finalization order) and !summary and possibly !discussion as well. I didn't detect any problems with the wording you submitted, but probably I didn't read carefully enough. :-) ****************************************************************