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.
Term entry: stable property —
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
specific 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.
{
AI12-0405-1}
The specific and class-wide stable properties of a type together comprise
the stable properties of the type.
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 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.
{
AI12-0405-1}
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
{
AI12-0187-1}
For a primitive subprogram
S of a type
T, the specific
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 specific stable properties for a subprogram. Thus we
say “specific 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}
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:
S is a stable property function of T;
Reason: This prevents possible infinite
recursion, where the postcondition calls the function itself (directly
or indirectly).
P has mode out;
Reason: A parameter of mode out
doesn't necessarily have a defined input value, so there is no old value
to compare with. Ideally, the postcondition will include expressions
defining the values of the stable properties after the call, but we do
not try to ensure this.
the Global aspect of S is null, and
P has mode in and the mode is not overridden by a global
aspect.
Reason: An in parameter of a Global
=> null subprogram cannot be modified, even if it has indirect
parts, without violating the Global aspect. Thus, there is no need to
assert that the properties don't change.
{
AI12-0187-1}
{
AI12-0324-1}
{
AI12-0405-1}
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].
Ramification: There is one F(P) =
F(P)'Old subexpression for every combination of a specific stable
property function of type T and a parameter of type T.
For instance, if there are three specific 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.
Reason: Null procedures and abstract
subprograms are excluded as they do not allow specific postconditions.
Moreover, for null procedures, static analysis tools can be certain that
their parameters aren't modified so there is no need to assert that the
properties don't change. Abstract subprograms cannot be directly called.
{
AI12-0187-1}
{
AI12-0324-1}
{
AI12-0405-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].
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.
{
AI12-0405-1}
In the case of a derived type
T, when the preceding rules refer
to “every primitive subprogram
S of a type
T”,
the referenced set of subprograms includes any inherited subprograms.
{
AI12-0405-1}
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.
NOTE {
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
