AI22-0038-1

!standard 7.3.2(1/5)                                  22-06-23  AI22-0038-1/04

!class presentation 22-02-04

!status Corrigendum 1-2022 22-06-23

!status WG9 Approved 22-10-18

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

!status work item 22-02-04

!status received 21-05-20

!priority Low

!difficulty Easy

!subject Introduction to 7.3.2

!summary

An introduction to 7.3.2 is added.

!question

[WG 9 comment #148] It would help readers if the intro of 7.3.2 were to

explain that the aim of the Type_Invariant('Class) feature is to ensure that

any object of this type/class satisfies the invariant when inspected or used

by a client of the defining package, but the invariant does not have to be

satisfied at each point within the operations of the defining package itself

(where the full type declaration is visible). Therefore, the invariant is

checked at the boundary between the defining package and its clients.

Should an introduction be added? (Yes.)

!recommendation

(See Summary.)

!wording

Add before 7.3.2(1/5):

A type invariant for a given private type is an assertion that is expected to be true about every object of the type, except when such an object is in the middle of an operation that has visibility on the representation of its full type. The type invariant is enforced much like a postcondition, including when such an object completes default initialization, or upon return from an externally callable subprogram that might update the object and has visibility on the full type.

!discussion

Most subclauses have some sort of introduction, it's unusual that this one does not.

!corrigendum 7.3.2(1/5)

@dinsb

For a private type, private extension, or interface, the following language-defined assertion aspects may be specified with an @fa{aspect_specification} (see 13.1.1):

@dinst

A type invariant for a given private type is an assertion that is expected to be true about every object of the type, except when such an object is in the middle of an operation that has visibility on the representation of its full type. The type invariant is enforced much like a postcondition, including when such an object completes default initialization, or upon return from an externally callable subprogram that might update the object and has visibility on the full type.

!ACATS test

No tests are needed for presentation changes.

!appendix

From: Niklas Holsti

WG 9 Review issue #148 - May 20, 2021

[Comment on 7.3.2.]

It might help readers if the intro were to explain that the aim of the

Type_Invariant('Class) feature is to ensure that any object of this type/class

satisfies the invariant when inspected or used by a client of the defining

package, but the invariant does not have to be satisfied at each point within

the operations of the defining package itself (where the full type declaration

is visible). Therefore, the invariant is checked at the boundary between the

defining package and its clients. Similar text is now in the Ramification

RM 7.3.2 (23.a/5), but that is quite late in the section and is not visible

in the non-annotated RM.

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

From: Randy Brukardt

WG 9 Review issue #148 - May 21, 2021

This makes sense, but since the existing text (of which there is none!) is

neither new nor wrong, this is out of bounds for this review. As such, it will

be deferred.

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