2.16 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 expresion 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.