# 11. Exceptions¶

## 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.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.