6.1 Subprogram Declarations

danger

This Reference Manual output has not been verified, and may contain omissions or errors. Report any problems on the tracking issue

[A subprogram_declaration declares a procedure or function.]

Syntax

2/3

subprogram_declaration ::= 
    [overriding_indicator]
    subprogram_specification
        [aspect_specification];

3/2

This paragraph was deleted.

4/2

subprogram_specification ::= 
    procedure_specification
  | function_specification

4.1/2

procedure_specification ::= 
proceduredefining_program_unit_nameparameter_profile

4.2/2

function_specification ::= 
functiondefining_designatorparameter_and_result_profile

designator ::= [parent_unit_name . ]identifier | operator_symbol

defining_designator ::= 
    defining_program_unit_name | defining_operator_symbol

defining_program_unit_name ::= [parent_unit_name . ]defining_identifier

[The optional parent_unit_name is only allowed for library units (see 10.1.1).]

operator_symbol ::= string_literal

10/5

The sequence of characters in an operator_symbol shall form a reserved word, a delimiter, or compound delimiter that corresponds to an operator belonging to one of the six categories of operators defined in 4.5.

10.a/3

reason

The “sequence of characters” of the string literal of the operator is a technical term (see 2.6), and does not include the surrounding quote characters. As defined in 2.2, lexical elements are “formed” from a sequence of characters. Spaces are not allowed, and upper and lower case is not significant.

defining_operator_symbol ::= operator_symbol

parameter_profile ::= [formal_part]

13/2

parameter_and_result_profile ::= 
    [formal_part] return [null_exclusion] subtype_mark
  | [formal_part] return access_definition

formal_part ::= 
   (parameter_specification {; parameter_specification})

15/5

parameter_specification ::= 
    defining_identifier_list : [aliased] mode [null_exclusion] subtype_mark [:= default_expression]
        [aspect_specification]
  | defining_identifier_list : access_definition [:= default_expression]
        [aspect_specification]

15.a/5

discussion

Only implementation-defined aspects are allowed on formal parameters in Ada 2022. Implementers are cautioned that any aspect allowed on a formal parameter will need conformance rules. If, for instance, an aspect changed the representation of a parameter, rules would be needed to ensure that the representation is the same for the specification and body.

mode ::= [in] | in out | out

Name Resolution Rules

A formal parameter is an object [directly visible within a subprogram_body] that represents the actual parameter passed to the subprogram in a call; it is declared by a parameter_specification. For a formal parameter, the expected type for its default_expression, if any, is that of the formal parameter.

Legality Rules

18/3

The parameter mode of a formal parameter conveys the direction of information transfer with the actual parameter: in, in out, or out. Mode in is the default, and is the mode of a parameter defined by an access_definition.

18.a/3

This paragraph was deleted.

A default_expression is only allowed in a parameter_specification for a formal parameter of mode in.

20/3

A subprogram_declaration or a generic_subprogram_declaration requires a completion [unless the Import aspect (see B.1) is True for the declaration; the completion shall be a body or a renaming_declaration (see 8.5)]. [A completion is not allowed for an abstract_subprogram_declaration (see 3.9.3), a null_procedure_declaration (see 6.7), or an expression_function_declaration (see 6.8).]

20.a/3

ramification

Abstract subprograms , null procedures, and expression functions are not declared by subprogram_declarations, and so do not require completion (although the latter two can be completions). Protected subprograms are declared by subprogram_declarations, and so require completion. Note that an abstract subprogram is a subprogram, a null procedure is a subprogram, an expression function is a subprogram, and a protected subprogram is a subprogram, but a generic subprogram is not a subprogram.

20.b/3

proof

When the Import aspect is True for any entity, no completion is allowed (see B.1).

A name that denotes a formal parameter is not allowed within the formal_part in which it is declared, nor within the formal_part of a corresponding body or accept_statement.

21.a

ramification

By contrast, generic_formal_parameter_declarations are visible to subsequent declarations in the same generic_formal_part.

Static Semantics

The profile of (a view of) a callable entity is either a parameter_profile or parameter_and_result_profile[; it embodies information about the interface to that entity — for example, the profile includes information about parameters passed to the callable entity. All callable entities have a profile — enumeration literals, other subprograms, and entries. An access-to-subprogram type has a designated profile.] Associated with a profile is a calling convention. A subprogram_declaration declares a procedure or a function, as indicated by the initial reserved word, with name and profile as given by its specification.

23/2

The nominal subtype of a formal parameter is the subtype determined by the optional null_exclusion and the subtype_mark, or defined by the access_definition, in the parameter_specification. The nominal subtype of a function result is the subtype determined by the optional null_exclusion and the subtype_mark, or defined by the access_definition, in the parameter_and_result_profile.

23.1/3

An explicitly aliased parameter is a formal parameter whose parameter_specification includes the reserved word aliased.

24/2

An access parameter is a formal in parameter specified by an access_definition. An access result type is a function result type specified by an access_definition. An access parameter or result type is of an anonymous access type (see 3.10). [Access parameters of an access-to-object type allow dispatching calls to be controlled by access values. Access parameters of an access-to-subprogram type permit calls to subprograms passed as parameters irrespective of their accessibility level.]

24.a/2

discussion

Access result types have normal accessibility and thus don't have any special properties worth noting here.

The subtypes of a profile are:

For any non-access parameters, the nominal subtype of the parameter.

27/2

For any access parameters of an access-to-object type, the designated subtype of the parameter type.

27.1/3

For any access parameters of an access-to-subprogram type, the subtypes of the designated profile of the parameter type.

28/2

For any non-access result, the nominal subtype of the function result.

28.1/2

For any access result type of an access-to-object type, the designated subtype of the result type.

28.2/3

For any access result type of an access-to-subprogram type, the subtypes of the designated profile of the result type.

[ The types of a profile are the types of those subtypes.]

30/3

[A subprogram declared by an abstract_subprogram_declaration is abstract; a subprogram declared by a subprogram_declaration is not. See 3.9.3, “Abstract Types and Subprograms”. Similarly, a procedure declared by a null_procedure_declaration is a null procedure; a procedure declared by a subprogram_declaration is not. See 6.7, “Null Procedures”. Finally, a function declared by an expression_function_declaration is an expression function; a function declared by a subprogram_declaration is not. See 6.8, “Expression Functions”.]

30.1/2

[An overriding_indicator is used to indicate whether overriding is intended. See 8.3.1, “Overriding Indicators”.]

Dynamic Semantics

31/2

The elaboration of a subprogram_declaration has no effect.

NOTE 1 A parameter_specification with several identifiers is equivalent to a sequence of single parameter_specifications, as explained in 3.3.

NOTE 2 Abstract subprograms do not have bodies, and cannot be used in a nondispatching call (see 3.9.3, “Abstract Types and Subprograms”).

NOTE 3 The evaluation of default_expressions is caused by certain calls, as described in 6.4.1. They are not evaluated during the elaboration of the subprogram declaration.

NOTE 4 Subprograms can be called recursively and can be called concurrently from multiple tasks.

Examples

Examples of subprogram declarations:

procedure Traverse_Tree;
procedure Increment(X : in out Integer);
procedure Right_Indent(Margin : out Line_Size);          -- see 3.5.4
procedure Switch(From, To : in out Link);                -- see 3.10.1

