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
