Version 1.6 of ai12s/ai12-0422-1.txt

!standard 3.3(13/3) 21-01-21 AI12-0422-1/03
!standard 6.1.1(22.1/5)
!standard 6.1.2(10/5)
!class Amendment 21-01-14
!status Amendment 1-2012 21-01-21
!status ARG Approved 16-0-0 21-01-20
!status work item 21-01-14
!status received 21-01-14
!priority Low
!difficulty Easy
!subject When is a constant known-on-entry?

The notion of "known to have no variable views" is defined, and used in several rules.

There are two issues with 6.1.1(22.1/5).

First, this rule is about a constant "for which all views are constant" and then references 3.3. Is the definition in 3.3 right? It seems to suggest that an object "for which all views are constant" can have a controlled subcomponent, which is wrong.

Second, even if that was correct, it seems to require breaking privacy to check this rule. If a component has a private type, and the full type has a controlled component, then certainly a variable view of a part of the object exists. That is what we're trying to avoid depending on. But this definition is eventually used in a Legality Rule, so breaking privacy should be a last resort.

Add after 3.3(13/3):

AARM Ramification: If some part of an object has a variable view, then the object as a whole has a variable view, and not all views of the object are constant. That's true even if only a subcomponent has a variable view.

Also add after 3.3(13/3):

A constant object is /known to have no variable views/ if it does not have a part that is immutably limited, or of a controlled type, private type, or private extension.

AARM Reason: This definition can be used in Legality Rules as it respects privacy. It is an assume-the-worst rule, as all private types and private extensions might have a controlled component.

Modify 6.1.1(22.1/5):

* a name statically denoting a full constant declaration [of a type for

The Global aspect identifies the set of variables (which, for the purposes of this clause{,} includes all constants {except those which are known to have no variable views (see 3.3)}[with some part being immutably limited, or of a controlled type, private type, or private extension]) that are global to a callable entity or task body, and that are read or updated as part of the execution of the callable entity or task body. If specified for a protected unit, it refers to all of the protected operations of the protected unit. Constants of any type may also be mentioned in a Global aspect.

We do not try to prevent the possible misreading of 3.3(13/3) noted in the question. Rather, we add an AARM note to clarify the meaning when a subcomponent may have a variable view.

If we did not either assume-the-worst or look into private types, we could have a "constant" whose value changes during a period of interest. A value which could be changed cannot be "known on entry", and it needs to be covered by a Global aspect.

It seemed best to add a term to describe the "assume-the-worst" list of items that potentially could have a variable view of a part of a constant object. Repeating that list in each rule just makes it more likely to make a mistake, and it will simplify writing any similar rules in the future.

An object is either a constant object or a variable object. Similarly, a view of an object is either a constant or a variable. All views of a constant elementary object are constant. All views of a constant composite object are constant, except for parts that are of controlled or immutably limited types; variable views of those parts and their subcomponents may exist. In this sense, objects of controlled and immutably limited types are inherently mutable. A constant view of an object cannot be used to modify its value. The terms constant and variable by themselves refer to constant and variable views of objects.

A constant object is known to have no variable views if it does not have a part that is immutably limited, or of a controlled type, private type, or private extension.

See the conflict file for the changes.

No separate ACATS tests ought to be needed. One could imagine a B-Test that uses an indexing of a constant array object with a component of a private type as the prefix of 'Old. The test would check that a dynamic index of the array is not allowed when the reference is conditionally evaluated. But this seems of low value as it is rather unlikely.