38
function Random return Probability;                      -- see 3.5.7

39/4
function Min_Cell(X : Link) return Cell;                 -- see 3.10.1
function Next_Frame(K : Positive) return Frame;          -- see 3.10
function Dot_Product(Left, Right : Vector) return Real;  -- see 3.6
function Find(B : aliased in out Barrel; Key : String) return Real;
                                                         -- see 4.1.5

40
function "*"(Left, Right : Matrix) return Matrix;        -- see 3.6

Examples of in parameters with default expressions:

procedure Print_Header(Pages  : in Natural;
            Header : in Line    :=  (1 .. Line'Last => ' '); -- see 3.6
            Center : in Boolean := True);

Extensions to Ada 83

42.a

The syntax for abstract_subprogram_declaration is added. The syntax for parameter_specification is revised to allow for access parameters (see 3.10)

42.b/3

Program units that are library units may have a parent_unit_name to indicate the parent of a child (see 10.1.1).

Wording Changes from Ada 83

42.c

We have incorporated the rules from RM83-6.5, “Function Subprograms” here and in 6.3, “Subprogram Bodies”

42.d

We have incorporated the definitions of RM83-6.6, “Parameter and Result Type Profile - Overloading of Subprograms” here.

42.e

The syntax rule for defining_operator_symbol is new. It is used for the defining occurrence of an operator_symbol, analogously to defining_identifier. Usage occurrences use the direct_name or selector_name syntactic categories. The syntax rules for defining_designator and defining_program_unit_name are new.

Extensions to Ada 95

42.f/2

Subprograms now allow overriding_indicators for better error checking of overriding.

42.g/2

An optional null_exclusion can be used in a formal parameter declaration. Similarly, an optional null_exclusion can be used in a function result.

42.h/2

The return type of a function can be an anonymous access type.

Wording Changes from Ada 95

42.i/2

A description of the purpose of anonymous access-to-subprogram parameters and the definition of the profile of subprograms containing them was added.

42.j/2

Split the production for subprogram_specification in order to make the declaration of null procedures (see 6.7) easier.

42.k/2

Moved the Syntax and Dynamic Semantics for abstract_subprogram_declaration to 3.9.3, so that the syntax and semantics are together. This also keeps abstract and null subprograms similar.

42.l/2

Revised to allow other_format characters in operator_symbols in the same way as the underlying constructs.

Extensions to Ada 2005

42.m/3

Parameters can now be explicitly aliased, allowing parts of function results to designate parameters and forcing by-reference parameter passing.

42.n/3

The parameters of a function can now have any mode.

42.o/3

An optional aspect_specification can be used in a subprogram_declaration. This is described in 13.1.1.

Wording Changes from Ada 2005

42.p/3

Added expression functions (see 6.8) to the wording.

Extensions to Ada 2012

42.q/5

Parameters now can have an aspect_specification, allowing the specification of (implementation-defined) aspects for individual parameters.

6.1.1 Preconditions and Postconditions

1/5

For a noninstance subprogram [(including a generic formal subprogram)], a generic subprogram, an entry, or an access-to-subprogram type, the following language-defined assertion aspects may be specified with an aspect_specification (see 13.1.1):

1.a/4

ramification

“Noninstance subprogram” excludes a subprogram that is an instance of a generic subprogram. In that case, the aspects should be specified on the generic subprogram. If preconditions or postconditions need to be added to an instance of a generic subprogram, it can be accomplished by creating a separate subprogram specification and then completing that specification with a renames-as-body of the instance.

1.b/5

proof

A generic formal subprogram is a subprogram, and there are no rules to prevent using these attributes on it.

2/5

Pre

This aspect specifies a specific precondition for a callable entity or an access-to-subprogram type; it shall be specified by an expression, called a specific precondition expression. If not specified for an entity, the specific precondition expression for the entity is the enumeration literal True.

2.a/3

To be honest: In this and the following rules, we are talking about the enumeration literal True declared in package Standard (see A.1), and not some other value or identifier True. That matters as some rules depend on full conformance of these expressions, which depends on the specific declarations involved.

2.b/5

Aspect Description for Pre: Precondition; a condition that is expected to hold true before a call.

3/5

Pre'Class

This aspect specifies a class-wide precondition for a dispatching operation of a tagged type and its descendants; it shall be specified by an expression, called a class-wide precondition expression. If not specified for an entity, then if no other class-wide precondition applies to the entity, the class-wide precondition expression for the entity is the enumeration literal True.

3.a/3

ramification

If other class-wide preconditions apply to the entity and no class-wide precondition is specified, no class-wide precondition is defined for the entity; of course, the class-wide preconditions (of ancestors) that apply are still going to be checked. We need subprograms that don't have ancestors and don't specify a class-wide precondition to have a class-wide precondition of True, so that adding such a precondition to a descendant has no effect (necessary as a dispatching call through the root routine would not check any precondition).

3.b/5

Pre'Class cannot be specified on an access-to-subprogram type because of a Legality Rule found in 13.1.1 that limits 'Class aspects to tagged types and primitive subprograms of tagged types. The same is true for Post'Class (below).

3.c/5

Aspect Description for Pre'Class: Precondition that applies to corresponding subprograms of descendant types.

4/5

Post

This aspect specifies a specific postcondition for a callable entity or an access-to-subprogram type; it shall be specified by an expression, called a specific postcondition expression. If not specified for an entity, the specific postcondition expression for the entity is the enumeration literal True.

4.a/5

Aspect Description for Post: Postcondition; a condition that will hold true after a call.

5/5

Post'Class

This aspect specifies a class-wide postcondition for a dispatching operation of a tagged type and its descendants; it shall be specified by an expression, called a class-wide postcondition expression. If not specified for an entity, the class-wide postcondition expression for the entity is the enumeration literal True.

5.a/5

Aspect Description for Post'Class: Postcondition that applies to corresponding subprograms of descendant types.

5.b/5

discussion

In the AARM notes below, we use the terms “inherited” and “inheritance” informally with respect to class-wide pre/post-conditions, to mean that the aspect applies to corresponding subprograms in descendant types.

5.c/5

Term entry: precondition — assertion that is expected to be True when a given subprogram is called

5.d/5

Term entry: postcondition — assertion that is expected to be True when a given subprogram returns normally

Name Resolution Rules

6/3

The expected type for a precondition or postcondition expression is any boolean type.

7/5

Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram S of a tagged type T, a name that denotes a formal parameter (or S'Result) of type T is interpreted as though it had a (notional) nonabstract type NT that is a formal derived type whose ancestor type is T, with directly visible primitive operations. Similarly, a name that denotes a formal access parameter (or S'Result for an access result) of type access-to-T is interpreted as having type access-to-NT. [The result of this interpretation is that the only operations that can be applied to such names are those defined for such a formal derived type.]

7.a/4

reason

This ensures that the expression is well-defined for any primitive subprogram of a type descended from T.

7.b/5

ramification

The operations of NT are also nonabstract, so the rule against a call of an abstract subprogram does not trigger for a class-wide precondition or postcondition.

8/5

For an attribute_reference with attribute_designator Old, if the attribute reference has an expected type (or class of types) or shall resolve to a given type, the same applies to the prefix; otherwise, the prefix shall be resolved independently of context.

Legality Rules

9/3

The Pre or Post aspect shall not be specified for an abstract subprogram or a null procedure. [Only the Pre'Class and Post'Class aspects may be specified for such a subprogram.]

9.a/3

discussion

Pre'Class and Post'Class can only be specified on primitive routines of tagged types, by a blanket rule found in 13.1.1.

10/3

If a type T has an implicitly declared subprogram P inherited from a parent type T1 and a homograph (see 8.3) of P from a progenitor type T2, and

11/3

the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and

12/3

the class-wide precondition expression True does not apply to P1 (implicitly or explicitly); and

13/3

there is a class-wide precondition expression that applies to the corresponding primitive subprogram P2 of T2 that does not fully conform to any class-wide precondition expression that applies to P1,

14/3

then:

15/3

If the type T is abstract, the implicitly declared subprogram P is abstract.

16/3

Otherwise, the subprogram P requires overriding and shall be overridden with a nonabstract subprogram.

16.a/3

discussion

We use the term "requires overriding" here so that this rule is taken into account when calculating visibility in 8.3; otherwise we would have a mess when this routine is overridden.

16.b/3

reason

Such an inherited subprogram would necessarily violate the Liskov Substitutability Principle (LSP) if called via a dispatching call from an ancestor other than the one that provides the called body. In such a case, the class-wide precondition of the actual body is stronger than the class-wide precondition of the ancestor. If we did not enforce that precondition for the body, the body could be called when the precondition it knows about is False — such "counterfeiting" of preconditions has to be avoided. But enforcing the precondition violates LSP. We do not want the language to be implicitly creating bodies that violate LSP; the programmer can still write an explicit body that calls the appropriate parent subprogram. In that case, the violation of LSP is explicitly in the code and obvious to code reviewers (both human and automated).

16.c/3

We have to say that the subprogram is abstract for an abstract type in this case, so that the next concrete type has to override it for the reasons above. Otherwise, inserting an extra level of abstract types would eliminate the requirement to override (as there is only one declared operation for the concrete type), and that would be bad for the reasons given above.

16.d/3

ramification

This requires the set of class-wide preconditions that apply to the interface routine to be strictly stronger than those that apply to the concrete routine. Since full conformance requires each name to denote the same declaration, it is unlikely that independently declared preconditions would conform. This rule does allow "diamond inheritance" of preconditions, and of course no preconditions at all match.

16.e/3

We considered adopting a rule that would allow examples where the expressions would conform after all inheritance has been applied, but this is complex and is not likely to be common in practice. Since the penalty here is just that an explicit overriding is required, the complexity is too much.

17/3

If a renaming of a subprogram or entry S1 overrides an inherited subprogram S2, then the overriding is illegal unless each class-wide precondition expression that applies to S1 fully conforms to some class-wide precondition expression that applies to S2 and each class-wide precondition expression that applies to S2 fully conforms to some class-wide precondition expression that applies to S1.

17.a/3

reason

Such an overriding subprogram would violate LSP, as the precondition of S1 would usually be different (and thus stronger) than the one known to a dispatching call through an ancestor routine of S2. This is always OK if the preconditions match, so we always allow that.

17.b/3

ramification

This only applies to primitives of tagged types; other routines cannot have class-wide preconditions.

17.1/4

Pre'Class shall not be specified for an overriding primitive subprogram of a tagged type T unless the Pre'Class aspect is specified for the corresponding primitive subprogram of some ancestor of T.

17.c/4

reason

Any such Pre'Class will have no effect, as it will be ored with True. As such, it is highly misleading for readers, especially for those who are determining the assumptions that can be made in the body of the primitive subprogram. Note that in this case there is nothing explicit that might indicate that the class-wide precondition is ineffective. This rule does not prevent explicitly writing an ineffective class-wide precondition (for instance, if the parent subprogram has explicitly specified a precondition of True).

17.2/4

In addition to the places where Legality Rules normally apply (see 12.3), these rules also apply in the private part of an instance of a generic unit.

Static Semantics

18/5

If a Pre'Class or Post'Class aspect is specified for a primitive subprogram S of a tagged type T, or such an aspect defaults to True, then a corresponding expression also applies to the corresponding primitive subprogram S of each descendant of T [(including T itself)]. The corresponding expression is constructed from the associated expression as follows:

18.a/4

ramification

A Pre'Class defaults to True only if no class-wide preconditions are inherited for the subprogram. The same is true for Post'Class.

18.b/4

reason

We have to inherit precondition expressions that default to True, so that later overridings don't strengthen the precondition (a violation of LSP). We do the same for postconditions for consistency.

18.1/4

References to formal parameters of S (or to S itself) are replaced with references to the corresponding formal parameters of the corresponding inherited or overriding subprogram S (or to the corresponding subprogram S itself).

18.c/4

reason

We have to define the corresponding expression this way as overriding routines are only required to be subtype conformant; in particular, the parameter names can be different. So we have to talk about corresponding parameters without mentioning any names.

18.2/5

If the primitive subprogram S is not abstract, but the given descendant of T is abstract, then a nondispatching call on S is illegal if any Pre'Class or Post'Class aspect that applies to S is other than a static boolean expression. Similarly, a primitive subprogram of an abstract type T, to which a non-static Pre'Class or Post'Class aspect applies, shall neither be the prefix of an Access attribute_reference, nor shall it be a generic actual subprogram for a formal subprogram declared by a formal_concrete_subprogram_declaration.

18.d/5

This paragraph was deleted.

18.e/5

reason

The above rules mean that a concrete primitive of an abstract type is effectively treated as abstract, if any nontrivial Pre'Class or Post'Class aspects apply to it. This makes sense because we are using a notional formal derived type model for such aspects, and an abstract type is not permitted as an actual type for such a formal type. If we didn't do this, the evaluation of the precondition or postcondition of a concrete subprogram of an abstract type could possibly call abstract functions..

18.f/5

discussion

As this Reference Manual was frozen, a significant incompatibility has come to light with the above rule. The wording makes some calls to non-abstract primitives of a tagged abstract type illegal even if no abstract routines are involved in the Pre'Class or Post'Class. It is likely that the above rule will be adjusted; check with ARG work at www.ada-auth.org/arg.html to find the adjusted rules.

19/5

If performing checks is required by the Pre, Pre'Class, Post, or Post'Class assertion policies (see 11.4.2) in effect at the point of a corresponding aspect specification applicable to a given subprogram, entry, or access-to-subprogram type, then the respective precondition or postcondition expressions are considered enabled.

19.a/3

ramification

If a class-wide precondition or postcondition expression is enabled, it remains enabled when inherited by an overriding subprogram, even if the policy in effect is Ignore for the inheriting subprogram.

20/5

A subexpression of a postcondition expression is known on entry if it is any of:

21/5

a static subexpression (see 4.9);

22/5

a literal whose type does not have any Integer_Literal, Real_Literal, or String_Literal aspect specified, or the function specified by such an attribute has aspect Global specified to be null;

22.a/5

reason

We mention literals explicitly in case they are not static (as when their subtype is not static, they are the literal null, and so on). We exclude literals of types with the aspects that are not Global => null as those cause a user-written subprogram with possible side effects to be called.

22.1/5

a name statically denoting a full constant declaration which is known to have no variable views (see 3.3);

22.b/5

ramification

Constants of types with immutably limited or controlled parts are not allowed by this rule. Generic formal in objects are allowed by this rule (as they are defined to be full constant declarations).

22.c/5

reason

We only want things that cannot be changed. We can't just say “constant” since that includes views of variables in some cases (for instance, a dereference of an access to constant object can be a view of a variable). There are other things we could have allowed (like a loop parameter), but having a subprogram declaration where those could be used (like inside of a loop) seems unusual enough to not be worth defining.

22.2/5

a name statically denoting a nonaliased in parameter of an elementary type;

22.d/5

ramification

All such parameters are by-copy, so the value won't change during the execution of the subprogram.

22.3/5

an Old attribute_reference;

22.4/5

an invocation of a predefined operator where all of the operands are known on entry;

22.5/5

a function call where the function has aspect Global => null where all of the actual parameters are known on entry;

22.e/5

reason

Such a function can only depend on the values of its parameters.

22.6/5

a selected_component of a known-on-entry prefix;

22.7/5

an indexed_component of a known-on-entry prefix where all index expressions are known on entry;

22.8/5

a parenthesized known-on-entry expression;

22.9/5

a qualified_expression or type_conversion whose operand is a known-on-entry expression;

22.10/5

a conditional_expression where all of the conditions, selecting_expressions, and dependent_expressions are known on entry.

22.f/5

discussion

It's OK if such an expression raises an exception, so long as every evaluation of the expression raises the same exception.

22.11/5

A subexpression of a postcondition expression is unconditionally evaluated, conditionally evaluated, or repeatedly evaluated. A subexpression is considered unconditionally evaluated unless it is conditionally evaluated or repeatedly evaluated.

22.12/5

The following subexpressions are repeatedly evaluated:

22.13/5

A subexpression of a predicate of a quantified_expression;

22.14/5

A subexpression of the expression of an array_component_association;

22.15/5

A subexpression of the expression of a container_element_association.

22.16/5

For a subexpression that is conditionally evaluated, there is a set of determining expressions that determine whether the subexpression is actually evaluated at run time. Subexpressions that are conditionally evaluated and their determining expressions are as follows:

22.17/5

For an if_expression that is not repeatedly evaluated, a subexpression of any part other than the first condition is conditionally evaluated, and its determining expressions include all conditions of the if_expression that precede the subexpression textually;

22.18/5

For a case_expression that is not repeatedly evaluated, a subexpression of any dependent_expression is conditionally evaluated, and its determining expressions include the selecting_expression of the case_expression;

23/5

For a short-circuit control form that is not repeatedly evaluated, a subexpression of the right-hand operand is conditionally evaluated, and its determining expressions include the left-hand operand of the short-circuit control form;

24/5

For a membership test that is not repeatedly evaluated, a subexpression of a membership_choice other than the first is conditionally evaluated, and its determining expressions include the tested_simple_expression and the preceding membership_choices of the membership test.

24.1/5

A conditionally evaluated subexpression is determined to be unevaluated at run time if its set of determining expressions are all known on entry, and when evaluated on entry their values are such that the given subexpression is not evaluated.

24.a/5

ramification

To be precise, a conditionally evaluated expression is determined to be unevaluated (including all of its subexpressions) under the following circumstances:

24.b/5

Within an if_expression, a dependent_expression with an associated condition that evaluates to False, or a condition or dependent_expression where a condition of a preceding part of the if_expression evaluates to True;

24.c

Within a case_expression, a dependent_expression with an discrete_choice_list that is not covered by the value of the selecting_expression;

24.d/5

The right-hand operand of a short-circuit control form where the left-hand operand evaluates to False for and then or True for or else;

24.e/5

A membership_choice of a membership test where the individual membership test defined by any prior membership_choice evaluates to True.

25/3

For a prefix X that denotes an object of a nonlimited type, the following attribute is defined:

26/5

X'Old

Each X'Old in a postcondition expression that is enabled, other than those that occur in subexpressions that are determined to be unevaluated, denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement.

26.a/5

ramification

If X'Old occurs in a subexpression that is determined to be unevaluated, then there is no associated constant, and no evaluation of the prefix takes place. In general, this will require evaluating one or more known-on-entry subexpressions before creating and initializing any X'Old constants. Note that any 'Old in a known-on-entry subexpression evaluated this way represents the current value of the prefix (the 'Old itself can be ignored).

