pragma Assert_And_Cut ( boolean_EXPRESSION [, string_EXPRESSION]);
The effect of this pragma is identical to that of pragma
except that in an
Assertion_Policy pragma, the identifier
Assert_And_Cut is used to control whether it is ignored or checked
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.