Version 1.2 of ai12s/ai12-0280-2.txt

Unformatted version of ai12s/ai12-0280-2.txt version 1.2
Other versions for file ai12s/ai12-0280-2.txt

!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
!status work item 18-05-15
!status received 18-05-14
!priority Low
!difficulty Medium
!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.
!problem
The restrictions on the use of 'Old in potentially unevaluated 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).
Additionally, the requirement to evaluate all 'Old prefixes can be expensive (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-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.
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 are determined to be unevaluated is calculated at runtime; this term is referring to a Dynamic Semantics property.)
Finally, we use the above terms to define when parts of the postcondition are evaluated and when the prefix of Old attribute references is not evaluated.
!wording
Add after 6.1.1(24/3):
A subexpression of a postcondition expression is pre-evaluable if it is any of:
* a static subexpression (see 4.9);
* a literal;
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.).
* 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.
* 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;
* a predefined operator 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-evaluable;
* a parenthesized pre-evaluable expression;
* a qualified pre-evaluable expression;
* a conditional expression where all of the conditions, selecting_expressions, 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-evaluable selecting_expression, then nothwithstanding the above:
[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;
* 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-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 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 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-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).
Add after 6.1.1(39/5):
Implementation Permissions
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 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 is.
Rather than introducing a new construct that has the needed properties, we 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.
!ACATS test
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 these rules; (B) that the prefix of 'Old is not evaluated when it is determined to be unevaluated.
!appendix

From: Randy Brukardt
Sent: Saturday, April 14, 2018  7:22 PM

...
> Alternative proposals are always of interest, but (as I'm sure you'd
> agree) ya gotta give me something more concrete than that.

I had an idea when I woke up this morning. So here's a quick outline of the
ideas (two).

---------

For the 'Old evaluation problem:

The basic issue is that in general, the value of conditionals aren't known at
the start of the subprogram, so we have to unconditionally evaluate 'Old
prefixes. Obviously, there is a subset where it *is* possible to know. In that
case, we don't need to evaluate 'Old unconditionally, and we can drop the
restrictions.

That would look something like (some details to be worked out):

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);
   (2) A literal;
   (3) An in parameter of a by-copy type;
   (4) An 'Old attribute_reference;
   (5) A predefined operator where all of the operands are pre-evaluable;
   (6) A function with global = null ("pure function") where all of the operands
       are pre-evaluable;

For a conditional expression that is not itself potentially unevaluated, if the
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
in the normal manner. (This needs a bit of wording improvement to properly
evaluate if conditions only if the preceding ones are False, but I hope you get
the idea.) We might want a term to describe this kind of expression.

We probably would want to do something similar for short circuit forms.

The rule would be applied recursively (for nested if statements could be subject
to it).

This eliminates the "potentially unevaluated" checks for whatever part of the
postcondition can be pre-evaluated -- one only needs to make the conditions
pre-evaluable. And it eliminates overhead for copying objects that will never be
used.

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).

The advantage we have over SPARK here is that we (the ARG) can get rid of the
Legality Rules in the existing construct, whereas for SPARK to do that, they
have to invent a new construct. It's better to file down the bump than to start
over...

[The rest of the message pertains to a proposal found in AI12-0214-2 - Editor.]

****************************************************************


Questions? Ask the ACAA Technical Agent