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.