7.3.4 Stable Properties of a Type
{
AI12-0187-1}
{
AI12-0324-1}
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.
Glossary entry: A characteristic associated
with objects of a given type that is preserved by many of the primitive
operations of the type.
Static Semantics
{
AI12-0187-1}
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.
Reason: This provides restrictions on
name resolution so overloaded functions can be used as a stable property
function.
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.
Discussion: We do not allow this aspect
on generic formal types, as it is only meaningful for primitive subprograms
and generic formal types have no such subprograms.
Ramification: Class-wide aspects are
only allowed on tagged types (see
13.1.1),
so we don't say that here.
Aspect Description for Stable_Properties:
A list of functions describing characteristics that usually are unchanged
by primitive operations of the type or an individual primitive subprogram.
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.]
Proof: Class-wide inheritance has to
be explicitly defined. Here we are not making such a definition, so there
is no inheritance.
6.1.1 defines the inheritance
of class-wide postconditions.
Discussion: Since class-wide postconditions
are inherited by descendants, we don't need the stable property functions
to be inherited; if they were inherited, we'd be duplicating the checks,
which we don't want.
Ramification: Class-wide aspects are
only allowed on primitive subprograms of tagged types (see
13.1.1),
so we don't say that here.
Aspect Description for Stable_Properties'Class:
A list of functions describing characteristics that usually are unchanged
by primitive operations of a class of types or a primitive subprogram
for such a class.
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.
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.]
Reason: The subprogram versions of Stable_Properties
are provided to allow overriding the stable properties of a type for
an individual primitive subprogram. While they can be used even if the
type has no stable properties, that is not an intended use (as simply
modifying the postcondition directly makes more sense for something that
only happens in one place).
Legality Rules
{
AI12-0187-1}
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.
all or none of the items shall be preceded by not;
Ramification: Mixing not functions
with regular functions is not allowed.
any property functions mentioned after not
shall be a stable property function of a type for which S is primitive.
Static Semantics
{
AI12-0187-1}
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.
Discussion: A primitive subprogram can
be primitive for more than one type, and thus there can be more than
one such set of stable properties for a subprogram. Thus we say “stable
property functions for subprogram S for type T”.
{
AI12-0187-1}
A similar definition applies for class-wide stable property functions
by replacing aspect Stable_Properties with aspect Stable_Properties'Class
in the above definition.
{
AI12-0187-1}
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.
{
AI12-0187-1}
{
AI12-0324-1}
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].
Ramification: There is one F(P) =
F(P)'Old subexpression for every combination of a stable expression
function of type T and a parameter of type T. For instance,
if there are three stable property functions for type T and two
parameters of type T, then there are six such subexpressions appended
to the postcondition.
The resulting specific postcondition is evaluated
as described in
6.1.1. One hopes that compilers
can be smart enough to prove that many of these added postcondition subexpressions
cannot fail, but that is not required here.
{
AI12-0187-1}
{
AI12-0324-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].
Reason: We suppress stable property expressions
if the property function appears in the explicit class-wide postcondition,
or in any inherited class-wide postconditions. If we didn't do that,
we could have conflicting requirements in an inherited postcondition
and the current one. We also avoid redundant property checks.
Ramification: The resulting class-wide
postcondition is evaluated as described in
6.1.1.
In particular, the enhanced class-wide postcondition
is the class-wide
postcondition for
S, and therefore inherited postconditions include
any stable property expressions for
S.
15 {
AI12-0112-1}
For an example of the use of these aspects, see the Vector container
definition in
A.18.2.
Extensions to Ada 2012
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe