AI22-0019-1

!standard 13.1.1(13.1/5)                                      23-06-24  AI22-0019-1/03

!class binding interpretation 21-11-12

!status Corrigendum 1-2022 22-06-23

!status ARG Approved 15-0-0  22-06-23

!status work item 21-11-12

!status received 21-11-09

!priority Low

!difficulty Easy

!qualifier Error

!subject Freezing of aspect specifications

!summary

The circular freezing rule for aspects only applies to aspects that are frozen at the freezing point of the enclosing entity.

!issue

13.1.1(13.1/5) says:

An expression or name that causes freezing of an entity shall not occur within an aspect_specification that specifies a representation or operational aspect of that entity.

Since AI12-0396-1 decided that all aspects are either representation or operational, it's bizarre that we mention both kinds explicitly here. Moreover, the text of AI12-0396-1 says that this rule shouldn't apply to at least some operational aspects. But the wording was unchanged (just moved) from the Corrigendum version.

Is something wrong here? (Yes.)

!recommendation

(See Summary.)

!wording

Replace 13.1.1(13.1/5):

An expression or name that causes freezing of an entity shall not occur within an aspect_specification that specifies a representation or operational aspect of that entity.

with:

If a name or expression within an aspect_specification causes freezing when the entity associated with the aspect_specification is frozen (see 13.14), that name or expression shall not cause freezing of this associated entity.

!discussion

The purpose of 13.1.1(13.1/5) is to prevent a property of an entity (which is necessarily not determined until the entity is frozen) from depending upon the entity itself. That's most important for representation aspects, but could matter for any aspect that is evaluated at the freezing point of the entity.

On the other hand, we definitely do not want 13.1.1(13.1/5) to apply to assertion aspects, which are frozen on use (long after the entity is frozen). It's fine for these to depend on properties of the entity.

There is a fairly complex rule in 13.14 determining which aspects need to be frozen at the freezing point of an entity. We definitely do not want to repeat that in this rule. Therefore, we use the mouthful before the comma in the proposed rewording, to refer to the rules of 13.14(7.2/5).

!example

We need a rule like 13.1.1(13.1/5) to prevent problems for aspects that are evaluated at the freezing point, such as representation aspects. For example:

Freezing Obj freezes My_Int. Freezing My_Int requires Short_Int'Size. Short_Int'Size requires freezing Short_Int. Freezing Short_Int requires freezing My_Int. We're back to where we started, so we will be going in circles. 13.1.1(13.1/5) makes this situation illegal.

On the other hand, aspects that aren't evaluated until some later point, like assertion aspects, do not need such a rule. Consider:

Here, the Default_Initial_Condition is not evaluated until after a default initialized object of type My_Priv is created. My_Priv necessarily will be frozen before that point (perhaps only a little bit before). Thus there is no problem with this expression, and it should be legal. The newly updated version of 13.1.1(13.1/5) makes that the case.

We're not claiming that this particular example is very useful, but other examples could be.

For instance, it might be useful to refer to a subprogram from inside of a precondition or postcondition of that subprogram. For instance, one could write:

We would not want 13.1.1(13.1/5) to make this recursive call illegal. But it would if we required the expression to be frozen before the function could be frozen. We don't need that, as any evaluation of Post would necessarily follow a call on Factorial (which already froze Factorial).

!ACATS test

Any ACATS B-Tests for this rule should be revised with this change in mind (but they probably don't try cases like this anyway).

!appendix

From: Randy Brukardt [privately]

Sent: Tuesday, November 9, 2021  7:00 PM

[Note: This was part of a much larger thread. Only the parts significant

to this question are included here.]

AI12-0396-1's text says that the freezing rule of 13.1(9.1/4) (now moved to

13.1.1(13.1/5)) should not apply to operational aspects, the actual rules in

13.14 separate assertion aspects from other operational aspects.

But the wording of 13.1.1(13.1/5) is the same as the previous wording, saying

"representation or operational aspects" (which is now decided to be all

aspects, so why we call those out that way doesn't make a ton of sense). We

certainly meant to exclude assertion aspects from this rule, and possibly

others as well.

Maybe someone was intending to implicitly drag in the 13.14 rules for freezing

of these expressions, but the existing wording surely doesn't do that (at

least not cleanly). At a minimum, we need an AARM note to explain the model

(once I know what it is ;-).

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

From: Tucker Taft [privately]

Sent: Thursday, November 11, 2021  10:08 AM

13.1.1(13.1/5) does look like confused wording.  I think the point is that for

an aspect specification where (according to 13.14(7.2/5)) all names and

expressions within it cause freezing at the freezing point of the associated

entity, those names and expressions must not be freezing the associated entity

itself.

13.14(7.2/5) says:

At the freezing point of the entity associated with an aspect_specification,

any static expressions within the aspect_specification cause freezing, as do

expressions or names in aspect_definitions for representation aspects, or

operational aspects that have a corresponding operational attribute.

Similarly, if an aspect_definition for an operational aspect, other than

an assertion aspect, could affect the Name Resolution, Static Semantics, or

Legality Rules of a subsequent construct, then any expressions or names

within the aspect_definition cause freezing at the freezing point of the

associated entity. Any static expressions within an aspect_specification

also cause freezing at the end of the immediately enclosing declaration

list. For the purposes of this rule, if there is no declared entity

associated with an aspect_specification, the freezing point is considered

to occur immediately following the aspect_specification.

I would suggest we rewrite 13.1.1(13.1/5), perhaps as follows:

If a name or expression within an aspect_specification causes freezing upon

the freezing of the entity associated with the aspect_specification

(see 13.14), that name or expression shall not be one that causes freezing

of this associated entity.

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