Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
 
Annotated Ada Reference Manual (Ada 2022) — 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/5
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

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} {AI12-0388-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, each optionally preceded by reserved word 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} {AI12-0405-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 specific 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-0405-1} The specific and class-wide stable properties of a type together comprise the stable properties of the type.
8/5
{AI12-0187-1} For a primitive subprogram, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
9/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.
10/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.]
10.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

11/5
{AI12-0187-1} A stable property function of a type T shall have a nonlimited return type and shall be:
12/5
a primitive function with a single parameter of mode in of type T; or
13/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. 
14/5
{AI12-0187-1} {AI12-0285-1} In a subprogram property aspect definition for a subprogram S:
15/5
all or none of the items shall be preceded by not;
15.a/5
Ramification: Mixing not functions with regular functions is not allowed. 
16/5
any property functions mentioned after not shall be a stable property function of a type for which S is primitive. 
17/5
{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

18/5
{AI12-0187-1} For a primitive subprogram S of a type T, the specific stable property functions of S for type T are:
19/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;
20/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;
21/5
if S does not have an aspect Stable_Properties, those functions denoted in the aspect Stable_Properties for T, if any.
21.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 specific stable properties for a subprogram. Thus we say “specific stable property functions for subprogram S for type T”. 
22/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.
23/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.
24/5
{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:
25/5
S is a stable property function of T;
25.a/5
Reason: This prevents possible infinite recursion, where the postcondition calls the function itself (directly or indirectly). 
26/5
P has mode out;
26.a/5
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. 
27/5
the Global aspect of S is null, and P has mode in and the mode is not overridden by a global aspect.
27.a/5
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. 
28/5
{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].
28.a/5
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.
28.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. 
28.c/5
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.
29/5
{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].
29.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.
29.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.
29.c/5
{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. 
30/5
{AI12-0405-1} The equality operation that is used in the aforementioned equality expressions is as described in the case of an individual membership test whose membership_choice is a choice_simple_expression (see 4.5.2).
31/5
{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. 
32/5
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

32.a/5
{AI12-0187-1} {AI12-0285-1} {AI12-0405-1} These aspects are new.
Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe