6.1.1 Preconditions and Postconditions
Pre
This aspect specifies a specific precondition for a callable entity;
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.
Pre'Class
This aspect specifies a class-wide precondition for an 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.
Post
This aspect specifies a specific postcondition for a callable entity;
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.
Post'Class
This aspect specifies a class-wide postcondition for an 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
The expected type for a precondition or postcondition
expression is any boolean type.
Within the expression for a Pre'Class or Post'Class
aspect for a primitive subprogram of a tagged type T, a name that
denotes a formal parameter of type T is interpreted as having
type T'Class. Similarly, a name that denotes a formal access parameter
of type access-to-T is interpreted as having type access-to-T'Class.
This ensures that the expression is well-defined for a primitive subprogram
of a type descended from T.
For an attribute_reference with attribute_designator
Old, if the attribute reference has an expected type or shall resolve
to a given type, the same applies to the
prefix;
otherwise, the
prefix
shall be resolved independently of context.
Legality Rules
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.
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
the corresponding primitive subprogram P1
of type T1 is neither null nor abstract; and
the class-wide precondition expression True does
not apply to P1 (implicitly or explicitly); and
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,
then:
If the type T is abstract, the implicitly
declared subprogram P is abstract.
Otherwise, the subprogram
P requires
overriding and shall be overridden with a nonabstract subprogram.
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.
Static Semantics
If a Pre'Class or Post'Class aspect is specified
for a primitive subprogram of a tagged type T, then the associated
expression also applies to the corresponding primitive subprogram of
each descendant of T.
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 or entry, then the respective precondition or postcondition
expressions are considered
enabled.
An
expression
is
potentially unevaluated if it occurs within:
the right operand of a short-circuit control form;
or
For a
prefix
X that denotes an object of a nonlimited type, the following attribute
is defined:
X'Old
For each X'Old in a postcondition
expression that is enabled, a constant is implicitly declared at the
beginning of the subprogram or entry. The constant is of the type of
X and is initialized to the result of evaluating X (as an expression)
at the point of the constant declaration. The value of X'Old in the postcondition
expression is the value of this constant; the type of X'Old is the type
of X. These implicit constant declarations occur in an arbitrary order.
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
that is potentially unevaluated shall statically denote an entity.
For a
prefix
F that denotes a function declaration, the following attribute is defined:
F'Result
Within a postcondition expression
for function F, denotes the result object of the function. The type of
this attribute is that of the function result except within a Post'Class
postcondition expression for a function with a controlling result or
with a controlling access result. For a controlling result, the type
of the attribute is
T'Class, where
T is the function result
type. For a controlling access result, the type of the attribute is an
anonymous access type whose designated type is
T'Class, where
T is the designated type of the function result type.
Use of this attribute is allowed only within
a postcondition expression for F.
Dynamic Semantics
Upon a call of the subprogram or entry, after evaluating
any actual parameters, precondition checks are performed as follows:
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.
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.
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.
It is not specified whether in a call on a protected operation, the checks
are performed before or after starting the protected action. For an entry
call, the checks are performed prior to checking whether the entry is
open.
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.
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.
For any subprogram or entry call (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.
The class-wide precondition check for a call to
a subprogram or entry consists solely of checking the class-wide precondition
expressions that apply to the denoted callable entity (not necessarily
the one that is invoked).
For a call via an access-to-subprogram value, all
precondition and postcondition checks performed are determined by the
subprogram or entry denoted by the prefix of the Access attribute reference
that produced the value.
5 A precondition is checked just before
the call. If another task can change any value that the precondition
expression depends on, the precondition need not hold within the subprogram
or entry body.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe