Ada Reference Manual (Ada 2022)

7.3.4 Stable Properties of a Type

Certain characteristics of an object of a given type are unchanged by most of the primitive operations of the type. Such characteristics are called stable properties of the type.

Static Semantics

A property function of type T is a function with a single parameter of type T or of a class-wide type that covers T.

A type property aspect definition is a list of names written in the syntax of a positional_array_aggregate. A subprogram property aspect definition is a list of names, each optionally preceded by reserved word not, also written in the syntax of a positional_array_aggregate.

For a nonformal private type, nonformal private extension, or full type that does not have a partial view, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):

Stable_Properties

This aspect shall be specified by a type property aspect definition; each name shall statically denote a single property function of the type. This aspect defines the specific stable property functions of the associated type.

Stable_Properties'Class

This aspect shall be specified by a type property aspect definition; each name shall statically denote a single property function of the type. This aspect defines the class-wide stable property functions of the associated type. Unlike most class-wide aspects, Stable_Properties'Class is not inherited by descendant types and subprograms, but the enhanced class-wide postconditions are inherited in the normal manner.

The specific and class-wide stable properties of a type together comprise the stable properties of the type.

For a primitive subprogram, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):

Stable_Properties

This aspect shall be specified by a subprogram property aspect definition; each name shall statically denote a single property function of a type for which the associated subprogram is primitive.

Stable_Properties'Class

This aspect shall be specified by a subprogram property aspect definition; each name shall statically denote a single property function of a tagged type for which the associated subprogram is primitive. Unlike most class-wide aspects, Stable_Properties'Class is not inherited by descendant subprograms, but the enhanced class-wide postconditions are inherited in the normal manner.

Legality Rules

A stable property function of a type T shall have a nonlimited return type and shall be:

a primitive function with a single parameter of mode in of type T; or

a function that is declared immediately within the declarative region in which an ancestor type of T is declared and has a single parameter of mode in of a class-wide type that covers T.

In a subprogram property aspect definition for a subprogram S:

all or none of the items shall be preceded by not;

any property functions mentioned after not shall be a stable property function of a type for which S is primitive.

If a subprogram_renaming_declaration declares a primitive subprogram of a type T, then the renamed callable entity shall also be a primitive subprogram of type T and the two primitive subprograms shall have the same specific stable property functions and the same class-wide stable property functions (see below).

Static Semantics

For a primitive subprogram S of a type T, the specific stable property functions of S for type T are:

if S has an aspect Stable_Properties specified that does not include not, those functions denoted in the aspect Stable_Properties for S that have a parameter of T or T'Class;

if S has an aspect Stable_Properties specified that includes not, those functions denoted in the aspect Stable_Properties for T, excluding those denoted in the aspect Stable_Properties for S;

if S does not have an aspect Stable_Properties, those functions denoted in the aspect Stable_Properties for T, if any.

A similar definition applies for class-wide stable property functions by replacing aspect Stable_Properties with aspect Stable_Properties'Class in the above definition.

The explicit specific postcondition expression for a subprogram S is the expression directly specified for S with the Post aspect. Similarly, the explicit class-wide postcondition expression for a subprogram S is the expression directly specified for S with the Post'Class aspect.

For a primitive subprogram S of a type T that has a parameter P of type T, the parameter is excluded from stable property checks if:

S is a stable property function of T;

P has mode out;

the Global aspect of S is null, and P has mode in and the mode is not overridden by a global aspect.

For every primitive subprogram S of a type T that is not an abstract subprogram or null procedure, the specific postcondition expression of S is modified to include expressions of the form F(P) = F(P)'Old, all anded with each other and any explicit specific postcondition expression, with one such equality included for each specific stable property function F of S for type T that does not occur in the explicit specific postcondition expression of S, and P is each parameter of S that has type T and is not excluded from stable property checks. The resulting specific postcondition expression of S is used in place of the explicit specific postcondition expression of S when interpreting the meaning of the postcondition as defined in 6.1.1.

For every primitive subprogram S of a type T, the class-wide postcondition expression of S is modified to include expressions of the form F(P) = F(P)'Old, all anded with each other and any explicit class-wide postcondition expression, with one such equality included for each class-wide stable property function F of S for type T that does not occur in any class-wide postcondition expression that applies to S, and P is each parameter of S that has type T and is not excluded from stable property checks. The resulting class-wide postcondition expression of S is used in place of the explicit class-wide postcondition expression of S when interpreting the meaning of the postcondition as defined in 6.1.1.

The equality operation that is used in the aforementioned equality expressions is as described in the case of an individual membership test whose membership_choice is a choice_simple_expression (see 4.5.2).

The Post expression additions described above are enabled or disabled depending on the Post assertion policy that is in effect at the point of declaration of the subprogram S. A similar rule applies to the Post'Class expression additions.

NOTE For an example of the use of these aspects, see the Vector container definition in A.18.2.