x=x0; y=y0; z=0;

// α = (x=x0, y=y0, z=0)

while (x!=0) // x0*y0 = z+xy

{ if (x%2)

z+=y;

// x0y0=z+(x/2)*2y

x/=2;

// x0y0=z+x*2y

y+=y;

// x0y0=z+xy

}

// z=f(x0,y0)

gdzie f(x,y)=xy

α{P}β - fomuła logiki Hoare'a, której znaczenie jest następujące:

Jeżeli dane wejściowe spełniają warunek α, to jeśli program P zakończy swoje działanie bezbłędnie dla tych danych, to dane wyjściowe będą spełniały warunek β.

Taka formuła nazywa się formułą częściowej poprawności.

Powiemy, że program P jest całkowicie poprawny względem warunków α, β wtedy i tylko wtedy, gdy jest względem nich częściowo poprawny, oraz dla każdych danych spełniających warunek α zakończy swoje działanie i to bez błędu.

Ja stwierdzić to, że program się zakończy?

Określamy funkcję f(x1,...,xn) w zbiór dobrze ufundowany (np. (N,>)) w taki sposób, aby wartości tej funkcji w kolejnych obrotach pętli tworzyły kolejne elementy łańcuchów.

W naszym przypadku dla x>=0 taką funkcją może być funkcja

f(x,y,z,x0,y0) = x

w zbiór (N,>).

Funkcja ta spełnia nasze założenia, bowiem ilekroć wchodzimy do pętli wiemy, że x>0, a dla x'ów dodatnich wartość x/2 jest ostro mniejsza od x.

Zauważmy, że funkcja f(x,y,z,x0,y0)=|x| nie byłaby dobrą funkcją dla dowolnych liczb całkowitych, gdyż (-1)/2=-1, zatem kolejne wartości przyjmowane przez zmienną x nie będą w relacji dobrego ufundowania dla x=-1, bo -1 nie jest większe od -1.

Zatem nasz algorytm nie jest poprawny dla x'ów ujemnych.

---