CVS difference for ai12s/ai12-0280-2.txt

Differences between 1.1 and version 1.2
Log of other versions for file ai12s/ai12-0280-2.txt

--- ai12s/ai12-0280-2.txt	2018/05/15 23:28:11	1.1
+++ ai12s/ai12-0280-2.txt	2018/05/17 07:43:21	1.2
@@ -1,4 +1,4 @@
-!standard 6.1.1(24/3)                                  18-05-15  AI12-0280-2/01
+!standard 6.1.1(24/3)                                  18-05-16  AI12-0280-2/02
 !standard 6.1.1(26.4/4)
 !standard 6.1.1(39/5)
 !class Amendment 18-05-15
@@ -16,19 +16,19 @@
 !problem
 
 The restrictions on the use of 'Old in potentially unevaluated subexpressions
-can made it hard to properly express complex postconditions, or can make the
+can make it hard to properly express complex postconditions, or can make the
 evaluation of such postconditions expensive (by requiring the saving of a large
 object rather than a single, smaller, part).
 
 Additionally, the requirement to evaluate all 'Old prefixes can be expensive
-(especially if the object is large or has controlled parts), especially if 
+(especially if the object is large or has controlled parts), especially if
 some of them are in mutually exclusive subexpressions of the postcondition.
 
 
 !proposal
 
-We define the term "pre-evalable subexpression" to describe expressions that
-can evaluated at the point of evaluation of 'Old, getting the same value
+We define the term "pre-evaluable subexpression" to describe expressions that
+can be evaluated at the point of evaluation of 'Old, getting the same value
 without side-effects that would be determined when evaluated as part of the
 postcondition expression.
 
@@ -45,10 +45,10 @@
 
 Add after 6.1.1(24/3):
 
-A subexpression of a postcondition expression is *pre-evalable* if it is any
+A subexpression of a postcondition expression is *pre-evaluable* if it is any
 of:
 