26.b/5

In the case of an accept statement, the constant is declared inside of the rendezvous. It is considered part of the initialization of the postcondition check, which is part of the rendezvous by definition (see 9.5.2).

26.1/4

The implicitly declared entity denoted by each occurrence of X'Old is declared as follows:

26.2/4

If X is of an anonymous access type defined by an access_definition A then

26.3/4

X'Old : constant A := X;

26.4/4

If X is of a specific tagged type T then

26.5/4

anonymous : constant T'Class := T'Class(X);
X'Old : T renames T(anonymous);

26.6/4

where the name X'Old denotes the object renaming.

26.c/4

ramification

This means that the underlying tag associated with X'Old is that of X and not that of the nominal type of X.

26.7/4

Otherwise

26.8/4

X'Old : constant S := X;

26.9/4

where S is the nominal subtype of X. This includes the case where the type of S is an anonymous array type or a universal type.

26.10/5

The type and nominal subtype of X'Old are as implied by the above definitions.

27/5

Reference to this attribute is only allowed within a postcondition expression. The prefix of an Old attribute_reference shall not contain a Result attribute_reference, nor an Old attribute_reference, nor a use of an entity declared within the postcondition expression but not within prefix itself (for example, the loop parameter of an enclosing quantified_expression). The prefix of an Old attribute_reference shall statically name (see 4.9) an entity, unless the attribute_reference is unconditionally evaluated, or is conditionally evaluated where all of the determining expressions are known on entry.

