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.
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.
Aspect Description
for Pre: Precondition;
a condition that must hold true before a call.
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.
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).
Aspect Description
for Pre'Class: Precondition
inherited on type derivation.
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.
Aspect Description
for Post: Postcondition;
a condition that must hold true after a call.
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.
Aspect Description
for Post'Class: Postcondition
inherited on type derivation.
Name Resolution Rules
{
AI05-0145-2}
The expected type for a precondition or postcondition
expression is any boolean type.
{
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.]
{
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
{
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.]
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.
{
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
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,
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.
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.
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).
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.
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.
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.
{
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.
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.
Ramification: This
only applies to primitives of tagged types; other routines cannot have
class-wide preconditions.
Static Semantics
{
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.
{
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.
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.
the right operand of a short-circuit
control form; or
{
AI05-0145-2}
For a prefix
X that denotes an object of a nonlimited type, the following attribute
is defined:
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.
{
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.
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.
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.
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).
If X has controlled parts,
adjustment and finalization are implied by the implicit constant declaration.
If postconditions are
disabled, we want the compiler to avoid any overhead associated with
saving 'Old values.
'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.
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).
{
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:
Table : array (1..10) of Integer := ...
procedure Bar (I : in out Natural)
with Post => I > 0 and then Table(I)'Old = 1; -- Illegal
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 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 in such a context to statically denote an object,
which eliminates anything that could change at during execution.
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.)
{
AI05-0145-2}
For a prefix
F that denotes a function declaration, the following attribute is defined:
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.
{
AI05-0262-1}
Use of this attribute is allowed only within a
postcondition expression for F.
Dynamic Semantics
{
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:
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.
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.
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.
{
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.
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.
{
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.
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.
{
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.
{
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].
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.
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.
Note that this rule does
not apply to class-wide preconditions; they have their own rules mentioned
below.
{
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).
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.
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.
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.
{
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.
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
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe