Version 1.6 of ai05s/ai05-0273-1.txt

Unformatted version of ai05s/ai05-0273-1.txt version 1.6
Other versions for file ai05s/ai05-0273-1.txt

!standard 6.1.1(0)          12-02-06 AI05-0273-1/03
!class Amendment 11-11-11
!status Amendment 2012 11-11-12
!status ARG Approved 9-0-0 11-11-12
!status work item 11-11-11
!status received 11-11-04
!priority Low
!difficulty Easy
!subject Problems with the Old attribute
!summary
(1) The prefix of 'Old cannot contain any names that do not exist at the start of the subprogram.
(2) If 'Old occurs in a subexpression that is potentially unevaluated, the prefix of the 'Old reference cannot be dynamic in any way.
!problem
The prefix of the 'Old attribute used in a postcondition is unconditionally evaluated when the subprogram is entered. This causes a number of problems:
(1) If the prefix uses something that doesn't exist when the subprogram is entered, there is a problem:
procedure Proc (X : in out String) with Post => (for all I in X'range => X(I) /= X(I)'Old);
function Foo return String with Post => Foo'Result /= Foo'Result'Old;
(2) If evaluating the prefix would raise an exception, there could be a problem:
Table : array (1..10) of Integer := ... procedure Bar (I : in out Natural) with Post => I > 0 and then Tab(I)'Old = 1;
If I = 0 on entry, the evaluation of Tab(0) will raise Constraint_Error. The "and then" provides no protection because there is no way for the compiler to tell what I is on exit from the subprogram, so it is not known whether the value Tab(I)'Old will be needed when Bar exits. So Tab(I) has to be unconditionally evaluated on entry.
The language actually requires Tab(I) to be evaluated unconditionally even if the compiler can figure out that it is never needed. That makes the problem worse.
!proposal
(See summary.)
!wording
Add before 6.1.1(21/3):
An expression is potentially unevaluated if it occurs within:
* any part of an if_expression other than the first condition; * a dependent_expression of a case_expression; * the right operand of a short-circuit control form; or * a membership_choice other than the first of a membership operation.
Replace 6.1.1(21/3-22/3) with:
X'Old For each X'Old in a postcondition expression that is enabled, a constant is implicitly declared at the beginning of the subprogram or entry. The constant is of the type of X and is initialized to the result of evaluating X (as an expression) at the point of the constant declaration. The value of X'Old in the postcondition expression is the value of this constant; the type of X'Old is the type of X. These implicit constant declarations occur in an arbitrary order.
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 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 denote an entity.
!discussion
We do not allow 'Old in the prefix of another 'Old, as it doesn't add any value:
A(I'Old)'Old
and
A(I)'Old
These have exactly the same semantics: the old (original) value of I is used in both expressions. Having two ways to write the same thing is considered confusioning. Moreover, we would need a rule requiring the I'Old constant to be evaluated before the A(I'Old)'Old constant. This would be an unnecessary complication to the wording and to implementations.
For the second example, the programmer probably meant
procedure Bar (I : in out Natural) with Post => I > 0 and then Tab'Old(I) = 1;
which will not raise Constraint_Error (but does require copying the entire Tab array).
We'll address unneeded evaluation of assertions more generally in AI05-0274-1, so we won't worry about that here.
The solution that we adopted is that any 'Old reference in a subexpression that is not guaranteed to be evaluated must statically denote an entity. In this case, evaluation of the prefix doesn't make any checks and thus cannot fail, so it is OK to make that evaluation unconditionally.
It's almost always possible to change such references to one that would be legal; simply move 'Old to the outermost item (as in the example above). These might cost more by copying a larger object, but they are also much more likely to reflect the actual intent.
We didn't adopt this rule for all 'Old prefixes, as that would make it impossible to write various Old values. Many of the problems aren't all that compelling (a function call would not be allowed, but since significant side-effects are supposed to be avoided, such a call would be equivalent to putting 'Old on the parameter(s)), but there is clearly a performance issue involved, as copying large objects would needed even when only a small component is of interest. (Compilers could sometimes optimize most of these copies away, but that is not possible in general.)
Most compelling is that some postconditions could not be written at all. For instance, consider a variation on the original example:
procedure Bar2 (P : in out Positive) with Post => Tab(P)'Old = 1 or else P > 10;
Here "P" in Tab(P) is really P'Old, and in this example, P can be changed by the subprogram body. Moving the 'Old to Tab (giving Tab'Old(P)) would not necessarily give the same answer, since P could have changed during the execution of the subprogram. Tab(P)'Old is the only (correct) way to write this postcondition.
Thus, rather than throwing the baby out with the bathwater, we only make cases where there is potentially trouble illegal, rather than all of them.
!example
(See problem.)
!corrigendum 6.1.1(0)
Insert new clause:
Force a conflict; the real text is found in the conflict file.
!ACATS Test
ACATS B-Tests should be constructed to check these rules.
!ASIS
No ASIS impact.
!appendix

From: Steve Baird
Sent: Friday, November  4, 2011  3:21 PM

Are we missing some legality checks with respect to the allowable prefix of an
Old attribute?

I think both of the following attribute uses should be illegal:

   package Pkg is
    procedure Proc (X : in out String) with
      Post => (for all I in X'Range => X(I) /= X(I)'Old);

     function Foo return String with
       Post => Foo'Result /= Foo'Result'Old;
   end Pkg;

Do others agree that
   a) they should be illegal