27.a/3

discussion

The prefix X can be any nonlimited object that obeys the syntax for prefix other than the few exceptions given above (discussed below). Useful cases are: the name of a formal parameter of mode [in] out, the name of a global variable updated by the subprogram, a function call passing those as parameters, a subcomponent of those things, etc.

27.b/3

A qualified expression can be used to make an arbitrary expression into a valid prefix, so T'(X + Y)'Old is legal, even though (X + Y)'Old is not. The value being saved here is the sum of X and Y (a function result is an object). Of course, in this case "+"(X, Y)'Old is also legal, but the qualified expression is arguably more readable.

27.c/3

Note that F(X)'Old and F(X'Old) are not necessarily equal. The former calls F(X) and saves that value for later use during the postcondition. The latter saves the value of X, and during the postcondition, passes that saved value to F. In most cases, the former is what one wants (but it is not always legal, see below).

27.d/4

If X has controlled parts, adjustment and finalization are implied by the implicit constant declaration. Similarly, the implicit constant declaration defines the accessibility level of X'Old.

27.e/3

If postconditions are disabled, we want the compiler to avoid any overhead associated with saving 'Old values.

27.f/3

'Old makes no sense for limited types, because its implementation involves copying. It might make semantic sense to allow build-in-place, but it's not worth the trouble.

