Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
 
Annotated 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
{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.
1.a.1/5
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

2/5
{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.
2.a/5
Reason: This provides restrictions on name resolution so overloaded functions can be used as a stable property function. 
3/5
{AI12-0285-1} {AI12-0324-1} 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.
3.a/5
To be honest: A single name would technically be a parenthesized expression rather than an aggregate; we mean to include that here. We say "syntax of a positional_array_aggregate" to hopefully clarify that the specification is in no other way an actual aggregate.
4/5
{AI12-0187-1} {AI12-0272-1} 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
{AI12-0187-1} {AI12-0285-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.
5.a/5
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.
5.b/5
Ramification: Class-wide aspects are only allowed on tagged types (see 13.1.1), so we don't say that here. 
5.c/5
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.
6/5
{AI12-0187-1} {AI12-0285-1} 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.]
6.a/5
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. 
6.b/5
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. 
6.c/5
Ramification: Class-wide aspects are only allowed on primitive subprograms of tagged types (see 13.1.1), so we don't say that here.
6.d/5
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.
7/5
{AI12-0187-1} For a primitive subprogram, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
8/5
{AI12-0187-1} {AI12-0285-1} 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
{AI12-0187-1} {AI12-0285-1} 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.]
9.a/5
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

10/5
{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:
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
{AI12-0187-1} {AI12-0285-1} In a subprogram property aspect definition for a subprogram S:
14/5
all or none of the items shall be preceded by not;
14.a/5
Ramification: Mixing not functions with regular functions is not allowed. 
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
{AI12-0187-1} 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.
19.a/5
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”. 
20/5
{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.
21/5
{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.
22/5
{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].
22.a/5
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.
22.b/5
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. 
23/5
{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].
23.a/5
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.
23.b/5
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. 
NOTES
24/5
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

24.a/5
{AI12-0187-1} {AI12-0285-1} These aspects are new.

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