and
   b) these cases are not covered by current RM wording and
   c) this is a very low-priority issue
?

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

From: Robert Dewar
Sent: Friday, November  4, 2011  3:38 PM

Right, GNAT detects both as erors, for the second it gives:

      1.    package Pkg is
      2. --    procedure Proc (X : in out String) with
      3. --      Post => (for all I in X'Range => X(I) /= X(I)'Old);
      4.
      5.      function Foo return String with
      6.        Post => Foo'Result /= Foo'Result'Old;
                                         |
         >>> warning: attribute Old applied to constant has no effect

      7.    end Pkg;

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

From: Jean-Pierre Rosen
Sent: Friday, November  4, 2011  5:07 PM

> I think both of the following attribute uses should be illegal:
>
>   package Pkg is
>    procedure Proc (X : in out String) with
>      Post => (for all I in X'Range => X(I) /= X(I)'Old);

But I hope that X'Old(I) (which is the same thing) is legal...

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

From: Steve Baird
Sent: Friday, November  4, 2011  5:11 PM

Yes it is legal, but no it isn't the same thing.

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

From: Robert Dewar
Sent: Friday, November  4, 2011 11:10 PM

And of course X'Old (I) works fine in GNAT, though it takes a copy of the whole
of X which is a bit wasteful.

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

From: Jean-Pierre Rosen
Sent: Saturday, November  5, 2011  1:03 AM

What did I miss? Since I is dynamic, X(I)'Old could be implemented only by
saving the whole of X, isn't it?

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

From: Bob Duff
Sent: Saturday, November  5, 2011  5:07 AM

X(I)'Old is meaningless.  It means "the value of X(I) on entry to this
procedure", but that makes no sense, because I didn't exist at that point.
X'Old(I) makes sense.

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

From: Steve Baird
Sent: Friday, November 11, 2011  6:22 PM

replace 6.1.1 (21/3-22/3) with:

X'Old
   For each X'Old in a postcondition expression that is enabled, a
   constant is implicitly declared at the beginning of the subprogram
   or entry. The constant is of the type of X and is initialized to the
   result of evaluating X (as an expression) at the point of the constant
   declaration. The value of  X'Old in the postcondition expression is
   the value of this constant; the type  of X'Old is the type of X. These
   implicit constant declarations occur in an arbitrary order, except
   that if one Old attribute use occurs as part of the prefix of another,
   then the constant declaration associated with the first use
   precedes that of the second.

   Use of this attribute is allowed only within a postcondition
   expression. The prefix of an Old attribute shall not
   contain either a Result attribute use or a use of a
   declaration declared within an enclosing expression but not
   within the given Old attribute prefix (e.g., the loop parameter of an
   enclosing quantified expression).

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

From: Edmond Schonberg
Sent: Saturday, November 12, 2011  11:19 AM

An expression is potentially unevaluated if  it occurs within:

o      part of an if-expression other than the first condition

o     any dependent expression of a case expression

o     the right-hand side of a short-circuit operation

o     a membership choice other than the first in a membership operation

The prefix of an attribute reference Old that is potentially unevaluated shall
statically denote an entity.

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

From: Robert Dewar
Sent: Saturday, November 12, 2011  6:11 PM

I wonder if it is too restrictive to just say "the prefix of attribute reference
Old must statically denote an entity".

The special rules above seem horribly complex too me

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

Questions? Ask the ACAA Technical Agent