27.g/5

reason

Since the prefix of an Old attribute_reference is evaluated when the subprogram is called (if it is evaluated at all), we cannot allow it to include values that do not exist at that time (like 'Result and loop parameters of quantified_expressions). We also do not allow the prefix itself to include 'Old references, as those would be redundant (because the evaluation of the prefix, if it occurs, already happens on entry to the subprogram ), and allowing them would require some sort of order to the implicit constant declarations (because in A(I'Old)'Old, we surely would want the value of I'Old evaluated before the A(I'Old) is evaluated).

27.h/5

An additional rule applies when it cannot be determined on entry to the subprogram whether the Old attribute_reference will or will not be evaluated when the overall postcondition expression is evaluated. In such cases, we require that the prefix of the Old attribute_reference to statically name some object. This is necessary because the Old prefixes have to be evaluated when the subprogram is called if there is any possibility that they might be needed; the compiler cannot in general know whether they will be needed in the postcondition expression. To see the problem, consider:

27.i/3

Table : array (1..10) of Integer := ...
procedure Bar (I : in out Natural)
   with Post => I > 0 and then Table(I)'Old = 1; -- Illegal

27.j/5

In this example, the compiler cannot know on entry what will be the value of I when the subprogram returns (since the subprogram execution can change it), and thus it does not know whether Table(I)'Old will be needed then. Thus it has to always create an implicit constant and evaluate Table(I) when Bar is called (because not having the value when it is needed is not acceptable). But if I = 0 when the subprogram is called, that evaluation will raise Constraint_Error, and that will happen even if I is unchanged by the subprogram and the value of Table(I)'Old is not ultimately needed. It's easy to see how a similar problem could occur for a dereference of an access type. This would be mystifying (since the point of the short circuit is to eliminate this possibility, but it cannot do so). Therefore, we require the prefix of any Old attribute_reference in such a context to statically name an object, which eliminates anything that could change during execution.

27.k/3

It is easy to work around most errors that occur because of this rule. Just move the 'Old to the outer object, before any indexing, dereferences, or components. (That does not work for function calls, however, nor does it work for array indexing if the index can change during the execution of the subprogram.)

27.l/4

ramification

An accept statement for a task entry with enabled postconditions such as

27.m/4

accept E do
   statements
exception
   handlers
end;

27.n/4

behaves (at runtime) as follows:

27.o/4

accept E do
   declare
      declarations, if any, of 'Old constants
   begin
      begin
         statements
      exception
         handlers
      end;
      postcondition checks
   end;
end;

27.p/4

Preconditions are checked by the caller before the rendezvous begins. Postcondition expressions might, of course, reference 'Old constants.

27.q/4

In the case of a protected operation with enabled postconditions, 'Old constant declarations (if any) are elaborated after the start of the protected action. Postcondition checks (which might reference these constants) are performed before the end of the protected action as described below.

27.r/5

The prefix of an Old attribute_reference has to statically name an entity if it appears within a repeatedly evaluated expression.

28/5

For a prefix F that denotes a function declaration or an access-to-function type, the following attribute is defined:

29/5

F'Result

Within a postcondition expression for F, denotes the return object of the function call for which the postcondition expression is evaluated. The type of this attribute is that of the result subtype of the function or access-to-function type except within a Post'Class postcondition expression for a function with a controlling result or with a controlling access result; in those cases the type of the attribute is described above as part of the Name Resolution Rules for Post'Class.

30/3

Use of this attribute is allowed only within a postcondition expression for F.

30.a/5

To be honest: An “access-to-function type” is an access-to-subprogram type whose designated profile is a function profile.

30.1/5

For a prefix E that denotes an entry declaration of an entry family (see 9.5.2), the following attribute is defined:

30.2/5

E'Index

Within a precondition or postcondition expression for entry family E, denotes the value of the entry index for the call of E. The nominal subtype of this attribute is the entry index subtype.

30.3/5

Use of this attribute is allowed only within a precondition or postcondition expression for E.

Dynamic Semantics

31/3

Upon a call of the subprogram or entry, after evaluating any actual parameters, precondition checks are performed as follows:

32/3

The specific precondition check begins with the evaluation of the specific precondition expression that applies to the subprogram or entry, if it is enabled; if the expression evaluates to False, Assertions.Assertion_Error is raised; if the expression is not enabled, the check succeeds.

33/3

The class-wide precondition check begins with the evaluation of any enabled class-wide precondition expressions that apply to the subprogram or entry. If and only if all the class-wide precondition expressions evaluate to False, Assertions.Assertion_Error is raised.

33.a/3

ramification

The class-wide precondition expressions of the entity itself as well as those of any parent or progenitor operations are evaluated, as these expressions apply to the corresponding operations of all descendants.

33.b/3

Class-wide precondition checks are performed for all appropriate calls, but only enabled precondition expressions are evaluated. Thus, the check would be trivial if no precondition expressions are enabled.

34/5

The precondition checks are performed in an arbitrary order, and if any of the class-wide precondition expressions evaluate to True, it is not specified whether the other class-wide precondition expressions are evaluated. The precondition checks and any check for elaboration of the subprogram body are performed in an arbitrary order. In a call on a protected operation, the checks are performed before starting the protected action. For an entry call, the checks are performed prior to checking whether the entry is open.

34.a/3

reason

We need to explicitly allow short-circuiting of the evaluation of the class-wide precondition check if any expression fails, as it consists of multiple expressions; we don't need a similar permission for the specific precondition check as it consists only of a single expression. Nothing is evaluated for the call after a check fails, as the failed check propagates an exception.

35/3

Upon successful return from a call of the subprogram or entry, prior to copying back any by-copy in out or out parameters, the postcondition check is performed. This consists of the evaluation of any enabled specific and class-wide postcondition expressions that apply to the subprogram or entry. If any of the postcondition expressions evaluate to False, then Assertions.Assertion_Error is raised. The postcondition expressions are evaluated in an arbitrary order, and if any postcondition expression evaluates to False, it is not specified whether any other postcondition expressions are evaluated. The postcondition check, and any constraint or predicate checks associated with in out or out parameters are performed in an arbitrary order.

35.a/3

ramification

The class-wide postcondition expressions of the entity itself as well as those of any parent or progenitor operations are evaluated, as these apply to all descendants; in contrast, only the specific postcondition of the entity applies. Postconditions can always be evaluated inside the invoked body.

35.1/4

For a call to a task entry, the postcondition check is performed before the end of the rendezvous; for a call to a protected operation, the postcondition check is performed before the end of the protected action of the call. The postcondition check for any call is performed before the finalization of any implicitly-declared constants associated (as described above) with Old attribute_references but after the finalization of any other entities whose accessibility level is that of the execution of the callable construct.

35.a.1/4

reason

If a postcondition references the implicitly-declared constant associated with an Old attribute, the postcondition must be evaluated before the constant is finalized. One way to think of this is to imagine declaring a controlled object between any implicit "'Old" constant declarations and any explicit declarations, then performing postcondition checks during the finalization of this object.

36/3

If a precondition or postcondition check fails, the exception is raised at the point of the call[; the exception cannot be handled inside the called subprogram or entry]. Similarly, any exception raised by the evaluation of a precondition or postcondition expression is raised at the point of call.

37/4

For any call to a subprogram or entry S (including dispatching calls), the checks that are performed to verify specific precondition expressions and specific and class-wide postcondition expressions are determined by those for the subprogram or entry actually invoked. Note that the class-wide postcondition expressions verified by the postcondition check that is part of a call on a primitive subprogram of type T includes all class-wide postcondition expressions originating in any progenitor of T[, even if the primitive subprogram called is inherited from a type T1 and some of the postcondition expressions do not apply to the corresponding primitive subprogram of T1]. Any operations within a class-wide postcondition expression that were resolved as primitive operations of the (notional) formal derived type NT, are in the evaluation of the postcondition bound to the corresponding operations of the type identified by the controlling tag of the call on S.[ This applies to both dispatching and non-dispatching calls on S.]

37.a/3

ramification

This applies to access-to-subprogram calls, dispatching calls, and to statically bound calls. We need this rule to cover statically bound calls as well, as specific pre- and postconditions are not inherited, but the subprogram might be.

37.b/3

For concrete subprograms, we require the original specific postcondition to be evaluated as well as the inherited class-wide postconditions in order that the semantics of an explicitly defined wrapper that does nothing but call the original subprogram is the same as that of an inherited subprogram.

37.c/3

Note that this rule does not apply to class-wide preconditions; they have their own rules mentioned below.

38/4

The class-wide precondition check for a call to a subprogram or entry S consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily to the one that is invoked). Any operations within such an expression that were resolved as primitive operations of the (notional) formal derived type NT are in the evaluation of the precondition bound to the corresponding operations of the type identified by the controlling tag of the call on S.[ This applies to both dispatching and non-dispatching calls on S.]

