Ada Reference Manual (Ada 2022) — Legal Information

# 7.3.4 Stable Properties of a Type

1/5
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

2/5
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.
3/5
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.
4/5
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):
5/5
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.
6/5
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.
7/5
The specific and class-wide stable properties of a type together comprise the stable properties of the type.
8/5
For a primitive subprogram, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
9/5
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.
10/5
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

11/5
A stable property function of a type T shall have a nonlimited return type and shall be:
12/5
a primitive function with a single parameter of mode in of type T; or
13/5
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.
14/5
In a subprogram property aspect definition for a subprogram S:
15/5
all or none of the items shall be preceded by not;
16/5
any property functions mentioned after not shall be a stable property function of a type for which S is primitive.
17/5
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

18/5
For a primitive subprogram S of a type T, the specific stable property functions of S for type T are:
19/5
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;
20/5
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;
21/5
if S does not have an aspect Stable_Properties, those functions denoted in the aspect Stable_Properties for T, if any.
22/5
A similar definition applies for class-wide stable property functions by replacing aspect Stable_Properties with aspect Stable_Properties'Class in the above definition.
23/5
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.
24/5
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:
25/5
S is a stable property function of T;
26/5
P has mode out;
27/5
the Global aspect of S is null, and P has mode in and the mode is not overridden by a global aspect.
28/5
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.
29/5
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.
30/5
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).
31/5
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.
32/5
NOTE For an example of the use of these aspects, see the Vector container definition in A.18.2.

Ada 2005 and 2012 Editions sponsored in part by Ada-Europe