main08

Definition 8.6.1

We say that a proposition α is an invariant of the loop while γ do I od, where γ is a loop's condition and I is a loop's body, when for every iteration of this loop whenever providing that conditions γ and α are satisfied before loop's body is executed, α is satisfied after loop's body is executed.

Let's consider again the Euclid's algorithm, but this time we implement it with an iterative loop (instead of a recursive procedure). We assume that the arithmetic formulas introduced in example 8.5.2 are still valid and that both n and m are not equal to 0.

gcd(n,m)

{x:=n; y := m;
while x ≠ y do
if x>y then
x := x-y else
y:=y-x fi od;
return y;
}

It is easy to be derived that this algorithm loop's invariant has the following form:

In order to prove its correctness let's assume that x ≠ y and the formula nwd(x,y) = nwd(n,m) is satisfied while program is entering the loop. If x>y then, according to arithmetic rules, from the example 8.5.2 we obtain nwd(x-y,y) = nwd(x,y). Now the program only carry out one instruction x := x-y and this step causes that the equality nwd(x,y) = nwd(n,m) is again valid (new value of x is old value of x-y). Similarly, we can analyse the second case (i.e. y := y-x). Therefore, after the "if" instruction, the invariant nwd(x,y) = nwd (n,m) is still valid.

The loop's end is reached when x = y. According to the finite induction principle, if nwd(x,y) = nwd(n,m) is satisfied just before the loop entrance, and for every loop iteration, providing that this formula is satisfied before the instruction "if", it follows that the formula is correct after the instruction "if", then nwd(x,y) = nwd(n,m) is also valid after the execution of the loop "while". Thus, nwd(n,m) = nwd(x,y) = nwd(y,y) = y.

It follows that the value of gcd(n,m) calculated by the algorithm is in fact the greatest common divisor for the given numbers n and m.

Let us consider now the problem if this algorithm ever stops (i.e. whether it leads after a finite number of iterations to x = y). This time we can use mathematical induction too.

Take into consideration the sequence (x₁,y₁), (x₂,y₂),... , where x and y are successive values of x and y. The products (x_i * y_i) for i =1,2,... is a decreasing sequence of natural numbers. Hence, according to the minimum principle, it can not be infinite. Thus, there is such iteration which causes x_i = y_i, i.e. the termination of the considered algorithm.

Lemma 8.6.1

If the proposition α is valid before the entrance to the loop instruction "while", and if it is this loop's invariant, then after executing the loop "while" the formula (α ∧¬ γ) is valid.