Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
Annotated Ada Reference Manual (Ada 2022)Legal Information
Contents   Index   References   Search   Previous   Next 

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 expression at a point within a sequence of declarations or statements.
 {AI05-0274-1} {AI12-0265-1} Assert pragmas, subtype predicates (see 3.2.4), preconditions and postconditions (see 6.1.1),  and 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.
Term entry: assertion — boolean expression that is expected to be True at run time at certain specified places
Note: Certain pragmas and aspects define various kinds of assertions.
 {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. 


{AI95-00286-01} The form of a pragma Assert is as follows: 
  pragma Assert([Check =>] boolean_expression[, [Message =>] string_expression]);
A pragma Assert is allowed at the place where a declarative_item or a statement is allowed.
{AI95-00286-01} The form of a pragma Assertion_Policy is as follows: 
  pragma Assertion_Policy(policy_identifier);
{AI05-0290-1}   pragma Assertion_Policy(
         assertion_aspect_mark => policy_identifier
     {, assertion_aspect_mark => policy_identifier});
{AI05-0290-1} A pragma Assertion_Policy is allowed only immediately within a declarative_part, immediately within a package_specification, or as a configuration pragma.

Name Resolution Rules

{AI95-00286-01} The expected type for the boolean_expression of a pragma Assert is any boolean type. The expected type for the string_expression of a pragma Assert is type String. 
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} {AI12-0265-1} {AI12-0396-1} The assertion_aspect_mark 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 defined aspect_mark. The policy_identifier shall be either Check, Ignore, or some implementation-defined identifier.
Implementation defined: Implementation-defined policy_identifiers and assertion_aspect_marks allowed in a pragma Assertion_Policy.
To be honest: {AI12-0396-1} “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. 

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 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; the policy_identifier 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_references, and if static, will still have an effect on loop iteration over the subtype, and the selection of case_statement_alternatives and variants.]
  {AI05-0290-1} If no assertion_aspect_marks are specified in the pragma, the specified policy applies to all assertion aspects.
  {AI05-0290-1} {AI12-0396-1} A pragma Assertion_Policy applies to the named assertion aspects in a specific region, and applies to all assertion expressions associated with those aspects 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.
  {AI05-0290-1} If a pragma Assertion_Policy applies to a generic_instantiation, then the pragma Assertion_Policy applies to the entire instance.
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:
{AI12-0414-1} package Ada.Assertions is
    with pragma Pure is(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}

Dynamic Semantics

{AI95-00286-01} {AI05-0290-1} 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.
{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} {AI12-0439-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 can might result in deadlock or a (nested) protected action.

Implementation Requirements

  {AI12-0179-1} {AI12-0265-1} 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).
Ramification: The 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). 
  {AI12-0179-1} {AI12-0265-1} 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.
Ramification: In other words, evaluating such an assertion expression will not return a result of False, nor will it propagate an exception other than by evaluating a raise_expression 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.
  {AI12-0112-1} 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.
Reason: {AI12-0005-1} {AI12-0112-1} 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. 

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} {AI12-0445-1} If the result of a function call in an assertion is not used 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} {AI12-0444-1} An implementation may disallow 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 can could produce a different value. Similarly, an implementation may disallow 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 can could produce a different value than in the case when 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

{AI12-0005-1} 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.
NOTE   {AI95-00286-01} {AI12-0442-1} {AI12-0447-1} 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 individual kinds of assertions. 

Wording Changes from Ada 2012

{AI12-0112-1} 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.
{AI12-0179-1} {AI12-0265-1} 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.
{AI12-0265-1} Added default initial conditions to the kinds of assertions (see 7.3.3).
{AI12-0396-1} Correction: Added a definition of assertion aspects, used in some freezing rules (see 13.14).

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe