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  13.12.1(7/2)
-!standard  2.8(10)
-!standard  H.4(24)
+!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 @@
 
 !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
@@ -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 @@
 
 !proposal
 
-** TBD.
+(See summary.)
 
 !wording
+
+Replace 6.1.1(21/3-22/3) with:
 
-** TBD.
+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).
 
+** TBD: Wording for (2) **
+
 !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.
 
-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
+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.
 
 !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