Ada Reference Manual (Ada 2022) — Legal Information

# 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):
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.
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.
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.
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.

#### 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.
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.
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.
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.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.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.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.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.
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.
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.1/5
a name statically denoting a full constant declaration which is known to have no variable views (see 3.3);
22.2/5
a name statically denoting a nonaliased in parameter of an elementary type;
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.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.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.
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.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.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.
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.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.
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.
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.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.
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.
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.
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.
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.
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.

#### 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.
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.

Ada 2005 and 2012 Editions sponsored in part by Ada-Europe