CVS difference for ai05s/ai05-0273-1.txt
--- ai05s/ai05-0273-1.txt 2011/12/22 08:20:30 1.1
+++ ai05s/ai05-0273-1.txt 2011/12/23 04:18:40 1.2
@@ -1,7 +1,4 @@
-!standard 13.12.1(6/2) 11-11-11 AI05-0273-1/00
+!standard 6.1.1(0) 11-11-11 AI05-0273-1/01
!class Amendment 11-11-11
!status work item 11-11-11
!status received 11-11-04
@@ -11,8 +8,13 @@
+(1) The prefix of 'Old cannot contain any names that do not exist at the start of the
+(2) If 'Old occurs in a subexpression that is potentially unevaluated, the prefix of
+the 'Old reference cannot be dynamic in any way.
The prefix of the 'Old attribute used in a postcondition is unconditionally evaluated
@@ -21,17 +23,17 @@
(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);
+ 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;
+ 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;
+ 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
@@ -43,29 +45,74 @@
+Replace 6.1.1(21/3-22/3) with:
+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
+** TBD: Wording for (2) **
+We do not allow 'Old in the prefix of another 'Old, as it doesn't add any value:
+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.
-In the second example, the programmer probably meant
+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
+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.
+Force a conflict; the real text is found in the conflict file.
+ACATS B-Tests should be constructed to check these rules.
Questions? Ask the ACAA Technical Agent