-  * a static subexpression (see 4.8);
+  * a static subexpression (see 4.9);
   * a literal;
 
   AARM Reason: We mention literals explicitly in case they are not static (as
@@ -57,89 +57,87 @@
   * a name statically denoting a full constant declaration of a type for which
     all views are constant (see 3.3);
 
-  AARM Ramification: Constants of types with immuntably limited or controlled
+  AARM Ramification: Constants of types with immutably limited or controlled
   parts are not allowed by this rule.
 
-  * a name statically denoting non-aliased /in/ parameter of an elementary
+  * a name statically denoting a non-aliased /in/ parameter of an elementary
     type;
 
   AARM Ramification: All such parameters are by-copy, so the value won't change
   during the execution of the expression.
 
-  * an 'Old attribute_reference;
+  * an Old attribute_reference;
 
   * a predefined operator where all of the operands are pre-evaluable;
 
-  * a function with global = null where all of the operands are pre-evaluable;
+  * a function with Global => null where all of the operands are pre-evaluable;
 
   AARM Reason: Such a function can only depend on the values of its parameters.
 
   * a selected component of a pre-evaluable prefix;
 
   * an indexed component of a pre-evaluable prefix where all index expressions
-    are pre-evalable;
+    are pre-evaluable;
 
-  * a dereference of a pre-evaluable prefix;
+  * a parenthesized pre-evaluable expression;
 
-  * a parenthesized pre-evalable expression;
-
   * a qualified pre-evaluable expression;
 
   * a conditional expression where all of the conditions, selecting_expressions,
-    and dependent_expressions are pre-evalable.
+    and dependent_expressions are pre-evaluable.
 
 AARM Discussion: It's OK if such an expression raises an exception, so long as
 every evaluation of the expression raises the same exception.
 
-If a case_expression is not potentially unevaluated and has a pre-evalable
-selecting_expression, then Nothwithstanding the above:
+If a case_expression is not potentially unevaluated and has a pre-evaluable
+selecting_expression, then nothwithstanding the above:
 
-[We use "nothwithstanding" here to override the basic definition of "potentially
-unevaluable".]
+[We use "notwithstanding" here to override the basic definition of "potentially
+unevaluated".]
   * none of the dependent_expressions are potentially unevaluated;
   * each dependent_expression other than the one selected by the selecting
     expression is *determined to be unevaluated*.
 
 If an if_expression is not potentially unevaluated and all of its conditions
-are pre-evalable, then Nothwithstanding the above:
+are pre-evaluable, then nothwithstanding the above:
   * none of the dependent_expressions are potentially unevaluated;
   * each dependent_expression whose associated condition is False
     is *determined to be unevaluated*;
   * each condition and dependent_expression that follows the first condition
     that evaluates to True is *determined to be unevaluated*.
 
-AARM Reason: We require all of the conditions to be pre-evalable for
+AARM Reason: We require all of the conditions to be pre-evaluable for
 simplicity of description and implementation: either a conditional expression
 has to be pre-evaluated or it does not. If we allowed only the first condition
-to be pre-evalable, we would have a mixture of parts that are and are not
+to be pre-evaluable, we would have a mixture of parts that are and are not
 potentially unevaluated.
 
 If the left operand of a short-circuit control form is pre-evaluable, then
-Nothwithstanding the above:
+nothwithstanding the above:
    * the right operand is not potentially unevaluated;
    * if the left operand is True for an /or else/ form, the right operand
      is *determined to be unevaluated*;
    * if the left operand is False for an /and then/ form, the right operand
      is *determined to be unevaluated*;
 
-AARM Ramification: These rules defining "determined to be unevaluated" are 
-applied recursively; if one of these rules changes (for example) an 
-if_expression that appears as a dependent expression from potentially 
-unevaluated to not potentially unevaluated, then it also is evaluated for 
+AARM Ramification: These rules defining "determined to be unevaluated" are
+applied recursively; if one of these rules changes (for example) an
+if_expression that appears as a dependent expression from potentially
+unevaluated to not potentially unevaluated, then it also is evaluated for
 such a change.
 
 Modify 6.1.1.(26/4):
 
 Each X'Old in a postcondition expression {other than those that occur
-in subexpressions that are determined to be unevaluated} that is enabled 
-denotes a constant that is implicitly declared at the beginning of the 
-subprogram body, entry body, or accept statement. 
+in subexpressions that are determined to be unevaluated} that is enabled
+denotes a constant that is implicitly declared at the beginning of the
+subprogram body, entry body, or accept statement.
 
 AARM Ramification: If X'Old occurs in a subexpression that is determined to be
 unevaluated, then there is no associated constant, and no evaluation of the
 prefix takes place. In general, this will require evaluating one or more
-pre-evalable subexpressions before creating and initializing any X'Old 
-constants. Note that any 'Old in a pre-evalable subexpression evaluated this
+pre-evaluable subexpressions before creating and initializing any X'Old
+constants. Note that any 'Old in a pre-evaluable subexpression evaluated this
 way represents the current value of the prefix (the 'Old itself can be
 ignored).
 
@@ -147,18 +145,18 @@
 
 Implementation Permissions
 
-An implementation may evaluate pre-evalable subexpression of a postcondition 
-expression of an entity at the place where 'Old constants are created for the
+An implementation may evaluate pre-evaluable subexpression of a postcondition
+expression of an entity at the place where X'Old constants are created for the
 entity, with the normal evaluation of the postcondition expression, or both.
 
 AARM Reason: We allow the evaluation of pre-evaluable subexpressions when they
 might be needed to determine whether to create a particular 'Old constant. We
 allow them to be evaluated later as well, or for the results to be saved
 somehow. This permission shouldn't matter, as the results ought to be same
-whereever they are evaluated and there should not be any side-effects. The
+wherever they are evaluated and there should not be any side-effects. The
 main effect of the permission is to determine when any exceptions caused by
 such subexpressions may be raised. We never require waiting to determine the
-value of such subexpressions, even if they aren't used to determine the 
+value of such subexpressions, even if they aren't used to determine the
 creation of a constant for 'Old.
 
 !discussion
@@ -171,16 +169,32 @@
 is.
 
 Rather than introducing a new construct that has the needed properties, we
-instead look to improve the existing desscription of postconditions to better
+instead look to improve the existing description of postconditions to better
 match the sorts of problems that Contract_Cases handles. We do this in two
 parts, first, by changing the evaluation of 'Old to avoid extra evaluations
 and the Legality Rules needed to make those make sense (this AI), and by
 expanding the abilities of case expressions (and statements), in AI12-0214-1
 or AI12-0214-2.
+
+!example
 
----
+Consider:
 
+    procedure Proc (A : access Integer)
+       with Post => (if A /= null then (A.all'Old > 1 and A.all > 1));
 
+In Ada 2012, the reference A.all'Old is illegal as the prefix does not
+statically denote an object (required as the "then" dependent_expression
+is potentially unevaluated).
+
+With the proposed AI, since "A /= null" meets the requirements of a
+pre-evalable expression (A being an in parameter of an elementary type),
+there is no restriction on the use of 'Old, and if A = null, then the 'Old
+reference is not evaluated at all. This allows the author to write the
+postcondition they want with less likelihood of tripping over these rules (and
+as a side-effect, requires less evaluation of 'Old prefixes that are never
+going to be used).
+
 !ASIS
 
 No ASIS effect.
@@ -218,7 +232,7 @@
 
 That would look something like (some details to be worked out):
 
-For a postcondition expression, a subexpression of it is "pre-evalable" if is
+For a postcondition expression, a subexpression of it is "pre-evaluable" if is
 any of:
 
    (1) A declared constant object of a type that doesn't change (see 3.3.1);
@@ -230,7 +244,7 @@
        are pre-evaluable;
 
 For a conditional expression that is not itself potentially unevaluated, if the
-selector expression or all of the conditions are pre-evalable, then the parts of
+selector expression or all of the conditions are pre-evaluable, then the parts of
 the expression are *not* potentially unevaluated. Rather, the selector or
 conditions are evaluated when the subprogram is entered, and only the 'Old
 expressions in the dependent_expression that is selected are evaluated and saved
@@ -248,7 +262,7 @@
 pre-evaluable. And it eliminates overhead for copying objects that will never be
 used.
 
-A compiler could evaluate the pre-evalable expressions at the start of the
+A compiler could evaluate the pre-evaluable expressions at the start of the
 subprogram and somehow save the answers, or it could just evaluate them twice
 (and let the compiler optimizer deal with the duplication - they tend to be good
 at things like that).
@@ -259,5 +273,6 @@
 over...
 
 [The rest of the message pertains to a proposal found in AI12-0214-2 - Editor.]
+
 ****************************************************************
 

Questions? Ask the ACAA Technical Agent