11.4.2 Pragmas Assert and Assertion_Policy
Pragma Assert is used to assert the truth of a boolean expression at
a point within a sequence of declarations or statements.
Assert pragmas, subtype predicates (see 3.2.4
preconditions and postconditions (see 6.1.1
type invariants (see 7.3.2
and default initial conditions (see 7.3.3)
are collectively referred to as assertions
; their boolean expressions
are referred to as assertion expressions
Glossary entry: A predicate is an assertion
that is expected to be True for all objects of a given subtype.
Glossary entry: A precondition is an
assertion that is expected to be True when a given subprogram is called.
Glossary entry: A postcondition is an
assertion that is expected to be True when a given subprogram returns
Glossary entry: An A
invariant is an assertion that is expected to be True for all objects
of a given private type when viewed from outside the defining package.
Glossary entry: See
An assertion is a boolean
expression that appears in any of the following: a pragma
Assert, a predicate, a precondition, a postcondition, an invariant, a
constraint, or a null exclusion. An assertion is expected to be True
at run time at certain specified places.
Pragma Assertion_Policy is used to control whether assertions are to
be ignored by the implementation, checked at run time, or handled in
some implementation-defined manner.
Name Resolution Rules
We allow any boolean type to
be like if_statement
and other conditionals; we only allow String for the message in order
to match raise_statement
of a pragma
Assertion_Policy shall identify an assertion
aspect, namely be
one of Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class,
Post, Post'Class, Type_Invariant, Type_Invariant'Class, Default_Initial_Condition,
or some implementation-defined (assertion) implementation
shall be either Check, Ignore, or some implementation-defined identifier
To be honest:
“Assert” is considered an “assertion
aspect” for the purposes of this rule, even though there is no
sort of entity that has an Assert aspect. It can only be specified using
an Assert pragma, and applies to a particular point in the execution
of a logical thread of control.
determines for each assertion aspect named in the pragma_argument_association
whether assertions of the given aspect are to be enforced by a runtime
check. The policy_identifier
Check requires that assertion expressions of the given aspect be checked
that they evaluate to True at the points specified for the given aspect;
Ignore requires that the assertion expression not be evaluated at these
points, and the runtime checks not be performed. [Note that for subtype
predicate aspects (see 3.2.4
), even when
the applicable Assertion_Policy is Ignore, the predicate will still be
evaluated as part of membership tests and Valid attribute_reference
and if static, will still have an effect on loop iteration over the subtype,
and the selection of case_statement_alternative
If no assertion_aspect_mark
are specified in the pragma, the specified policy applies to all assertion
applies to the named assertion aspects in a specific region, and applies
to all assertion expressions associated with those
specified in that region. A pragma
Assertion_Policy given in a declarative_part
or immediately within a package_specification
applies from the place of the pragma to the end of the innermost enclosing
declarative region. The region for a pragma
Assertion_Policy given as a configuration pragma is the declarative region
for the entire compilation unit (or units) to which it applies.
Ramification: This means that an Assertion_Policy
pragma that occurs in a scope enclosing the declaration of a generic
unit but not also enclosing the declaration of a given instance of that
generic unit will not apply to assertion expressions occurring within
the given instance.
If multiple Assertion_Policy pragmas apply to a given construct for a
given assertion aspect, the assertion policy is determined by the one
in the innermost enclosing region of a pragma
Assertion_Policy specifying a policy for the assertion aspect. If no
such Assertion_Policy pragma exists, the policy is implementation defined.
Implementation defined: The default assertion
The following language-defined library package exists:
Assertion_Error : exception
Assert(Check : in
Assert(Check : in
Boolean; Message : in
A compilation unit containing a check for an assertion (including a pragma
Assert) has a semantic dependence on the Assertions library unit.
If performing checks is required by the Assert assertion policy in effect
at the place of a pragma
Assert, the elaboration of the pragma consists of evaluating the boolean
expression, and if the result is False, evaluating the Message argument,
if any, and raising the exception Assertions.Assertion_Error, with a
message if the Message argument is provided.
Calling the procedure Assertions.Assert without a Message parameter is
if Check = False then
Calling the procedure Assertions.Assert with a Message parameter is equivalent
if Check = False then
raise Ada.Assertions.Assertion_Error with Message;
The procedures Assertions.Assert have these effects independently of
the assertion policy in effect.
Bounded (Run-Time) Errors
It is a bounded error to invoke a potentially blocking operation (see
) during the evaluation of an assertion
expression associated with a call on, or return from, a protected operation.
If the bounded error is detected, Program_Error is raised. If not detected,
execution proceeds normally, but if it is invoked within a protected
action, it might result in deadlock or a (nested) protected action.
Any postcondition expression, type invariant expression,
or default initial condition expression occurring in the specification
of a language-defined unit is enabled (see 6.1.1,
7.3.2, and 7.3.3).
Assertion_Policy does not have an effect on such postconditions, invariants,
and default initial conditions. This has no execution impact since such
assertions shouldn't fail anyway (see the next rule).
The evaluation of any such postcondition, type
invariant, or default initial condition expression shall either yield
True or propagate an exception from a raise_expression
that appears within the assertion expression.
other words, evaluating such an assertion expression will not return
a result of False, nor will it propagate an exception other than by evaluating
which is syntactically all or part of the assertion expression.
To be honest: Evaluation
of any expression might raise Storage_Error.
Reason: This allows
the Reference Manual to express semantic requirements as postconditions,
invariants, or default initial conditions (which are invariably clearer
than English prose would be) while keeping it clear that failing the
assertion check (or any other run time check) is not conforming behavior.
Any precondition expression occurring in the specification
of a language-defined unit is enabled (see 6.1.1)
unless suppressed (see 11.5). Similarly, any
predicate checks for a subtype occurring in the specification of a language-defined
unit are enabled (see 3.2.4) unless suppressed.
This allows the Reference Manual to express runtime
requirements on the client of a language-defined unit as preconditions
or predicates (which are clearer than English prose would be). Some such
requirements can be suppressed with pragma Suppress. Ada 2012 and earlier
versions did not provide a mechanism to suppress such code.
Assertion_Error may be declared by renaming an implementation-defined
exception from another package.
Reason: This permission is intended to
allow implementations which had an implementation-defined Assert pragma
to continue to use their originally defined exception. Without this permission,
such an implementation would be incorrect, as Exception_Name would return
the wrong name.
Implementations may define their own assertion policies.
If the result of a function call in an assertion is not needed to determine
the value of the assertion expression, an implementation is permitted
to omit the function call. [This permission applies even if the function
has side effects.]
An implementation need not allow the specification of an assertion expression
if the evaluation of the expression has a side effect such that an immediate
reevaluation of the expression could produce a different value. Similarly,
an implementation need not allow the specification of an assertion expression
that is checked as part of a call on or return from a callable entity
, if the evaluation of the expression has a side effect such
that the evaluation of some other assertion expression associated with
the same call of (or return from) C
could produce a different
value than it would if the first expression had not been evaluated.
Ramification: This allows an implementation
to reject such assertions. To maximize portability, assertions should
not include expressions that contain these sorts of side effects.
Discussion: The intended effect of the
second part of the rule (the part starting with “Similarly”)
is that an evaluation of the involved assertion expressions (subtype
predicates, type invariants, preconditions and postconditions) in any
order yields identical results.
The rule is intended to apply to all of the
assertion expressions that are evaluated at the start of call (and similarly
for the assertion expressions that are evaluated during the return from
a call), but not other assertions actually given in the body, nor between
the assertions checked at the start and end of the call. Specifically,
a side effect that alters a variable in a function called from a precondition
expression that changes the result of a postcondition expression of the
same subprogram does not trigger these rules unless it also changes
the value of a reevaluation of the precondition expression.
Language Design Principles
Our intent is that any assertion expression that
violates this Implementation Permission is considered pathological. We
definitely want compilers to be able to assume that if you evaluate an
assertion expression once and it is True, you don't need to evaluate
it again if all you are doing in the meantime is evaluating assertion
expressions. We were unable to find wording that had this effect that
didn't throw out important other cases (logging, memo functions), so
we settled for a strong warning that compilers can reject such pathologies.
Perhaps in a future version of Ada we'll be able to tighten this up.
Normally, the boolean expression in a pragma
Assert should not call functions that have significant side effects when
the result of the expression is True, so that the particular assertion
policy in effect will not affect normal operation of the program.
Extensions to Ada 95
Pragmas Assert and Assertion_Policy, and package
Assertions are new.
Incompatibilities With Ada 2005
There now is an Implementation Permission to reject
an assertion expression that calls a function that has a side effect
such that an immediate reevalution of the expression could produce a
different value. This means that a pragma
Assert that works in Ada 2005 might be illegal in Ada 2012 in the unlikely
event that the compiler detected such an error. This should be unlikely
to occur in practice and it is considered a good thing, as the original
expression was tricky and probably was not portable (as order of evaluation
is unspecified within an expression). Moreover, no compiler is required
to reject such expressions, so there is no need for any compiler to change
Extensions to Ada 2005
Assertion_Policy pragmas are now allowed in more
places and can specify behavior for individual kinds of assertions.
Wording Changes from Ada 2012
Added wording that preconditions and predicates
given on language-defined units are always checked unless suppressed
(that is, they act like language-defined checks). This is not considered
an inconsistency, since there are no such preconditions or predicates
in Ada 2012.
Correction: Added wording that postconditions,
type invariants, and default initial conditions given on language-defined
units cannot fail. This is not considered an inconsistency, since there
are no such postconditions, invariants, or default initial conditions
in Ada 2012.
Added default initial conditions to the kinds of
assertions (see 7.3.3).
Correction: Added a definition of assertion
aspects, used in some freezing rules (see 13.14).
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe