6.1.1 Preconditions and Postconditions
“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
A generic formal subprogram is a subprogram, and
there are no rules to prevent using these attributes on it.
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.
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.
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).
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).
Aspect Description for Pre'Class:
Precondition inherited on type derivation.
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.
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
The expected type for a precondition or postcondition expression is any
Within the expression for a Pre'Class or Post'Class aspect for a primitive
of a tagged type T
a name 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 having type T'Class
Similarly, a name name
that denotes a formal access parameter (or S'Result)
of type access-to-T
is interpreted as having type access-to-NT access-to-T'Class
[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. This
ensures that the expression is well-defined for a primitive subprogram
of a type descended from T.
This ensures that the expression is well-defined
for any primitive subprogram of a type descended from T.
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.
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.
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.]
Pre'Class and Post'Class can only be specified on primitive routines
of tagged types, by a blanket rule found in 13.1.1
If a type T
has an implicitly declared subprogram P
from a parent type T1
and a homograph (see 8.3
from a progenitor type T2
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
and shall be overridden with a nonabstract subprogram.
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.
If a renaming of a subprogram or entry S1
overrides an inherited
, 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
class-wide precondition expression that applies to S2
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.
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
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
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
If a Pre'Class or Post'Class aspect is specified
for a primitive subprogram S
tagged type T
, or such an aspect defaults
then a corresponding the
expression also applies to the corresponding primitive
of each descendant of
T [(including T itself)]
. The corresponding expression is constructed from the associated
expression as follows:
Pre'Class defaults to True only if no class-wide preconditions are inherited
for the subprogram. The same is true for Post'Class.
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.
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).
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.
The primitive subprogram S is illegal if
it is not abstract and the corresponding expression for a Pre'Class or
Post'Class aspect would be illegal.
can happen, for instance, if one of the subprograms called in the corresponding
expression is abstract. We made the rule general so that we don't have
to worry about exactly which cases can cause this to happen, both now
and in the future.
Reason: We allow
illegal corresponding expressions on abstract subprograms as they could
never be evaluated, and we need to allow such expressions to contain
calls to abstract subprograms.
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, or access-to-subprogram type,
then the respective precondition or postcondition expressions are considered
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.
A subexpression of a postcondition expression is
known on entry if it is any of: An
is potentially unevaluated if it occurs within:
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 a
of a case_expression
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.
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).
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.
a name statically denoting a nonaliased in
parameter of an elementary type;
such parameters are by-copy, so the value won't change during the execution
of the subprogram.
an invocation of a predefined operator where all
of the operands are known on entry;
a function call where the function has aspect Global
=> null where all of the actual parameters are known on entry;
Reason: Such a
function can only depend on the values of its parameters.
OK if such an expression raises an exception, so long as every evaluation
of the expression raises the same exception.
A subexpression of a postcondition expression is
unconditionally evaluated, conditionally evaluated,
or repeatedly evaluated. The following subexpressions
are repeatedly evaluated:
If a subexpression is not repeatedly evaluated,
and not evaluated unconditionally, then it is conditionally evaluated,
and there is a set of determining expressions
that determine whether the subexpression is actually evaluated at run
time. Such subexpressions and their determining expressions are as follows:
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;
For the right operand
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;;
For a membership test that is not repeatedly evaluated,
a subexpression of
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 of a membership operation
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.
To be precise, a conditionally evaluated expression is determined
to be unevaluated (including all of its subexpressions) under the following
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;
statically denotes the declaration
of an object [(possibly through one or more renames)];
from the definition of statically denotes (see 4.9).
is a selected_component
whose prefix statically names an object, there is no implicit dereference
of the prefix, and the selector_name
names a component that does not depend on a discriminant; or
Reason: We disallow
components that depend on a discriminant so that no discriminant checks
are needed to evaluate the selected_component.
is an indexed_component
whose prefix statically names an object, the object is statically constrained,
and the index expressions of the object are static and have values that
are within the range of the index constraint.
For a prefix
X that denotes an object of a nonlimited type, the following attribute
Each For 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, or
entry body, or accept statement
. 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.
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).
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
The implicitly declared entity denoted by each
occurrence of X'Old is declared as follows:
X'Old : constant A := X;
X is of a specific tagged type T then
anonymous : constant T'Class := T'Class(X);
X'Old : T renames T(anonymous);
name X'Old denotes the object renaming.
means that the underlying tag associated with X'Old is that of X and
not that of the nominal type of X.
X'Old : constant S := X;
is the nominal subtype of X. This includes the case where the type of
S is an anonymous array type or a universal type.
The type and nominal
subtype of X'Old is as implied by the above definitions. The expected type of the prefix of an Old attribute is that of the attribute.
Similarly, if an Old attribute shall resolve to be of some type, then
the prefix of the attribute shall resolve to be of that type.
Reference to this attribute is only allowed within a postcondition expression.
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
of an Old attribute_reference
that is potentially unevaluated
an entity, unless the attribute_reference
is unconditionally evaluated, or is conditionally evaluated where all
of the determining expressions are known on entry
X can be any nonlimited object that obeys the syntax for prefix other
than the few exceptions given above (discussed below). Useful cases are:
a formal parameter of mode [in
, 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. Similarly, the
implicit constant declaration defines the accessibility level of X'Old.
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.
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_expression
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).
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 prefix
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.)
An accept statement for a task entry with enabled
postconditions such as
accept E do
(at runtime) as follows:
accept E do
declarations, if any, of 'Old constants
Preconditions are checked by the caller before
the rendezvous begins. Postcondition expressions might, of course, reference
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.
For a prefix
F that denotes a function declaration or an access-to-function
, the following attribute is defined:
Within a postcondition expression for function
F, denotes the return result
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
access-to-function type result
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 was described previously.
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
To be honest:
An “access-to-function type” is an
access-to-subprogram type whose designated profile is a function profile.
For a prefix
E that denotes an entry declaration of an entry family (see 9.5.2),
the following attribute is defined:
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.
Use of this attribute is allowed only within a
precondition or postcondition expression for E.
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
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 It
is not specified whether in
a call on a protected operation, the
checks are performed before or after
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.
Upon successful return from a call of the subprogram or entry, prior
to copying back any by-copy in out
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
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.
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.
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.
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
For any call to a
subprogram or entry S 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
]. 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
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.
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 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.]
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.
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
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
). 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
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.
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.
For a call via an access-to-subprogram value, all
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.
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.
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.
[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.]
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.
An implementation may evaluate 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.
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.
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.
For an example of the use of these aspects and
attributes, see the Streams Subsystem definitions in 13.13.1.
Extensions to Ada 2005
Inconsistencies With Ada 2012
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 Standard. 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.
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.
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.
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 wheras 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
Incompatibilities With Ada 2012
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 be 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).
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.)
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
Extensions to Ada 2012
We make no restriction on the prefix of an Old
attribute 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.
Pre and Post can be given on an access-to-subprogram
type and on a generic formal subprogram.
Wording Changes from Ada 2012
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.
Correction: Removed redundant (and sometimes
incorrect) wording about the resolution of the Old and Result attributes.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe