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.
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
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.
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 (including a class-wide stable property function)
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.
Static Semantics
For a primitive subprogram
S of a type T, the 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 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.
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.
15 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