Pragma Assert_And_Cut (GNAT Reference Manual)

### 2.15 Pragma Assert_And_Cut ¶

Syntax:

    pragma Assert_And_Cut (
      boolean_EXPRESSION
      [, string_EXPRESSION]);

The effect of this pragma is identical to that of pragma `Assert`, except that in an `Assertion_Policy` pragma, the identifier `Assert_And_Cut` is used to control whether it is ignored or checked (or disabled).

The intention is that this be used within a subprogram when the given test expression sums up all the work done so far in the subprogram, so that the rest of the subprogram can be verified (informally or formally) using only the entry preconditions, and the expression in this pragma. This allows dividing up a subprogram into sections for the purposes of testing or formal verification. The pragma also serves as useful documentation.

This is an assertion kind pragma that can associate a set of its arguments with an assertion level. See SPARK 2014 Reference Manual, section 11.4.2.