Informatyka MIMUW

Całkowita poprawność programów

Mnożenie chłopów rosyjskich

Rozważmy następujący program:

program ChlopiRosyjscy(x0,y0:Integer);
var x,y,z:Integer;
 begin
 x:=x0; y:=y0; z:=0;
 while x<>0 do
 begin
if odd(x) then z:=z+y;
x:= x div 2;
y:=y+y
end;
Write(z)
end.

Fragment ten wyznacza pewną wartość z w zależności od początkowych wartości x0,y0. Spróbujmy określić tę zależność. Przeprowadźmy symulację dla paru wartości początkowych. Przekonamy się szybko, że np. dla pary wartości (x0,y0) równej (3,7) wynikiem jest 21, dla (5,6) wynikiem jest 30 i tak na oko końcowa wartość z jest wynikiem mnożenia x0 przez y0. Czy można ten fakt udowodnić?

Nazwa algorytmu pochodzi stąd, że etnografowie znaleźli na Syberii obszary, w których chłopi właśnie w ten sposób mnożyli w pamięci. Czy słusznie?

Znalezienie niezmiennika nie jest oczywiste, ale możliwe. Oto ten sam program z asercjami ułatwiającymi udowodnienie częściowej poprawności.

program ChlopiRosyjscy(x0,y0:Integer); 
var x,y,z:Integer;
begin 
x:=x0; y:=y0; z:=0; {x=x0, y=y0, z=0} 
while x<>0 do {z+xy=x0y0} begin 
if odd(x) then z:=z+y;
 {(odd(x) \( \land \) z-y+xy=x0y0) \( \lor (\neg \)odd(x)\( \land \) z+xy=x0y0)
 x:= x div 2; 
{z+2xy=x0y0}
 y:=y+y 
{z+xy=x0y0}
 end; 
{z=x0y0}
 Write(z)
end.

Łatwo się przekonać, że

1. Niezmiennik z+xy=x0y0 inicjalizuje się dobrze po początkowych przypisaniach x:=x0; y:=y0; z:=0.
2. Z niezmiennika z+xy=x0y0 i zaprzeczenia dozoru x=0 wynika natychmiast warunek końcowy z=x0y0.
3. Niezmiennik z+xy=x0y0 odtwarza się po każdym obrocie pętli. Ten ostatni fakt może nie jest tak oczywisty, więc parę słów wyjaśnienia. Po pierwsze musimy przypomnieć sobie, że x div 2=x/2, gdy x jest parzyste oraz że x div 2=(x-1)/2, gdy x jest nieparzyste. Jeśli na początku pętli x jest parzyste, to pierwsza instrukcja jest równoważna pustej i w oczywisty sposób niezmiennik pozostaje prawdziwy. Po wykonaniu x:=x div 2 prawdziwy jest warunek z+2xy=x0y0, gdyż x jest już dokładnie dwa razy mniejsze (zgodnie z regułą dowodzenia dla instrukcji przypisania), a po wykonaniu instrukcji y:=y+y mamy z+2x(y/2)=x0y0, czyli niezmiennik odtwarza się. Jeśli natomiast na początku pętli x jest nieparzyste, to najpierw wykona się instrukcja z:=z+y, po której będzie spełniony warunek z-y+xy=x0y0. Teraz wykonanie instrukcji x:=x div 2 spowoduje, że będzie spełniony warunek z-y+(2x+1)y=x0y0, co jest równoważne warunkowi z+2xy=x0y0, co po przypisaniu y:=y+y doprowadza nas z powrotem do z+xy=x0y0, a to jest odtworzony niezmiennik.

Zatem pokazaliśmy, że nasz program jest częściowo poprawny dla każdych początkowych wartości x oraz y. Dla każdych dlatego, że nie zakładaliśmy niczego o wartościach początkowych x0 i y0. Teraz niespodzianka! Zbadajmy, jak zachowuje się program dla danych ujemnych. Jeżeli x0 jest dodatnie, a y0 ujemne, nie ma problemu. Jeśli jednak x0 będzie ujemne, mamy kłopot. Zobaczmy na przykład, jakie wartości pojawią się kolejno dla danych początkowych x0=-5, y0=2.

Widać, że program się zapętla. Wartość x zawsze będzie równa -1, gdyż zachodzi (-1) div 2 = -1. Zauważmy, że program jest nadal częściowo poprawny, gdyż z definicji każdy pętlący się program taki jest. Przy okazji zweryfikujmy poprawność naszego niezmiennika. W każdym wierszu tabeli, reprezentującym stan obliczeń na początku pętli, wartość wyrażenia z+xy jest stała i równa -10, czyli x0y0.

Rzecz jasna musimy wrócić do pytania jak wymusić zatrzymanie się programu: gdyby bowiem program był częściowo poprawny, a do tego wiedzielibyśmy, że program zatrzyma się, mielibyśmy gwarancję uzyskania żądanego wyniku. Jak zatem wywnioskować, czy program się zatrzyma?

Metoda Floyda dowodzenia warunku stopu

Metoda ta opracowana przez Roberta Floyda w latach sześćdziesiątych korzysta z zasady indukcji. Pomysł jest następujący. Chodzi o pokazanie, że pewna wartość, mówiąc intuicyjnie, maleje w każdym obrocie pętli, a zmniejszanie to nie może się ciągnąć w nieskończoność. Aby przedstawić tą metodę możliwie ogólnie, wprowadźmy pojęcie relacji dobrze ufundowanej. Załóżmy, że mamy określoną relację dwuargumentową r w zbiorze A.

Definicja 1
Łańcuchem relacji r nazwiemy każdy skończony bądź nieskończony ciąg \( a=a_1,a_2,\ldots \) elementów z A taki, że dla każdych \( a_i,a_{i+1} \) należących do \( a \) zachodzi \( (a_i,a_{i+1})\in r \). Czyli kolejne wyrazy ciągu są ze sobą w relacji r.

Definicja 2

Powiemy, że relacja r jest dobrze ufundowana (ang. well founded) w zbiorze A wtedy i tylko wtedy, gdy nie istnieje nieskończony łańcuch relacji r w zbiorze A.

Jeśli relacja r jest dobrze ufundowana w zbiorze A, taki zbiór nazwiemy dobrze ufundowanym (przez relację r).

Najprostszym zbiorem dobrze ufundowanym jest zbiór liczb naturalnych z relacją \( > \). Istotnie nie można w nieskończoność pomniejszać liczb naturalnych. Oczywiście relacja \( \ge \) dobrze ufundowana nie jest w tym zbiorze: można stworzyć nieskończony łańcuch składający się choćby z samych zer. Widać, że relacja dobrze ufundowana musi być przeciwzwrotna.

Będziemy się teraz starali znaleźć odwzorowanie wartości zmiennych w zbiór dobrze ufundowany tak, aby kolejne wartości tego odwzorowania dla kolejnych obrotów pętli tworzyły łańcuch. Jeśli się nam to uda, to bedzie to oznaczało, że pętla musi się zatrzymać po skończonej liczbie kroków. W naszych przykładach typowym zbiorem dobrze ufundowanym będzie właśnie zbiór liczb naturalnych z relacją większości.

W przypadku algorytmu mnożenia chłopów rosyjskich taką funkcją będzie \( f(x,y,z)=x \). Pokażemy, że jeśli początkowa wartość x jest dodatnia, to po jednym obrocie pętli kolejna wartość jest mniejsza od poprzedniej. Jest to oczywisty fakt związany z funkcją dzielenia przez 2. Mamy bowiem dla x>0 \( x \div 2 \le x/2 < x \). Dla pełności dowodu warto tu dodać do niezmiennika warunek \( x\ge 0 \). Dlaczego nie \( x>0 \)? Bo nie dałoby się go udowodnić. Po prostu przy wyjściu z pętli x=0, więc warunek ten nie byłby spełniony. Zauważmy, że nie ma problemu z dowodem ostrej większości kolejnych wartości, gdyż nigdy nie wejdziemy do pętli jeśli x=0. Dozór pętli zapewnia nam bowiem, że \( x\neq 0 \), co w połączeniu z niezmienniczym \( x\ge 0 \) daje \( x>0 \), a to już wystarcza do ostrej nierówności z następną wartością x.

To czego brakuje to poprawna inicjalizacja niezmiennika. Aby był on spełniony na samym początku, konieczne jest, żeby x było nieujemne. Zatem podany program jest całkowicie poprawny dla wszystkich par (x0,y0) takich, że \( x0\ge 0 \). Nadmieńmy, że program nie wykonuje żadnych operacji mogących spowodować błąd, więc zawsze zakończy się dając poprawny wynik.

Wyszukiwanie binarne

Gdyby trzeba było wybrać najważniejszy algorytm w całej informatyce, to wybrałbym chyba algorytm wyszukiwania binarnego. Dzięki niemu jesteśmy w stanie szybko odnajdywać dane w posortowanym ciągu. Załóżmy tu, że w tablicy A:array[1..n] of Integer mamy posortowane niemalejąco liczby całkowite. Naszym zadaniem jest stwierdzić, czy pośród nich znajduje się liczba x. Wykorzystamy tu następujący pomysł. Porównamy wartość x ze środkowym elementem tablicy A[(n+1) div 2]. I teraz albo x będzie od niego większy i wtedy na pewno x-a nie ma na lewo od tego elementu, albo będzie mniejszy lub równy i wtedy jeśli jest, to tylko w lewej połówce tablicy. Zatem możemy za pomocą jednego sprawdzenia sprowadzić zadanie do dwa razy mniejszego rozmiaru. Oto rozwiązanie:

l:=1; p:=n;
<b>while</b> (l &lt; p) <b>do</b>
 <b>begin</b>
 s:=(l+p) <b>div</b> 2;
 <b>if</b> x &gt; A[s] <b>then</b> l&nbsp;:= s+1
 <b>else</b>
 p&nbsp;:=s 
<b>end</b>;
jest&nbsp;:= x = A[l] 
</pascale>
 
<p>Zróbmy parę spostrzeżeń. Po pierwsze, nie sprawdzamy nigdzie, czy przypadkiem A[s] nie równa się x, tylko doprowadzamy za każdym razem do momentu, w którym badany przedział jest jednoelementowy. Moglibyśmy sprawdzić czy A[s]=x wprowadzając dodatkowe sprawdzenie, ale czy to się opłaca, przedyskutujemy później. Po drugie, wybraliśmy akurat ostrą nierówność prowadzącą do przesunięcia indeksu l na prawo od s i wydaje się na pierwszy rzut oka, że równie dobrze byłoby sprawdzić nieostrą nierówność, zastępując instrukcję warunkową następującą: </p> 
 
<pascal>
<b>if</b> x&gt;=A[s] <b>then</b> l:=s
 <b>else</b> p:=s-1

Sytuacja wygląda na zupełnie symetryczną. Przekonamy się za chwilę, że wcale tak nie jest.

Udowodnijmy poprawność tego fragmentu kodu. Ustalmy, że predykat Sort(A) mówi nam o tym, że tablica A jest posortowana niemalejąco.

l:=1; p:=n;
 <b>while</b> l &lt; p <b>do</b> {Sort(A) \( \land (1\le l\le p\le n) \land \exists (1\le k \le n: A[k]=x \Leftrightarrow \exists (l\le k \le p: A[k]=x)} \) 
<b>begin</b> 
s:=(l+p) <b>div</b> 2;
 if x &gt; A[s] <b>then</b> l:=s+1 
<b>else</b> p:=s
 <b>end</b>;
 jest&nbsp;:= x=A[l]

Niezmiennik mówi nam, że po pierwsze tablica jest posortowana cały czas, po drugie indeksy l oraz p są w zakresie indeksów tablicy i że l nie przekracza p, a trzecia część niezmiennika mówi nam, że jeśli element x jest gdzieś w tablicy, to jest między indeksami l oraz p.

Zauważmy, że niezmiennik inicjalizuje się dobrze, jeśli tylko \( 1\le n \) i jest to warunek, który musimy tu dodać jako warunek wstępny na dane (przy okazji sprawdźmy, że jest to warunek konieczny poprawności programu; dla n=0 dostalibyśmy błąd!). Po drugie ze względu na to, że dla \( k>1 \) zachodzi \( 1\le k \div 2 < k \) otrzymujemy nierówność \( l\le (l+p) \div 2 < p \) i ta ostatnia ostra nierówność jest bardzo istotna. Zauważmy więc, że przypisując zmiennej l wartość (l+p) div 2 +1 otrzymujemy wartość ostro większą od l, a przypisując zmiennej p wartość (l+p) div 2 otrzymujemy wartość mniejszą ostro od p. Zatem funkcja F(l,p)=p-l ma wartości w zbiorze liczb naturalnych i maleje z każdym obrotem pętli. Czyli pętla zawsze się zakończy.

Odtworzenie się trzeciego warunku niezmiennika też jest dość oczywiste, gdyż jeśli x>A[s], to ze względu na przechodniość relacji większości mamy x>A[k] dla 1<=k<s, więc jeśli istnieje x w tablicy, to istnieje między s+1 a p. Gdy zaś x<=A[s], wówczas jeśli istnieje x w tablicy, to w szczególności znajdziemy je w przedziale 1..s, zatem przypisanie p:=s nadal utrzymuje w prawdziwości ten warunek.

Powstaje pytanie czy zaprzeczenie dozoru w połączeniu z niezmiennikiem da nam końcowy warunek \( A[l]=x \Leftrightarrow \exists 1\le k \le n: A[k]=x \)? Jeśli tak, to ostatnie przypisanie ustali nam wartość zmiennej jest na to, czego chcemy, czyli \( \exists 1\le k \le n: A[k]=x \).

Spróbujmy przerachować. Zaprzeczenie dozoru to l>=p. W połączeniu z niezmiennikiem daje nam l=p. Z niezmiennika wiemy, że warunek \( \exists 1\le k \le n: A[k]=x \) jest równoważny warunkowi \( \exists l\le k \le p: A[k]=x \), ale że l=p, to jest to równoważne warunkowi A[l]=x.

Możemy się przekonać, że tak znaleziona wartość x będzie zawsze pierwsza od lewej. Jak to pokazać? Bardzo prosto. Wystarczy do niezmiennika dodać warunek \( \forall 1\le k < l: A[k]\neq x$ \). Widzimy, że inicjalizacja jest dobra (dla l=1 warunek ten jest trywialnie spełniony), odtworzenie warunku po każdym obrocie jest oczywiste: tylko gdy l się zmienia ten warunek mógłby zajść, a l zmienia się na s+1 tylko wtedy, gdy x>A[s], więc na lewo od s+1 nie ma x-ów. Zatem przy wyjściu z pętli również mamy niezmiennik spełniony, a ten nam gwarantuje, że na lewo od l nie ma żadnej wartości x. Czyli jeśli znaleźliśmy x, to jest on pierwszy od lewej.

Czytelnikom jako ćwiczenie pozostawiamy sprawdzenie, czy symetryczna wersja wyszukiwania binarnego jest błędna. Program zapewne się zapętli. Jest to bardzo częsty błąd popełniany przy kodowaniu tego algorytmu.