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

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

--- ai12s/ai12-0280-2.txt	2018/05/17 07:43:21	1.2
+++ ai12s/ai12-0280-2.txt	2019/07/05 22:05:28	1.3
@@ -1,4 +1,4 @@
-!standard 6.1.1(24/3)                                  18-05-16  AI12-0280-2/02
+!standard 6.1.1(24/3)                                  19-06-15  AI12-0280-2/03
 !standard 6.1.1(26.4/4)
 !standard 6.1.1(39/5)
 !class Amendment 18-05-15
@@ -9,9 +9,9 @@
 !subject Making 'Old more sensible
 !summary
 
-For X'Old in a postcondition, X is not evaluated when the subprogram is
-entered if it is possible to tell that X'Old will not be needed to evaluate
-the postcondition.
+X'Old may be used in a potentially unevaluated subexpression so long as the
+condition controlling the subexpression can be evaluated on entry yielding
+the same result.
 
 !problem
 
@@ -21,20 +21,20 @@
 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
+(for example, 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-evaluable subexpression" to describe expressions that
+We define the term "known on entry 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.
 
 We then use that to define the term "determined to be unevaluated" to be used
 on subexpressions in a postcondition that are not going to evaluated given
-the value of the pre-evaluable subexpression. (Note: which subexpressions
+the value of the known on entry subexpression. (Note: which subexpressions
 are determined to be unevaluated is calculated at runtime; this term is
 referring to a Dynamic Semantics property.)
 
@@ -43,23 +43,36 @@
 
 !wording
 
-Add after 6.1.1(24/3):
+Add after 6.1.1(19/3):
 
-A subexpression of a postcondition expression is *pre-evaluable* if it is any
+A subexpression of a postcondition expression is *known on entry* if it is any
 of:
 
   * a static subexpression (see 4.9);
-  * a literal;
+  * a literal whose type does not have any Integer_Literal, Real_Literal, or
+    String_Literal aspect specified, or, the function specified by such an
+    attribute has aspect Global specified to be null;
 
   AARM Reason: We mention literals explicitly in case they are not static (as
-  when their subtype is not static, they are the literal null, etc.).
+  when their subtype is not static, they are the literal null, etc.). We exclude
+  literals of types with the aspects that are not Global => null those cause a
+  user-written subprogram with possible side-effects to be called.
 
   * 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 immutably limited or controlled
-  parts are not allowed by this rule.
+  parts are not allowed by this rule. Generic formal in objects are allowed by
+  this rule (as they are defined to be full constant declarations).
 
+  AARM Reason: We only want things that cannot be changed. We can't just say
+  "constant" since that includes views of variables in some cases (for
+  instance, a dereference of an access to constant object can be a view of a
+  variable). There are other things we could have allowed (like a loop
+  parameter), but having a subprogram declaration where those could be used
+  (for instance, inside of a loop) seems unusual enough to not be worth
+  defining.
+
   * a name statically denoting a non-aliased /in/ parameter of an elementary
     type;
 
@@ -68,64 +81,97 @@
 
   * an Old attribute_reference;
 
-  * a predefined operator where all of the operands are pre-evaluable;
+  * a predefined operator where all of the operands are known on entry;
 
-  * a function with Global => null where all of the operands are pre-evaluable;
+  * a function call where the function has aspect Global => null where all
+    of the actual parameters are known on entry;
 
   AARM Reason: Such a function can only depend on the values of its parameters.
 
-  * a selected component of a pre-evaluable prefix;
+  * a selected component of a known on entry prefix;
 
-  * an indexed component of a pre-evaluable prefix where all index expressions
-    are pre-evaluable;
+  * an indexed component of a known on entry prefix where all index expressions
+    are known on entry;
 
-  * a parenthesized pre-evaluable expression;
+  * a parenthesized known on entry expression;
 
-  * a qualified pre-evaluable expression;
+  * a qualified expression or type conversion whose operand is a known
+    on entry expression;
 
   * a conditional expression where all of the conditions, selecting_expressions,
-    and dependent_expressions are pre-evaluable.
+    choice_conditions, and dependent_expressions are known on entry.
 
 AARM Discussion: It's OK if such an expression raises an exception, so long as
 every evaluation of the expression raises the same exception.
+
+Add before 6.1.1(20/3):
+A subexpression of a postcondition is always evaluated if it is not potentially
+unevaluated. ...
+
+Modify 6.1.1(21/3):
+
+ * any part of an if_expression other than the first condition{, unless all of
+   the conditions are known on entry and then entire if_expression is always
+   evaluated};
+
+   AARM Ramification: If all of the conditions are known on entry, none of
+   the dependent_expressions or conditions are potentially unevaluated.
+
+   AARM Reason: We require all of the conditions to be known on entry for
+   simplicity of description and implementation: either a conditional expression
+   has to be known on entry or it does not. If we allowed only the first
+   condition to be known on entry, we would have a mixture of parts that are and
+   are not potentially unevaluated. That's possible but difficult to describe.
+
+Modify 6.1.1(22/3):
+
+ * a dependent_expression of a case_expression{, unless the
+   selecting_expression or all of the choice_conditions are
+   known on entry and the entire case_expression is not
+   potentially unevaluated};
 
-If a case_expression is not potentially unevaluated and has a pre-evaluable
-selecting_expression, then nothwithstanding the above:
+   AARM Ramification: If the selecting_expression is known on entry,
+   or all of the choice_conditions are known on entry, none of the
+   dependent_expressions are potentially unevaluated.
 
-[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-evaluable, then nothwithstanding the above:
-  * none of the dependent_expressions are potentially unevaluated;
+   AARM Reason: We require all of the choice_conditions to be known on
+   entry as a case_expression without a selecting_expression requires
+   exactly one to be true. A mix could cause whether the expression raises
+   an exception to change.
+
+[Author's note: See AI12-0214-2 for choice conditions.]
+
+Modify 6.1.1(23/3):
+
+ * the right operand of a short-circuit form{, unless the left operand
+   is known on entry and the entire short-circuit form is always evaluated};
+
+Add after 6.1.1(24/3): [Author's Note: These following rules are talking
+about a dynamic condition; this is all lumped together here in 6.1.1.]
+
+If an if_expression is always evaluated and all of its conditions
+are known on entry, then:
   * 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*.
+    that evaluates to True is *determined to be unevaluated*};
+
+If a case_expression with a selecting_expression is always evaluated and has a
+known on entry selecting_expression, then each dependent_expression other than
+the one selected by the selecting expression is *determined to be unevaluated*.
+
+If a case_expression without a selecting_expression is always evaluated and all
+of the choice_conditions are known on entry, then each dependent_expression
+other than the one corresponding to the (single) choice_condition that evaluated
+to True is *determined to be unevaluated*. [Author's note: See AI12-0214-2.]
 
-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-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:
-   * the right operand is not potentially unevaluated;
+If a short-circuit form is always evaluated and the left
+operand of the form is known on entry, then:
    * 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
-such a change.
-
 Modify 6.1.1.(26/4):
 
 Each X'Old in a postcondition expression {other than those that occur
@@ -136,8 +182,8 @@
 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-evaluable subexpressions before creating and initializing any X'Old
-constants. Note that any 'Old in a pre-evaluable subexpression evaluated this
+known on entry subexpressions before creating and initializing any X'Old
+constants. Note that any 'Old in a known on entry subexpression evaluated this
 way represents the current value of the prefix (the 'Old itself can be
 ignored).
 
@@ -145,11 +191,11 @@
 
 Implementation Permissions
 
-An implementation may evaluate pre-evaluable subexpression of a postcondition
+An implementation may evaluate known on entry 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
+AARM Reason: We allow the evaluation of known on entry 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
@@ -173,8 +219,7 @@
 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.
+expanding the abilities of case expressions (and statements), in AI12-0214-2.
 
 !example
 
@@ -188,7 +233,7 @@
 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),
+known on entry 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

Questions? Ask the ACAA Technical Agent