38.a/3

ramification

For a dispatching call, we are talking about the Pre'Class(es) that apply to the subprogram that the dispatching call is resolving to, not the Pre'Class(es) for the subprogram that is ultimately dispatched to. The class-wide precondition of the resolved call is necessarily the same or stronger than that of the invoked call. For a statically bound call, these are the same; for an access-to-subprogram, (which has no class-wide preconditions of its own), we check the class-wide preconditions of the invoked routine.

38.a.1/5

Since this check is based on the “callable entity”, it does not depend on the view of the entity. This matters any time the ancestor type (if any) of the partial view differs from the parent type of the full view. In such a case, the view of the callable entity associated with the full view might inherit a Pre'Class while the view of the same callable entity associated with the partial view does not.

38.b/3

implementation note

These rules imply that logically, class-wide preconditions of routines must be checked at the point of call (other than for access-to-subprogram calls, which must be checked in the body, probably using a wrapper). Specific preconditions that might be called with a dispatching call or via an access-to-subprogram value must be checked inside of the subprogram body. In contrast, the postcondition checks always need to be checked inside the body of the routine. Of course, an implementation can evaluate all of these at the point of call for statically bound calls if the implementation uses wrappers for dispatching bodies and for 'Access values.

38.c/3

There is no requirement for an implementation to generate special code for routines that are imported from outside of the Ada program. That's because there is a requirement on the programmer that the use of interfacing aspects do not violate Ada semantics (see B.1). That includes making pre- and postcondition checks. For instance, if the implementation expects routines to make their own postcondition checks in the body before returning, C code can be assumed to do this (even though that is highly unlikely). That's even though the formal definition of those checks is that they are evaluated at the call site. Note that pre- and postconditions can be very useful for verification tools (even if they aren't checked), because they tell the tool about the expectations on the foreign code that it most likely cannot analyze.

39/5

For the purposes of the above rules, a call on an inherited subprogram is considered to involve a call on a subprogram S' whose body consists only of a call (with appropriate conversions) on the non-inherited subprogram S from which the inherited subprogram was derived. It is not specified whether class-wide precondition or postcondition expressions that are equivalent (with respect to which non-inherited function bodies are executed) for S and S' are evaluated once or twice. If evaluated only once, the value returned is used for both associated checks.

39.a/5

implementation note

If the class-wide pre- and postcondition expressions are equivalent for S and S' because none of the primitive subprograms called in those expressions were overridden, no wrapper is needed. Otherwise, a wrapper is presumably needed to provide the correct logic.

40/5

For a call via an access-to-subprogram value, precondition and postcondition checks performed are as determined by the subprogram or entry denoted by the prefix of the Access attribute reference that produced the value. In addition, a precondition check of any precondition expression associated with the access-to-subprogram type is performed. Similarly, a postcondition check of any postcondition expression associated with the access-to-subprogram type is performed.

40.a/5

implementation note

A call via an access-to-subprogram value can be considered equivalent (with respect to dynamic semantics) to a call to a notional "wrapper" subprogram which has the Pre and Post aspects and the profile of the access-to-subprogram type and whose body contains (and returns, in the case of a function) only a call to the designated subprogram. However, other evaluation orders for the checks are allowed beyond those allowed by strictly following this model. This equivalence can be used to determine the appropriate point at which the constant associated with an Old attribute reference in the Post aspect for an access-to-subprogram type is elaborated and finalized.

40.b/5

ramification

In the case of type conversion between two access-to-subprogram types, the Pre and Post aspects of the source type of the conversion play no role in any subsequent call via the conversion result; only the Pre and Post aspects of the target type of the conversion are relevant in that case. The same applies in the case of a “conversion” (using the term loosely) which is accomplished by combining a dereference and an Access attribute reference, as in Some_Pointer.all'Access.

41/5

[For a call on a generic formal subprogram, precondition and postcondition checks performed are as determined by the subprogram or entry denoted by the actual subprogram, along with any specific precondition and specific postcondition of the formal subprogram itself.]

41.a/5

proof

This follows from the general Dynamic Semantics rules given above, but we mention it explicitly so that there can be no doubt that it is intended.

41.b/5

To be honest: The specific precondition and postcondition that apply to a generic formal subprogram also apply to any renaming of that subprogram, even if that renaming is visible in the instance and called from outside of the generic instance.

Implementation Permissions

42/5

An implementation may evaluate a known-on-entry subexpression of a postcondition expression of an entity at the place where X'Old constants are created for the entity, with the normal evaluation of the postcondition expression, or both.

42.a/5

reason

We allow the evaluation of known-on-entry subexpressions when they might be needed to determine whether to create a particular 'Old constant. We allow them to be evaluated later as well, or for the results to be saved somehow. This permission shouldn't matter, as the results ought to be same wherever they are evaluated and there should not be any side effects. The main effect of the permission is to determine when any exceptions caused by such subexpressions may be raised. We never require waiting to determine the value of such subexpressions, even if they aren't used to determine the creation of a constant for 'Old.

43/5

NOTE 1 A precondition is checked just before the call. If another task can change any value that the precondition expression depends on, the precondition can evaluate to False within the subprogram or entry body.

44/5

NOTE 2 For an example of the use of these aspects and attributes, see the Streams Subsystem definitions in 13.13.1.

Extensions to Ada 2005

44.a/3

Pre and Post aspects are new.

Inconsistencies With Ada 2012

44.b/4

Corrigendum: The Old attribute is defined more carefully. This changes the nominal subtype and place of declaration of the attribute compared to the published Ada 2012 Reference Manual. In extreme cases, this could change the runtime behavior of the attribute (for instance, the tag might be different). The changes are most likely going to prevent bugs by being more intuitive, but it is possible that a program that previously worked might fail.

44.c/4

Corrigendum: Eliminated unintentional redispatching from class-wide preconditions and postconditions. This means that a different body might be evaluated for a statically bound call to a routine that has a class-wide precondition or postcondition. The change means that the behavior of Pre and Pre'Class will be the same for a particular subprogram, and that the known behavior of the operations can be assumed within the body of that subprogram for Pre'Class. We expect that this change will primarily fix bugs, as it will make Pre'Class and Post'Class work more like expected. In the case where redispatching is desired, an explicit conversion to a class-wide type can be used.

44.d/5

correction

Specified that precondition checks always take place before starting a protected action. Original Ada 2012 left this unspecified, so if an implementation made the checks after starting the protected action, and a program depended upon that, the program might fail in a different compiler. But such a program was depending on unspecified behavior anyway, and thus was never portable; as such, such programs should be rare.

44.d.1/5

correction

Specified that an inherited subprogram check both the original and new versions of a class-wide precondition. If a call on an inherited subprogram fails the original class-wide precondition when it passes the new class-wide precondition, then the call will fail the precondition check whereas it would have passed in original Ada 2012. (A similar possibility exists for class-wide postconditions.) This can only happen if the overriding subprograms somehow fail to follow the guidelines of LSP, so this should be rare (the entire point of class-wide preconditions and postconditions is to use them in cases where LSP is followed).

Incompatibilities With Ada 2012

44.e/5

Corrigendum: Precondition and postcondition aspects cannot be specified on instances of generic subprograms (they should be specified on the generic subprogram instead). This was (unintentionally) allowed by the Ada 2012 standard. These are not allowed on instances as there is no corresponding way to add preconditions and postconditions to subprograms declared within the instance of a generic package. Therefore, allowing specification on a subprogram instance could present a maintenance problem in the future if the entity needs to be converted to a generic package (a common conversion).

44.f/4

Corrigendum: Pre'Class is no longer allowed to be specified for an overriding primitive subprogram unless there are also inherited class-wide precondittions. This incompatibility prevents cases where the explicit Pre'Class is counterfeited by an implicit class-wide precondition of True. This rule should catch more bugs than it creates; the programmer should have written Pre rather than Pre'Class in this case (or written Pre'Class on the original subprogram, not an overriding). Note that this incompatibility eliminates what otherwise would be an inconsistency with original Ada 2012, where precondition checks that would have previously been made for a statically bound call would no longer be made. That dynamic change was necessary to eliminate cases where the evaluated class-wide precondition on a dispatching call would have been weaker than the class-wide precondition of a statically bound call. (The original Ada 2012 violated the LSP semantics that class-wide preconditions were intended to model.)

