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.