Pragma Loop_Variant (GNAT Reference Manual)

### 2.107 Pragma Loop_Variant ¶

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 interpreted 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.

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.