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.