Version 1.1 of ai05s/ai05-0273-1.txt
!standard 13.12.1(6/2) 11-11-11 AI05-0273-1/00
!standard 13.12.1(7/2)
!standard 2.8(10)
!standard H.4(24)
!class Amendment 11-11-11
!status work item 11-11-11
!status received 11-11-04
!priority Low
!difficulty Easy
!subject Problems with the Old attribute
!summary
!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
** TBD.
!wording
** TBD.
!discussion
In 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).
!example
!ACATS Test
!ASIS
!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