6.1.1 Preconditions and Postconditions
1/3
2/3
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.
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/3
Aspect Description for Pre: Precondition;
a condition that must hold true before a call.
3/3
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.
3.a/3
Ramification: {
AI05-0254-1}
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/3
Aspect Description for Pre'Class:
Precondition inherited on type derivation.
4/3
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.
4.a/3
Aspect Description for Post: Postcondition;
a condition that must hold true after a call.
5/3
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.
5.a/3
Aspect Description for Post'Class:
Postcondition inherited on type derivation.
Name Resolution Rules
6/3
{
AI05-0145-2}
The expected type for a precondition or postcondition expression is any
boolean type.
7/3
{
AI05-0145-2}
{
AI05-0262-1}
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.]
8/3
{
AI05-0145-2}
{
AI05-0264-1}
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
9/3
{
AI05-0145-2}
{
AI05-0230-1}
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: {
AI05-0183-1}
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
{
AI05-0247-1}
{
AI05-0254-1}
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
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
{
AI05-0247-1}
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.
Static Semantics
18/3
{
AI05-0145-2}
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.
19/3
{
AI05-0145-2}
{
AI05-0262-1}
{
AI05-0290-1}
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.
19.a/3
Ramification: {
AI05-0290-1}
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/3
21/3
22/3
23/3
the right operand of a short-circuit control form;
or
24/3
25/3
{
AI05-0145-2}
For a
prefix
X that denotes an object of a nonlimited type, the following attribute
is defined:
26/3
X'Old
{
AI05-0145-2}
{
AI05-0262-1}
{
AI05-0273-1}
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.
27/3
{
AI05-0145-2}
{
AI05-0262-1}
{
AI05-0273-1}
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.
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/3
If X has controlled parts, adjustment and finalization
are implied by the implicit constant declaration.
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/3
Reason: {
AI05-0273-1}
Since the
prefix
is evaluated unconditionally when the subprogram is called, 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 it to include 'Old references, as those would be
redundant (the entire
prefix
is evaluated when the subprogram is called), 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/3
{
AI05-0273-1}
In addition, we only allow simple names as the
prefix
of the Old attribute if the
attribute_reference
might not be evaluated when the postcondition expression is evaluated.
This is necessary because the Old
prefixes
have to be unconditionally evaluated when the subprogram is called; 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 Tab(I)'Old = 1; -- Illegal
27.j/3
In this example,
the compiler cannot know the value of I when the subprogram returns (since
the subprogram execution can change it), and thus it does not know whether
Tab(I)'Old will be needed then. Thus it has to always create an implicit
constant and evaluate Tab(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 Tab(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 in such a context to statically denote an object,
which eliminates anything that could change at 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.)
28/3
{
AI05-0145-2}
For a
prefix
F that denotes a function declaration, the following attribute is defined:
29/3
F'Result
{
AI05-0145-2}
{
AI05-0262-1}
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.
30/3
{
AI05-0262-1}
Use of this attribute is allowed only within a postcondition expression
for F.
Dynamic Semantics
31/3
{
AI05-0145-2}
{
AI05-0247-1}
{
AI05-0290-1}
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/3
{
AI05-0145-2}
{
AI05-0247-1}
{
AI05-0254-1}
{
AI05-0269-1}
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.
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
{
AI05-0145-2}
{
AI05-0247-1}
{
AI05-0254-1}
{
AI05-0262-1}
{
AI05-0290-1}
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.
36/3
{
AI05-0145-2}
{
AI05-0262-1}
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/3
{
AI05-0145-2}
{
AI05-0247-1}
{
AI05-0254-1}
{
AI05-0262-1}
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].
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/3
{
AI05-0145-2}
{
AI05-0247-1}
{
AI05-0254-1}
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).
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.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/3
{
AI05-0145-2}
{
AI05-0247-1}
{
AI05-0254-1}
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.
40/3
5 {
AI05-0145-2}
{
AI05-0262-1}
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.
Extensions to Ada 2005
40.a/3
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe