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

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

--- ai12s/ai12-0280-2.txt	2019/07/19 04:34:42	1.4
+++ ai12s/ai12-0280-2.txt	2019/07/26 04:54:36	1.5
@@ -1,4 +1,4 @@
-!standard 6.1.1(24/3)                                  19-06-15  AI12-0280-2/03
+!standard 6.1.1(24/3)                                  19-07-09  AI12-0280-2/04
 !standard 6.1.1(26.4/4)
 !standard 6.1.1(39/5)
 !class Amendment 18-05-15
@@ -6,16 +6,16 @@
 !status received 18-05-14
 !priority Low
 !difficulty Medium
-!subject Making 'Old more sensible
+!subject Making 'Old more flexible
 !summary
 
-X'Old may be used in a potentially unevaluated subexpression so long as the
+X'Old may be used in a conditionally evaluated subexpression so long as the
 condition controlling the subexpression can be evaluated on entry yielding
 the same result.
 
 !problem
 
-The restrictions on the use of 'Old in potentially unevaluated subexpressions
+The restrictions on the use of 'Old in conditionally evaluated subexpressions
 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).
@@ -24,17 +24,16 @@
 (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 "known on entry 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 known on entry 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,12 +42,13 @@
 
 !wording
 
-Add after 6.1.1(19/3):
+Replace 6.1.1(20/3-24/3) with the following:
 
-A subexpression of a postcondition expression is *known on entry* 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 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;
@@ -70,148 +70,164 @@
   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.
+  (like 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;
 
-  AARM Ramification: All such parameters are by-copy, so the value won't change
-  during the execution of the expression.
+      AARM Ramification: All such parameters are by-copy, so the value
+      won't change during the execution of the expression.
 
   * an Old attribute_reference;
 
-  * a predefined operator where all of the operands are known on entry;
+  * an invocation of a predefined operator where all of the operands are
+    known on entry;
 
   * 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.
+      AARM Reason: Such a function can only depend on the values of its
+      parameters.
 
-  * a selected component of a known on entry prefix;
+  * a selected component of a known-on-entry prefix;
 
-  * an indexed component of a known on entry prefix where all index expressions
+  * an indexed component of a known-on-entry prefix where all index expressions
     are known on entry;
 
-  * a parenthesized known on entry expression;
+  * a parenthesized known-on-entry expression;
 
-  * a qualified expression or type conversion whose operand is a known
-    on entry 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,
     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};
-
-   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.
-
-   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*};
-
-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.]
-
-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 Discussion: It's OK if such an expression raises an
+      exception, so long as every evaluation of the expression raises
+      the same exception.
+
+   A subexpression of a postcondition expression is /unconditionally
+   evaluated/, /conditionally evaluated/, or /repeatedly evaluated/.
+   The following subexpressions are repeatedly evaluated:
+
+    * A subexpression of a predicate of a quantified_expression;
+
+    * A subexpression of the expression of an array_component_association;
+
+    * A subexpression of the expression of an container_element_association.
+
+   If a subexpression is not repeatedly evaluated, and not evaluated
+   unconditionally, then it is /conditionally evaluated/, and there is a
+   set of /determining expressions/ that determine whether the
+   subexpression is actually evaluated at run time. Such subexpressions
+   and their determining expressions are as follows:
+
+    * For an if_expression that is not repeatedly evaluated, a
+      subexpression of any part other than the first condition is
+      conditionally evaluated, and its determining expressions include all
+      conditions of the if_expression that precede the subexpression
+      textually;
+
+    * For a case_expression that is not repeatedly evaluated, a
+      subexpression of any dependent_expression is conditionally
+      evaluated, and its determining expressions include the
+      selecting_expression, or all of the choice_conditions, of the
+      case_expression;
+
+    * For a short-circuit control form that is not repeatedly evaluated,
+      a subexpression of the right-hand operand is conditionally
+      evaluated, and its determining expressions include the left-hand
+      operand of the short-circuit control form;
+
+    * For a membership test that is not repeatedly evaluated, a
+      subexpression of a membership_choice other than the first is
+      conditionally evaluated, and its determining expressions include the
+      tested_simple_expression and the preceding membership_choices of the
+      membership test.
+
+  A conditionally evaluated subexpression is /determined to be
+  unevaluated/ at run time if its set of determining expressions are all
+  known on entry, and when evaluated on entry their values are such that
+  the given subexpression is not evaluated.
+
+    AARM Ramification: To be precise, a conditionally evaluated
+    expression is determined to be unevaluated (including all of
+    its subexpressions) under the following circumstances:
+      * Within an if_expression, a dependent_expression with an
+        associated condition that evaluates to False, or a condition or
+        dependent_expression where a condition of a preceding part
+        of the if_expression evaluates to True;
+      * Within a case_expression, a dependent_expression with a
+        discrete_choice_list that is not covered by the value of the
+        selecting_expression, or has a choice_condition that evaluates to
+        False;
+      * The right-hand operand of a short-circuit control form where the
+        left-hand operand evaluates to False for AND THEN or True for OR
+        ELSE;
+      * A membership_choice of a membership test where the individual
+        membership test defined by any prior membership_choice
+        evaluates to True.
 
 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.
-
-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
-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).
+  Each X'Old in a postcondition expression that is enabled{, other than
+  those that occur in subexpressions that are determined to be
+  unevaluated,} 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 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).}
+
+Modify 6.1.1(27/5):
+
+  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 the prefix itself (for example, the loop parameter of an enclosing
+  quantified_expression). The prefix of an Old attribute_reference
+  [that is potentially unevaluated] shall
+  statically name an entity{, unless the attribute_reference is
+  unconditionally evaluated, or is conditionally evaluated where all of
+  the determining expressions are known on entry}.
+
+    {AARM Ramification: The prefix of an Old attribute_reference has to
+    statically name an entity if it appears within a repeatedly
+    evaluated expression.}
 
 Add after 6.1.1(39/5):
 
-Implementation Permissions
+  Implementation Permissions
 
-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 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
-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
-creation of a constant for 'Old.
+  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 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 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 creation of
+  a constant for 'Old.
 
 !discussion
 
-This proposal addresses some of the same problems that the Contract_Cases
-aspect does. Contract_Cases is not a good fit for Ada since it really requires
-a complex static check that its alternatives cover the precondition (provided
-by SPARK and GNATProve). Without such a check, it modifies the precondition,
-making it difficult for the caller to be sure what the precondition actually
+This proposal addresses some of the same problems that the proposed
+Contract_Cases aspect does (see AI12-0280-1). Contract_Cases is not a
+great fit for Ada since it potentially requires a complex static check
+that its alternatives cover the precondition (provided by SPARK and
+GNATProve). Without such a check, it modifies the precondition, making
+it difficult for the caller to be sure what the precondition actually
 is.
 
 Rather than introducing a new construct that has the needed properties, we
@@ -230,10 +246,10 @@
 
 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).
+is conditionally evaluated).
 
 With the proposed AI, since "A /= null" meets the requirements of a
-known on entry 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
@@ -248,7 +264,7 @@
 
 ACATS C-Tests are needed to check that the new capabilities are
 supported, specifically that (A) the restriction on 'Old prefixes is not
-enforced on a dependent expression that is not potentially unevaluated by
+enforced on a dependent expression that is not conditionally evaluated by
 these rules; (B) that the prefix of 'Old is not evaluated when it is
 determined to be unevaluated.
 
@@ -324,7 +340,7 @@
 From: Randy Brukardt
 Sent: Saturday, June 15, 2019  9:06 AM
 
-I got rid of the notwithstandings as requested, it actually isn't too bad. I 
+I got rid of the notwithstandings as requested, it actually isn't too bad. I
 also added the new form of case statement. And fixed the literal case.
 [This is version /03 of the AI - Editor.]
 

Questions? Ask the ACAA Technical Agent