C.6  Loop Specifications

Synopsis

Description The optional clause invariant formula states that the state in which the loop checks the value of exp for the first time (the loop’s “prestate”) is related by formula

1. to the loop’s prestate itself and
2. to every state that arises immediately after the execution of the loop’s body (the body’s “poststate”).

If the clause is omitted, the formula is assumed to be “true”.

The optional clause decreases term states that

1. the value of term in the loop’s prestate and in every poststate of the loop’s body denotes a non-negative integer number, and that
2. the value of term immediately before the execution of the loop’s body is greater than the value of term after the execution of the loop’s body.

Consequently the loop cannot perform an infinite number of iterations.

If the clause has form decreases term₁,…,term_n with n > 1, then then the values of some term₁,…,term_i may remain the same while term_i+1 with i+1 ≤ n is decreased as described above (decreasing lexicographical ordering).

Pragmatics It should be noted that the formulation of the invariant above relates the loop’s prestate to the body’s poststate which, due to the existence of and in the formula language, may be considered as different from the prestate of the subsequent loop iteration, respectively, if the loop terminates, from the loop’s poststate. For instance, if the body executes a break statement, the loop’s prestate is related to the body’s poststate by the formula BREAKS@NEXT but to the loop’s poststate by EXECUTES@NEXT. The first formula is more precise since it describes that the loop terminates from the execution of the loop body which the second formula does not. Our formulation therefore allows to express stronger invariants.