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.

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):

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):

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

In a subprogram property aspect definition for a subprogram S:

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).

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

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:

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.