11. Exceptions

11.1. Exception Declarations

No additions or restrictions

11.2. Exception Handlers

Legality Rules

  1. Exception handlers are not permitted in SPARK.

11.3. Raise Statements

Raise statements are in SPARK, but must (as described below) be provably never executed.

Verification Rules

  1. A raise_statement introduces an obligation to prove that the statement will not be executed, much like the verification condition associated with

    pragma Assert (False);

    [In other words, the verification conditions introduced for a raise statement are the same as those introduced for a run-time check which fails unconditionally.]

11.4. Exception Handling

No additions or restrictions but exception handlers are not permitted in SPARK.

11.4.1. The Package Exceptions

11.4.2. Pragmas Assert and Assertion_Policy

Legality Rules

  1. The pragmas Assertion_Policy, Suppress, and Unsuppress are allowed in SPARK, but have no effect on the generation of verification conditions. [For example, an array index value must be shown to be in bounds regardless of whether Index_Check is suppressed at the point of the array indexing.]

  2. The following SPARK defined aspects and pragmas are assertions and their Boolean_expressions are assertion expressions:

    • Assert_And_Cut;

    • Assume;

    • Contract_Cases;

    • Default_Initial_Condition;

    • Initial_Condition;

    • Loop_Invariant;

    • Loop_Variant; and

    • Refined_Post.

    There is an assertion_aspect_mark for each of these aspects and pragmas with the same identifier as the corresponding aspect or pragma. In addition, Ghost is a SPARK defined assertion_aspect_mark.

    An implementation may introduce further implementation defined assertion_aspect_marks some of which may apply to groups of these assertions.