Ada Reference Manual (Ada 202x Draft 25)Legal Information
Contents   Index   References   Search   Previous   Next 

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 preceded by an optional 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 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
For a primitive subprogram, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
8/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.
9/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

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

Static Semantics

16/5
For a primitive subprogram S of a type T, the stable property functions of S for type T are:
17/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;
18/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;
19/5
if S does not have an aspect Stable_Properties, those functions denoted in the aspect Stable_Properties for T, if any.
20/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.
21/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.
22/5
For every primitive subprogram S of a type T that is not a stable property function of T, 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 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. 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.
23/5
For every primitive subprogram S of a type T that is not a stable property function of 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. 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.
NOTES
24/5
15  For an example of the use of these aspects, see the Vector container definition in A.18.2.

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe