Pragma Loop_Invariant (GNAT Reference Manual)

### 2.105 Pragma Loop_Invariant ¶

Syntax:

    pragma Loop_Invariant ( boolean_EXPRESSION );

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

`Loop_Invariant` can only appear as one of the items in the sequence of statements of a loop body, or nested inside block statements that appear in the sequence of statements of a loop body. The intention is that it be used to represent a “loop invariant” assertion, i.e. something that is true each time through the loop, and which can be used to show that the loop is achieving its purpose.

Multiple `Loop_Invariant` and `Loop_Variant` pragmas that apply to the same loop should be grouped in the same sequence of statements.

To aid in writing such invariants, the special attribute `Loop_Entry` may be used to refer to the value of an expression on entry to the loop. This attribute can only be used within the expression of a `Loop_Invariant` pragma. For full details, see documentation of attribute `Loop_Entry`.

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.