11.4.2 Pragmas Assert and Assertion_Policy
{
AI95-00286-01}
{
AI05-0274-1}
Pragma Assert is used to assert the truth of a
boolean Boolean expression at a any point within a sequence of declarations or statements. Pragma Assertion_Policy is used to control whether such assertions
are to be ignored by the implementation, checked at run-time, or handled
in some implementation-defined manner.
{
AI05-0274-1}
Assert pragmas, subtype predicates (see 3.2.4),
preconditions and postconditions (see 6.1.1),
and type invariants (see 7.3.2) 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 normally.
Glossary entry: 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: 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.
{
AI05-0274-1}
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.
Syntax
Name Resolution Rules
Reason: We allow
any boolean type to be like if_statements
and other conditionals; we only allow String for the message in order
to match raise_statements.
Legality Rules
{
AI95-00286-01}
{
AI05-0290-1}
The assertion_aspect_mark
of a pragma
Assertion_Policy shall be one of Assert, Static_Predicate, Dynamic_Predicate,
Pre, Pre'Class, Post, Post'Class, Type_Invariant, Type_Invariant'Class,
or some implementation defined aspect_mark.
The policy_identifier of a pragma
Assertion_Policy shall be either
Check, Ignore, or some an implementation-defined identifier.
Static Semantics
{
AI95-00286-01}
{
AI05-0290-1}
A pragma
Assertion_Policy determines for each assertion
aspect named in the pragma_argument_associations
whether assertions of the given aspect are to be enforced by a run-time
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;
the policy_identifier
Ignore requires that the assertion expression not be evaluated at these
points, and the run-time 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_references,
and if static, will still have an effect on loop iteration over the subtype,
and the selection of case_statement_alternatives
and variants.] is
a configuration pragma that specifies the assertion policy in effect
for the compilation units to which it applies. Different policies may
apply to different compilation units within the same partition. The default
assertion policy is implementation-defined.
{
AI05-0290-1}
If no assertion_aspect_marks
are specified in the pragma, the specified policy applies to all assertion
aspects.
{
AI05-0290-1}
A pragma
Assertion_Policy applies to the named assertion aspects in a specific
region, and applies to all assertion expressions 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.
{
AI05-0290-1}
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 policy.
{
AI95-00286-01}
The following language-defined library package
exists:
package Ada.Assertions is
pragma Pure(Assertions);
Assertion_Error : exception;
procedure Assert(Check : in Boolean);
procedure Assert(Check : in Boolean; Message : in String);
end Ada.Assertions;
{
AI95-00286-01}
{
AI05-0290-1}
A compilation unit containing a check
for an assertion (including a pragma
Assert) has
a semantic dependence on the Assertions library unit.
This paragraph was
deleted. {
AI95-00286-01}
{
AI05-0290-1}
The
assertion policy that applies to a generic unit also applies to all its
instances.
Dynamic Semantics
{
AI95-00286-01}
{
AI05-0290-1}
An
assertion policy specifies how a pragma
Assert is interpreted by the implementation. If the assertion policy
is Ignore at the point of a pragma
Assert, the pragma is ignored. If
performing checks is required by the
Assert assertion
policy in effect is
Check at the place point 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.
{
AI95-00286-01}
Calling the procedure Assertions.Assert without
a Message parameter is equivalent to:
if Check = False then
raise Ada.Assertions.Assertion_Error;
end if;
{
AI95-00286-01}
Calling the procedure Assertions.Assert with a
Message parameter is equivalent to:
if Check = False then
raise Ada.Assertions.Assertion_Error with Message;
end if;
{
AI95-00286-01}
The procedures Assertions.Assert have these effects
independently of the assertion policy in effect.
Bounded (Run-Time) Errors
{
AI05-0274-1}
It is a bounded error to invoke a potentially blocking
operation (see 9.5.1) 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.
Implementation Permissions
{
AI95-00286-01}
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.
{
AI95-00286-01}
Implementations may define their own assertion
policies.
{
AI05-0274-1}
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.]
{
AI05-0274-1}
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 C, 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.
2 {
AI95-00286-01}
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
{
AI95-00286-01}
Pragmas Assert and Assertion_Policy,
and package Assertions are new.
Incompatibilities With Ada 2005
{
AI05-0274-1}
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
behavior.
Extensions to Ada 2005
{
AI05-0290-1}
Assertion_Policy pragmas are
now allowed in more places and can specify behavior for invidivual kinds
of assertions.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe