!standard 6.1.1(0) 11-11-12 AI05-0273-1/02 !class Amendment 11-11-11 !status Amendment 2012 11-11-12 !status ARG Approved 9-0-0 11-11-12 !status work item 11-11-11 !status received 11-11-04 !priority Low !difficulty Easy !subject Problems with the Old attribute !summary (1) The prefix of 'Old cannot contain any names that do not exist at the start of the subprogram. (2) If 'Old occurs in a subexpression that is potentially unevaluated, the prefix of the 'Old reference cannot be dynamic in any way. !problem The prefix of the 'Old attribute used in a postcondition is unconditionally evaluated when the subprogram is entered. This causes a number of problems: (1) If the prefix uses something that doesn't exist when the subprogram is entered, there is a problem: procedure Proc (X : in out String) with Post => (for all I in X'Range => X(I) /= X(I)'Old); function Foo return String with Post => Foo'Result /= Foo'Result'Old; (2) If evaluating the prefix would raise an exception, there could be a problem: Table : array (1..10) of Integer := ... procedure Bar (I : in out Natural) with Post => I > 0 and then Tab(I)'Old = 1; If I = 0 on entry, the evaluation of Tab(0) will raise Constraint_Error. The "and then" provides no protection because there is no way for the compiler to tell what I is on exit from the subprogram, so it is not known whether the value Tab(I)'Old will be needed when Bar exits. So Tab(I) has to be unconditionally evaluated on entry. The language actually requires Tab(I) to be evaluated unconditionally even if the compiler can figure out that it is never needed. That makes the problem worse. !proposal (See summary.) !wording Add before 6.1.1(21/3): An expression is *potentially unevaluated* if occurs within: * any part of a if_expression other than the first condition; * a dependent_expression of a case_expression; * the right operand of a short-circuit control form; or * a membership_choice other than the first of a membership operation. Replace 6.1.1(21/3-22/3) with: X'Old 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. Reference to this attribute is only allowed within a postcondition expression. The prefix of an Old attribute_reference shall not contain a Result attribute_reference, nor an Old attribute_reference, nor a use of an entity declared within the postcondition expression but not within prefix itself (for example, the loop parameter of an enclosing quantified_expression). The prefix of an Old attribute_reference that is potentially unevaluated shall statically denote an entity. !discussion We do not allow 'Old in the prefix of another 'Old, as it doesn't add any value: A(I'Old)'Old and A(I)'Old These have exactly the same semantics: the old (original) value of I is used in both expressions. Having two ways to write the same thing is considered confusioning. Moreover, we would need a rule requiring the I'Old constant to be evaluated before the A(I'Old)'Old constant. This would be an unnecessary complication to the wording and to implementations. For the second example, the programmer probably meant procedure Bar (I : in out Natural) with Post => I > 0 and then Tab'Old(I) = 1; which will not raise Constraint_Error (but does require copying the entire Tab array). We'll address unneeded evaluation of assertions more generally in AI05-0274-1, so we won't worry about that here. The solution that we adopted is that any 'Old reference in a subexpression that is not guaranteed to be evaluated must statically denote an entity. In this case, evaluation of the prefix doesn't make any checks and thus cannot fail, so it is OK to make that evaluation unconditionally. It's almost always possible to change such references to one that would be legal; simply move 'Old to the outermost item (as in the example above). These might cost more by copying a larger object, but they are also much more likely to reflect the actual intent. We didn't adopt this rule for all 'Old prefixes, as that would make it impossible to write various Old values. Many of the problems aren't all that compelling (a function call would not be allowed, but since significant side-effects are supposed to be avoided, such a call would be equivalent to putting 'Old on the parameter(s)), but there is clearly a performance issue involved, as copying large objects would needed even when only a small component is of interest. (Compilers could sometimes optimize most of these copies away, but that is not possible in general.) Most compelling is that some postconditions could not be written at all. For instance, consider a variation on the original example: procedure Bar2 (P : in out Positive) with Post => Tab(P)'Old = 1 or else P > 10; Here "P" in Tab(P) is really P'Old, and in this example, P can be changed by the subprogram body. Moving the 'Old to Tab (giving Tab'Old(P)) would not necessarily give the same answer, since P could have changed during the execution of the subprogram. Tab(P)'Old is the only (correct) way to write this postcondition. Thus, rather than throwing the baby out with the bathwater, we only make cases where there is potentially trouble illegal, rather than all of them. !example (See problem.) !corrigendum 6.1.1(0) @dinsc Force a conflict; the real text is found in the conflict file. !ACATS Test ACATS B-Tests should be constructed to check these rules. !ASIS !appendix From: Steve Baird Sent: Friday, November 4, 2011 3:21 PM Are we missing some legality checks with respect to the allowable prefix of an Old attribute? I think both of the following attribute uses should be illegal: package Pkg is procedure Proc (X : in out String) with Post => (for all I in X'Range => X(I) /= X(I)'Old); function Foo return String with Post => Foo'Result /= Foo'Result'Old; end Pkg; Do others agree that a) they should be illegal and b) these cases are not covered by current RM wording and c) this is a very low-priority issue ? **************************************************************** From: Robert Dewar Sent: Friday, November 4, 2011 3:38 PM Right, GNAT detects both as erors, for the second it gives: 1. package Pkg is 2. -- procedure Proc (X : in out String) with 3. -- Post => (for all I in X'Range => X(I) /= X(I)'Old); 4. 5. function Foo return String with 6. Post => Foo'Result /= Foo'Result'Old; | >>> warning: attribute Old applied to constant has no effect 7. end Pkg; **************************************************************** From: Jean-Pierre Rosen Sent: Friday, November 4, 2011 5:07 PM > I think both of the following attribute uses should be illegal: > > package Pkg is > procedure Proc (X : in out String) with > Post => (for all I in X'Range => X(I) /= X(I)'Old); But I hope that X'Old(I) (which is the same thing) is legal... **************************************************************** From: Steve Baird Sent: Friday, November 4, 2011 5:11 PM Yes it is legal, but no it isn't the same thing. **************************************************************** From: Robert Dewar Sent: Friday, November 4, 2011 11:10 PM And of course X'Old (I) works fine in GNAT, though it takes a copy of the whole of X which is a bit wasteful. **************************************************************** From: Jean-Pierre Rosen Sent: Saturday, November 5, 2011 1:03 AM What did I miss? Since I is dynamic, X(I)'Old could be implemented only by saving the whole of X, isn't it? **************************************************************** From: Bob Duff Sent: Saturday, November 5, 2011 5:07 AM X(I)'Old is meaningless. It means "the value of X(I) on entry to this procedure", but that makes no sense, because I didn't exist at that point. X'Old(I) makes sense. **************************************************************** From: Steve Baird Sent: Friday, November 11, 2011 6:22 PM replace 6.1.1 (21/3-22/3) with: X'Old 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, except that if one Old attribute use occurs as part of the prefix of another, then the constant declaration associated with the first use precedes that of the second. Use of this attribute is allowed only within a postcondition expression. The prefix of an Old attribute shall not contain either a Result attribute use or a use of a declaration declared within an enclosing expression but not within the given Old attribute prefix (e.g., the loop parameter of an enclosing quantified expression). **************************************************************** From: Edmond Schonberg Sent: Saturday, November 12, 2011 11:19 AM An expression is potentially unevaluated if it occurs within: o part of an if-expression other than the first condition o any dependent expression of a case expression o the right-hand side of a short-circuit operation o a membership choice other than the first in a membership operation The prefix of an attribute reference Old that is potentially unevaluated shall statically denote an entity. **************************************************************** From: Robert Dewar Sent: Saturday, November 12, 2011 6:11 PM I wonder if it is too restrictive to just say "the prefix of attribute reference Old must statically denote an entity". The special rules above seem horribly complex too me ****************************************************************