AI22-0145-1

!standard 6.1.1(25/3)                                    25-12-16  AI22-0145-1/02

!class Binding Interpretation 25-11-23

!status Revision-202Y  25-12-16

!status ARG Approved  8-1-0  25-12-11

!status work item 25-11-23

!status received 24-04-04

!assigned author Tucker Taft

!submitter Tucker Taft

!priority Medium

!difficulty Easy

!qualifier Omission

!subject 'Old should work on values as well as objects

!summary

The Old attribute is now allowed for values as well as objects.

!issue

Currently the Old attribute is restricted by 6.1.1(25/3) to be applied to objects:

 For a prefix X that denotes an object of a nonlimited type, the following attribute is defined:

X'Old

This restriction seems unnecessary. For example, it might make sense to refer to Arr_Ptr'Length'Old if Arr_Ptr might be altered to point to a different length array.

Should we permit a name that denotes a value rather than an object as a prefix for 'Old? (Yes.)

!recommendation

The wording in 6.1.1 should be modified to allow any name that denotes an object or value of a nonlimited type.

!wording

Modify 6.1.1(25/3):

For a prefix X that denotes an object{ or value} of a nonlimited type, the following attribute is defined:

Modify 6.1.1(27.a/3)

Discussion: The prefix X can be any nonlimited object{ or value} that obeys the syntax for prefix other than the few exceptions given above (discussed below). Useful cases are: the name of a formal parameter of mode [in] out, the name of a global variable updated by the subprogram, a function call passing those as parameters, a subcomponent of those things, etc.

!discussion

We recently allowed "object" renaming to rename values, so this is continuing the path of minimizing the distinction between objects and values.

!example

The Length attribute is the simplest example of an interesting nameable "value", and it is clearly something which might be appropriate in a postcondition:

procedure Grow (A : in out String_Ptr)
  with Post => A'Length >= A'Length'Old;

!corrigendum 6.1.1(25/3)

@drepl

For a @fa{prefix} X that denotes an object of a nonlimited type, the following attribute is defined:

@dby

For a @fa{prefix} X that denotes an object or value of a nonlimited type, the following attribute is defined:

!ACATS test

This is an extension to the current rules, so a C-Test is needed that would verify that it works correctly when a value is denoted by the prefix. Existing B-Tests should be examined to ensure that they are not requiring values to be rejected as the prefix of ‘Old.

!appendix

This is based on ARG GitHub Issue #92.