44.g/5

correction

A component expression in an array aggregate can now be potentially unevaluated, requiring the prefix to be statically determined. Existing code that uses the Old attribute with a dynamic prefix in such contexts will now be illegal. However, in many cases, the existing code will not do what the programmer is expecting (as Old is evaluated textually, once per occurrence, while array aggregate components are evaluated once per component). In addition, Old is a new Ada 2012 feature, so most Ada legacy code will not contain it. The problem is usually easily fixed by moving Old to an outer object (such as the entire aggregate).

Extensions to Ada 2012

44.h/5

The Index attribute is new.

44.i/5

correction

The prefix of a statically unevaluated Old attribute_reference can be a selected_component or indexed_component. This is considered a correction as the old rule is unintentionally too fierce, rejecting safe cases.

44.j/5

We make no restriction on the prefix of an Old attribute_reference if we can determine when the subprogram is entered (which is the point when Old prefixes are evaluated) whether it will be needed in the evaluation of the postcondition.

44.k/5

Pre and Post can be given on an access-to-subprogram type and on a generic formal subprogram.

44.l/5

correction

We now allow the definition of a concrete subprogram S that has applicable Pre'Class or Post'Class expressions that is primitive for an abstract type T even when a Pre'Class or Post'Class may call an abstract subprogram. Rather, S is treated as if it is abstract (meaning that uses that might require evaluating a statically bound Pre'Class or Post'Class expression are not allowed).

Wording Changes from Ada 2012

44.m/5

correction

Clarified the wording about the meaning of the notional type NT and the corresponding expression. Both changes follow from other rules but are nonobvious.

44.n/5

correction

Removed redundant (and sometimes incorrect) wording about the resolution of the Old and Result attributes.

6.1.2 The Global and Global'Class Aspects

1/5

The Global and Global'Class aspects of a program unit are used to identify the objects global to the unit that can be read or written during its execution.

Syntax

2/5

global_aspect_definition ::= 
    null
  | Unspecified
  | global_mode global_designator
  | (global_aspect_element{; global_aspect_element})

3/5

global_aspect_element ::= 
    global_mode global_set
  | global_mode all
  | global_mode synchronized

4/5

global_mode ::= 
    basic_global_mode
  | extended_global_mode

5/5

basic_global_mode ::= in | in out | out

6/5

global_set ::= global_name {, global_name}

7/5

global_designator ::= all | synchronized | global_name

8/5

global_name ::= object_name | package_name

Name Resolution Rules

9/5

A global_name shall resolve to statically name an object or a package (including a limited view of a package).

Static Semantics

10/5

For a subprogram, an entry, an access-to-subprogram type, a task unit, a protected unit, or a library package or generic library package, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):

11/5

Global

The Global aspect shall be specified with a global_aspect_definition.

11.a/5

Aspect Description for Global: Global object usage contract.

12/5

The Global aspect identifies the set of variables (which, for the purposes of this clause, includes all constants except those which are known to have no variable views (see 3.3)) that are global to a callable entity or task body, and that are read or updated as part of the execution of the callable entity or task body. If specified for a protected unit, it refers to all of the protected operations of the protected unit. Constants of any type may also be mentioned in a Global aspect.

13/5

If not specified or otherwise defined below, the aspect defaults to the Global aspect for the enclosing library unit if the entity is declared at library level, and to Unspecified otherwise. If not specified for a library unit, the aspect defaults to Global => null for a library unit that is declared Pure, and to Global => Unspecified otherwise.

14/5

For a dispatching subprogram, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):

15/5

Global'Class

The Global'Class aspect shall be specified with a global_aspect_definition. This aspect identifies an upper bound on the set of variables global to a dispatching operation that can be read or updated as a result of a dispatching call on the operation. If not specified, the aspect defaults to the Global aspect for the dispatching subprogram.

15.a/5

Aspect Description for Global'Class: Global object usage contract inherited on derivation.

16/5

Together, we refer to the Global and Global'Class aspects as global aspects.

17/5

A global_aspect_definition defines the Global or Global'Class aspect of some entity. The Global aspect identifies the sets of global variables that can be read, written, or modified as a side effect of executing the operation(s) associated with the entity. The Global'Class aspect associated with a dispatching operation of type T represents a restriction on the Global aspect on a corresponding operation of any descendant of type T.

18/5

The Global aspect for a callable entity defines the global variables that can be referenced as part of a call on the entity, including any assertion expressions that apply to the call (even if not enabled), such as preconditions, postconditions, predicates, and type invariants.

