Loop invariant

As a loop invariant properties of a loop are referred to in an algorithm that is valid at a certain point in each loop, regardless of the number of their current runs. They are necessary for verification of algorithms and also help to understand the processes within a loop better. Typically, loop invariants describe value ranges of variables and relationships of the variables with each other.

Each loop can be found a statement that applies before and after the loop, eg a tautology such as " true = true". So it is always possible to specify an invariant, but this is not always suited to carry out a formal proof of correctness.

Correctness proof

In the correctness proof for an algorithm by means of a loop invariant is to show that the loop invariant at initialization, maintenance is adhered to ( at the end of a loop iteration ) and after completion of the loop. The correctness check can be split in two. For this one first checks whether it is seen at the first critical point, whether it is therefore initialized. Finally, it is checked whether it is retained in the transition from one step to the next. This procedure corresponds to the complete induction of mathematics. At all three time points, the loop invariant must be correct, that is, variables must lie approximately within defined ranges. In addition, for example, may input array at a sorting method can not be changed in terms of value, but only the order may be adjusted.

It is proved that there is no algorithm that determines a loop invariant automatically.

Example

The following algorithm multiplies the two variables a and b to each other:

Multiply ( a, b) {     x: = a;     y: = b;     p: = 0;     / / The invariant must hold before the loop     while x > 0 do {        p: = p y;        / / Inside the loop, the invariant does not apply,        / / (X * y) p = a * b is not satisfied this point        x: = x - 1;        / / The invariant must hold at the end of each Durlaufs ...     }     / / ... So directly after the loop     return p   } A loop invariant for this algorithm is: