!standard 6.1.1(20/3)                                  19-07-25  AI12-0280-2/05
!standard 6.1.1(21/3)
!standard 6.1.1(22/3)
!standard 6.1.1(22.1/4)
!standard 6.1.1(22.2/5)
!standard 6.1.1(23/3)
!standard 6.1.1(24/3)
!standard 6.1.1(26/4)
!standard 6.1.1(27/5)
!standard 6.1.1(39/5)
!class Amendment 18-05-15
!status Amendment 1-2012 19-09-07
!status work item 18-05-15
!status received 18-05-14
!priority Low
!difficulty Medium
!subject Making 'Old more flexible
!summary

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

Additionally, the requirement to evaluate all 'Old prefixes can be expensive
(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
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 replace the Ada 2012 term "potentially unevaluated" by the new terms
"conditionally evaluated", "unconditionally evaluated", and "repeatedly
evaluated".

We then use those terms 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 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

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
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;

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

  * an Old attribute_reference;

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

  * a selected component of a known-on-entry prefix;

  * an indexed component of a known-on-entry prefix where all index expressions
    are known on entry;

  * a parenthesized 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.

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

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



!corrigendum 6.1.1(20/3)

@drepl
An @fa<expression> is @i<potentially unevaluated> if it occurs within:
@dby
A subexpression of a postcondition expression is @i<known on entry> if it is any
of:

!corrigendum 6.1.1(21/3)

@drepl
@xbullet<any part of an @fa<if_expression> other than the first @fa<condition>;>
@dby
@xbullet<a static subexpression (see 4.9);>

!corrigendum 6.1.1(22/3)

@drepl
@xbullet<a @i<dependent_>@fa<expression> of a @fa<case_expression>;>
@dby
@xbullet<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 @b<null>;>

!corrigendum 6.1.1(22.1/4)

@drepl
@xbullet<the @fa<predicate> of a @fa<quantified_expression>;>
@dby
** See the conflict file **

!corrigendum 6.1.1(23/3)

@drepl
@xbullet<the right operand of a short-circuit control form; or>
@dby
@xbullet<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;>

!corrigendum 6.1.1(24/3)

@drepl
@xbullet<a @fa<membership_choice> other than the first of a membership
operation.>
@dby
@xbullet<For a membership test that is not repeatedly evaluated, a
   subexpression of a @fa<membership_choice> other than the first is
   conditionally evaluated, and its determining expressions include the
   @i<tested_>@fa<simple_expression> and the preceding 
   @fa<membership_choice>s of the
   membership test.>

A conditionally evaluated subexpression is @i<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.

!corrigendum 6.1.1(26/4)

@drepl
@xhang<@xterm<X'Old>
Each X'Old in a postcondition expression that is enabled denotes
a constant that is implicitly declared at the beginning of the
subprogram body, entry body, or accept statement.>
@dby
@xhang<@xterm<X'Old>
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.>


!corrigendum 6.1.1(27/5)

@drepl
@xindent<Reference to this attribute is only allowed within a postcondition
   expression. The @fa<prefix> of an Old @fa<attribute_reference> shall not
   contain a Result @fa<attribute_reference>, nor an Old
   @fa<attribute_reference>, nor a use of an entity declared within the
   postcondition expression but not within @fa<prefix> itself (for example,
   the loop parameter of an enclosing @fa<quantified_expression>). The @fa<prefix>
   of an Old @fa<attribute_reference> that is potentially unevaluated shall
   statically denote an entity.>
@dby
@xindent<Reference to this attribute is only allowed within a postcondition
   expression. The @fa<prefix> of an Old @fa<attribute_reference> shall not
   contain a Result @fa<attribute_reference>, nor an Old
   @fa<attribute_reference>, nor a use of an entity declared within the
   postcondition expression but not within @fa<prefix> itself (for example,
   the loop parameter of an enclosing @fa<quantified_expression>). The @fa<prefix>
   of an Old @fa<attribute_reference> 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.>


!corrigendum 6.1.1(39/5)

@dinsa
For a call via an access-to-subprogram value, all precondition and
postcondition checks performed are determined by the subprogram or entry
denoted by the prefix of the Access attribute reference that produced the
value.
@dinst
@s8<@i<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.


!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 conditionally evaluated 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.]

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

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
also added the new form of case statement. And fixed the literal case.
[This is version /03 of the AI - Editor.]

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

From: Jeff Cousins
Sent: Thursday, July 25, 2019  1:10 PM

The wording includes:

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

Do we really mean expression, or should it be subprogram?  I thought we were
concerned about it changing between subprogram entry and the postcondition,
rather than it changing in the midst of evaluating the postcondition expression.

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

From: Steve Baird
Sent: Thursday, July 25, 2019  1:19 PM

Good point.

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

From: Randy Brukardt
Sent: Friday, July 26, 2019 12:53 AM

Despite Tucker having replaced more than 50% of the AI when he changed the
terminology (he volunteered to do that when Steve was out of commission) -
somehow that paragraph was unchanged. So I applied this fix (along with a number
of other fixes to Tucker's work).

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