CVS difference for ai05s/ai05-0273-1.txt

--- ai05s/ai05-0273-1.txt	2011/12/23 04:18:40	1.2
+++ ai05s/ai05-0273-1.txt	2011/12/23 05:22:38	1.3
@@ -1,5 +1,7 @@
-!standard  6.1.1(0)                              11-11-11    AI05-0273-1/01
+!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
@@ -49,6 +51,15 @@
 
 !wording
 
+Add before 6.1.1(21/3):
+
+A subexpression 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
@@ -63,9 +74,8 @@
 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) **
+quantified_expression). The prefix of an Old attribute_reference that is potentially
+unevaluated shall statically denote an entity.
 
 !discussion
 
@@ -98,6 +108,30 @@
 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