Definicja 9.6.1

Powiemy, że zdanie α jest niezmiennikiem pętli postaci while γ do I od, gdzie γ jest warunkiem, a I treścią pętli, jeśli dla każdej iteracji tej pętli z tego, że warunki γ i α są spełnione przed wykonaniem treści pętli I, wynika że α jest prawdziwe po jej wykonaniu.

Rozważmy jeszcze raz algorytm Euklidesa, tym razem jednak zapisany przy pomocy pętli, a nie w sposób rekurencyjny. Korzystamy przy tym z tych samych praw, które wymieniliśmy w przykładzie 9.5.2. Założymy ponadto, że ani n ani m nie są równe 0.

NWD(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;
}

Łatwo zauważyć, że niezmiennikiem pętli w tym algorytmie jest formuła nwd(x,y) = nwd (n,m). Rzeczywiście, załóżmy że x ≠ y i formuła nwd(x,y) = nwd(n,m) jest prawdziwa w chwili wejścia do pętli while. Jeśli x>y, to na mocy przytoczonych w przykładzie 8.7 praw mamy nwd(x-y,y)=nwd(x,y). Wykonując jedyną przewidzianą w tym przypadku instrukcję x := x-y, spowodujemy (nową wartością x jest stara wartość x-y), że na nowo spełniona jest równość nwd(x,y)=nwd(n,m). Analogicznie w drugim przypadku. Zatem, po wykonaniu instrukcji "if" nadal jest spełniona formuła nwd(x,y) = nwd(n,m).

Zakończenie całego procesu nastąpi wówczas, gdy x=y. Stosując skończoną zasadę indukcji matematycznej, skoro nwd(x,y) = nwd(n,m) jest prawdziwa tuż przed wykonaniem pętli "while" i dla każdej iteracji z prawdziwości tej formuły przed wykonaniem instrukcji "if" wynika jej prawdziwość po wykonaniu instrukcji "if", to nwd(x,y)=nwd(n,m) jest też prawdziwa po wyjściu z pętli "while". Ale wtedy nwd(n,m) = nwd(x,y) = nwd(y,y) =y.

Wynika stąd, że wyliczona przez procedurę wartość jest rzeczywiście największym wspólnym dzielnikiem liczb n i m.

Pozostał jeszcze jeden mały problem, czy ten algorytm kiedykolwiek doprowadzi do sytuacji, w której x=y. Czy pętla "while" zatrzyma się kiedykolwiek? I tu znów przychodzi nam z pomocą indukcja matematyczna.

Zauważmy, że jeśli wartości x i y kolejno uzyskiwane w czasie działania algorytmu zapiszemy jako kolejne pozycje ciągu (x₁,y₁), (x₂,y₂),... , to iloczyn (x_i ∙y_i) tworzy ciąg malejący. Ponieważ jest to ciąg liczb naturalnych, zatem na mocy zasady minimum nie może być ciągiem nieskończonym. Istnieje więc taka iteracja, w której x_i=y_i, czyli algorytm zatrzyma się.

Lemat 9.6.1

Jeśli zdanie α jest prawdziwe przed wykonaniem instrukcji "while" i jest niezmiennikiem tej pętli, to po wykonaniu instrukcji "while" jest prawdziwe zdanie (α ∧ ¬ γ).