19/5

The Global aspect for an access-to-subprogram object (or subtype) identifies the global variables that can be referenced when calling via the object (or any object of that subtype) including assertion expressions that apply.

20/5

For a predefined operator of an elementary type, the function representing an enumeration literal, or any other static function (see 4.9), the Global aspect is null. For a predefined operator of a composite type, the Global aspect of the operator defaults to that of the enclosing library unit (unless a Global aspect is specified for the type — see H.7).

21/5

The following is defined in terms of operations that are performed by or on behalf of an entity. The rules on operations apply to the entity(s) associated with those operations.

21.a/5

discussion

The operations performed by a callable entity are those associated with the body of the entity. For other kinds of entities (such as subtypes, see H.7), we explicitly list the associated operations.

22/5

The global variables associated with any global_mode can be read as a side effect of an operation. The in out and out global_modes together identify the set of global variables that can be updated as a side effect of an operation. Creating an access-to-variable value that designates an object is considered an update of the designated object, and creating an access-to-constant value that designates an object is considered a read of the designated object.

23/5

The overall set of objects associated with each global_mode includes all objects identified for the mode in the global_aspect_definition.

24/5

A global_set identifies a global variable set as follows:

25/5

all identifies the set of all global variables;

26/5

synchronized identifies the set of all synchronized variables (see 9.10), as well as variables of a composite type all of whose non-discriminant subcomponents are synchronized;

27/5

global_name{, global_name} identifies the union of the sets of variables identified by the global_names in the list, for the following forms of global_name:

28/5

object_name identifies the specified global variable (or constant);

29/5

package_name identifies the set of all variables declared in the private part or body of the package, or anywhere within a private descendant of the package.

Legality Rules

30/5

Within a global_aspect_definition, a given global_mode shall be specified at most once. Similarly, within a global_aspect_definition, a given entity shall be named at most once by a global_name.

31/5

If an entity (other than a library package or generic library package) has a Global aspect other than Unspecified or in out all, then the associated operation(s) shall read only those variables global to the entity that are within the global variable set associated with the in, in out, or out global_modes, and the operation(s) shall update only those variables global to the entity that are within the global variable set associated with either the in out or out global_modes. In the absence of the No_Hidden_Indirect_Globals restriction (see H.4), this ignores objects reached via a dereference of an access value. The above rule includes any possible Global effects of calls occurring during the execution of the operation, except for the following excluded calls:

32/5

calls to formal subprograms;

33/5

calls associated with operations on formal subtypes;

34/5

calls through formal objects of an access-to-subprogram type;

35/5

calls through access-to-subprogram parameters;

36/5

calls on operations with Global aspect Unspecified.

37/5

The possible Global effects of these excluded calls (other than those that are Unspecified) are taken into account by the caller of the original operation, by presuming they occur at least once during its execution. For calls that are not excluded, the possible Global effects of the call are those permitted by the Global aspect of the associated entity, or by its Global'Class aspect if a dispatching call.

37.a/5

ramification

For a predefined equality operator of a composite type, the possible Global effects includes those of the equality operations invoked as part of the evaluation of the operator (which might not be predefined and thus might have a different Global specification than the component types).

38/5

If a Global aspect other than Unspecified or in out all applies to an access-to-subprogram type, then the prefix of an Access attribute_reference producing a value of such a type shall denote a subprogram whose Global aspect is not Unspecified and is covered by that of the result type, where a global aspect G1 is covered by a global aspect G2 if the set of variables that G1 identifies as readable or updatable is a subset of the corresponding set for G2. Similarly on a conversion to such a type, the operand shall be of a named access-to-subprogram type whose Global aspect is covered by that of the target type.

39/5

If an implementation-defined global_mode applies to a given set of variables, an implementation-defined rule determines what sort of references to them are permitted.

40/5

For a subprogram that is a dispatching operation of a tagged type T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the in out mode, of the Global'Class aspect of a corresponding dispatching subprogram of any ancestor of T, unless the aspect of that ancestor is Unspecified.

Implementation Permissions

41/5

An implementation can allow some references to a constant object which are not accounted for by the Global or Global'Class aspect when it is considered a variable in the above rules, if the implementation can determine that the object is in fact immutable.

41.a/5

ramification

In particular, this allows the implementation to violate privacy in order to determine whether a constant needs to be covered by a Global aspect.

42/5

Implementations may perform additional checks on calls to operations with an Unspecified Global aspect to ensure that they do not violate any limitations associated with the point of call.

42.a/5

discussion

In this sense, Global => Unspecified is not permission to violate the caller's Global restrictions. It is rather that the implementor of the subprogram is presuming other means are being used to ensure safety. Note the No_Unspecified_Globals Restriction (H.4), which prevents the use of Unspecified with the Global aspect in a given partition.

43/5

Implementations may extend the syntax or semantics of the Global aspect in an implementation-defined manner[; for example, supporting additional global_modes].

43.a/5

implementation defined

Any extensions of the Global aspect.

43.b/5

reason

This is intended to allow preexisting usages from SPARK 2014 to remain acceptable in conforming implementations, as well as to provide flexibility for future enhancements. Note the word “extend” in this permission; we expect that any aspect usage that conforms with the (other) rules of this subclause will be accepted by any Ada implementation, regardless of any implementation-defined extensions.

44/5

NOTE For an example of the use of these aspects, see the Vector container definition in A.18.2.

Extensions to Ada 2012

44.a/5

The Global and Global'Class aspects are new.

6.1 Subprogram Declarations

Syntax​

Name Resolution Rules​

Legality Rules​

Static Semantics​

Dynamic Semantics​

Examples​

Extensions to Ada 83​

Wording Changes from Ada 83​

Extensions to Ada 95​

Wording Changes from Ada 95​

Extensions to Ada 2005​

Wording Changes from Ada 2005​

Extensions to Ada 2012​

6.1.1 Preconditions and Postconditions​

Name Resolution Rules​

Legality Rules​

Static Semantics​

Dynamic Semantics​

Implementation Permissions​

Extensions to Ada 2005​

Inconsistencies With Ada 2012​

Incompatibilities With Ada 2012​

Extensions to Ada 2012​

Wording Changes from Ada 2012​

6.1.2 The Global and Global'Class Aspects​

Syntax​

Name Resolution Rules​

Static Semantics​

Legality Rules​

Implementation Permissions​

Extensions to Ada 2012​

Syntax

Name Resolution Rules

Legality Rules

Static Semantics

Dynamic Semantics

Examples

Extensions to Ada 83

Wording Changes from Ada 83

Extensions to Ada 95

Wording Changes from Ada 95

Extensions to Ada 2005

Wording Changes from Ada 2005

Extensions to Ada 2012

6.1.1 Preconditions and Postconditions

Name Resolution Rules

Legality Rules

Static Semantics

Dynamic Semantics

Implementation Permissions

Extensions to Ada 2005

Inconsistencies With Ada 2012

Incompatibilities With Ada 2012

Extensions to Ada 2012

Wording Changes from Ada 2012

6.1.2 The Global and Global'Class Aspects

Syntax

Name Resolution Rules

Static Semantics

Legality Rules

Implementation Permissions

Extensions to Ada 2012