Syntax:
pragma Loop_Variant ( LOOP_VARIANT_ITEM {, LOOP_VARIANT_ITEM } );
LOOP_VARIANT_ITEM ::= CHANGE_DIRECTION => discrete_EXPRESSION
CHANGE_DIRECTION ::= Increases | Decreases
Loop_Variant 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. It allows the specification of quantities which must always decrease or increase in successive iterations of the loop. In its simplest form, just one expression is specified, whose value must increase or decrease on each iteration of the loop.
In a more complex form, multiple arguments can be given which are intepreted in a nesting lexicographic manner. For example:
pragma Loop_Variant (Increases => X, Decreases => Y);
specifies that each time through the loop either X increases, or X stays the same and Y decreases. A Loop_Variant pragma ensures that the loop is making progress. It can be useful in helping to show informally or prove formally that the loop always terminates.
Loop_Variant is an assertion whose effect can be controlled using an Assertion_Policy with a check name of Loop_Variant. The policy can be Check to enable the loop variant check, Ignore to ignore the check (in which case the pragma has no effect on the program), or Disable in which case the pragma is not even checked for correct syntax.
Multiple Loop_Invariant and Loop_Variant pragmas that apply to the same loop should be grouped in the same sequence of statements.
The Loop_Entry attribute may be used within the expressions of the Loop_Variant pragma to refer to values on entry to the loop.