Algorytm Euklidesa

(* Algorytm Euklidesa inaczej, zauważ, że w tym algorytmie jedyną operacją jest dodaj jeden, jedynym predykatem jest równość. *)

(* Dane: x>0 i y>0 liczby naturalne *)

[math]\color{blue}\mathbf{Deklaracje: }\ typ(x, y, n, m, r, q, max)=\mathbb{N}\ \land\ typ(n\_mniejsze)=Boolean [/math]

(* Wynik: nwd(x,y) *)

n:=x; m:=y;

while n ≠ m do

[math]\color{red}\mathbf{Oznaczenie}\ niech\ l=max(n,m) [/math]

r:=0;

while r ≠n and r ≠m

do

r:=r+1

od;

if r=n then n_miejsze:=true; max:=m else n_mniejsze:=false; max:=n fi;

[math]\color{blue}\mathbf{Stwierdzenie}\ (n\ltm \wedge m=max(n,m) \vee m\ltn \wedge n=max(n,m)) [/math]

q:=0;

while r≠max

do

r:= r+1; q:=q+1

od;

[math]\color{blue}\mathbf{Stwierdzenie}\ q = |m-n| \land (1 \leq q \lt max(n,m))\land r=max(n,m) [/math]

if n_mniejsze then m:=q else n := q fi

[math]\color{blue}\mathbf{Stwierdzenie}\ max(n,m) \lt \color{red}l [/math]

od ( wynik = n)

przejdź do analizy algorytmu Euklidesa