Co to znaczy, że algorytm działa poprawnie? Intuicja podpowiada nam, że chodzi tu o to, by dla dowolnych danych uzasadnić zgodność uzyskanych wyników z zamierzeniami. Aby jednak taką zgodność ustalić ponad wszelką wątpliwość, musimy jasno sformułować intencje, podać tzw. specyfikację algorytmu.

Specyfikacją algorytmu nazywać będziemy parę własności: <wp, wk>, gdzie wp jest warunkiem początkowym, a wk warunkiem końcowym. Intuicyjnie, warunek początkowy to ten, który mają spełniać dane początkowe, a warunek końcowy to ten, który ma być spełniony po wykonaniu algorytmu. Ogólnie, oba warunki powinny opisywać zależności między zmiennymi przed i po wykonaniu algorytmu.

Przykład 4.1 

Rozważmy problem znalezienia elementu największego w danym ciągu liczb naturalnych x₁,..., x_n. Naturalnym warunkiem początkowym będzie założenie  niepustości ciągu: nie można znaleźć elementu największego w zbiorze pustym. Możemy go zapisać w postaci: wp = {n>0}. Warunek końcowy, natomiast, powinien charakteryzować oczekiwany wynik i może mieć postać: wk = {result = x_i dla pewnego i £ n oraz dla wszystkich i, x_i £ result}. Algorytm rozwiązujący ten problem możemy zapisać w postaci:

Łatwo zauważyć, że po wykonaniu tego algorytmu w strukturze liczb naturalnych, wartością zmiennej result jest rzeczywiście element największy ciągu, czyli po wykonaniu algorytmu spełniony jest warunek końcowy wk. Warunek wk, podany w przykładzie 4.1., wydaje się być rozsądnym z punktu widzenia badanego problemu. Jest jednak jasne, że dla jednego algorytmu można zaproponować wiele różnych par postaci <wp, wk>, nie każda jest jednak dla nas interesująca, np.: para formuł

wp = {n>0},  wk = {i =(n+1)},

chociaż opisuje własności zmiennych występujących w algorytmie max, nie daje nam dostatecznej informacji o tym, czego mamy się spodziewać po wynikach i co właściwie robi ten algorytm.  Specyfikacja ma precyzować problem, ma umożliwić  odpowiedź na pytanie, czy algorytm rozwiązuje postawiony problem, czy nie. Specyfikacja ma opisać co ma robić algorytm, jednak bez wskazywania, jak ma to robić.

Podkreślmy jeszcze raz, że jeśli algorytm Alg jest całkowicie poprawny ze względu na specyfikację <wp, wk>, to warunek początkowy daje gwarancję, że algorytm zakończy obliczenie. Tak właśnie jest w przykładzie 4.1: algorytm max zatrzymuje się dla dowolnych danych w strukturze liczb naturalnych. Rzeczywiście, zmienna i, kontrolująca pętlę, przyjmuje jako swoje wartości kolejne liczby naturalne, a parametr n też jest liczbą naturalną. Zatem po skończonej liczbie kroków zmienna i przyjmie wartość n.

Co więcej, po wykonaniu algorytmu spełniony jest warunek ("i)(x_i £ result):  W pętli "while" każdy element ciągu jest porównywany z elementem result. Jeśli po przejrzeniu i-pierwszych elementów ciągu, result ma wartość największego z nich, to w następnym kroku, result przyjmie wartość największego elementu wśród pierwszych (i+1) elementów: max{max{x₁,..., x_i}, x_i+1} = max{x₁,..., x_i+1}. Ponieważ, dla ciągu o długości 1, wartością zmiennej result jest element największy (ten jedyny element ciągu), to, na mocy zasady indukcji matematycznej, dla ciągu dowolnej długości n, po zakończeniu pętli "while", wartością result będzie element największy ciągu x₁,...,x_n.

Łatwo zauważyć, że nie są tu istotne wartości elementów ciągu, ani ich typy. To samo rozumowanie możemy powtórzyć dla ciągów o elementach z dowolnej liniowo uporządkowanej przestrzeni, byle tylko n było liczbą naturalną. Prawdziwe jest więc ogólniejsze twierdzenie sformułowane jako lemat 4.1.

Nie zawsze można znaleźć dostatecznie silny warunek początkowy, który gwarantowałby zatrzymywanie się programu. Nie zawsze też zależy nam na tym. W takich przypadkach zadowolimy się częściową poprawnością algorytmu.

Wprost z przyjętych definicji wynika, że całkowita poprawność algorytmu implikuje jego częściową  poprawność ze względu na tę samą specyfikację. Nie jest jednak odwrotnie, jak pokazuje następujący przykład.

Przykład 4.2

Rozważmy następujący algorytm sqrt_1, którego zadaniem ma być obliczenie pierwiastka kwadratowego z liczby x. Będziemy go rozważać w strukturze liczb rzeczywistych, to znaczy, że operacje użyte w tym algorytmie są operacjami w zbiorze liczb rzeczywistych, a zmienne przyjmują wyłącznie wartości rzeczywiste. Niech specyfikacja algorytmu ma postać:

wp = {x>0},        wk = {result = Öx}.

Proste eksperymenty z tym algorytmem pokażą, że dla x=4 wynikiem jest 2, dla x=16 wynikiem jest 4. itd. Można udowodnić, że dla dowolnego x postaci n², wynikiem programu jest n. W strukturze liczb rzeczywistych, ten algorytm nie zawsze się jednak zatrzymuje. Wystarczy przyjąć jakąkolwiek liczbę całkowitą postaci n² + 1. Po żadnej liczbie kroków nie otrzymamy warunku reszta=0. Wynika stąd, że algorytm sqrt jest częściowo poprawny ze względu na podaną specyfikację w strukturze liczb rzeczywistych, ale nie jest całkowicie poprawny.

Uwaga Gdybyśmy nieco zmodyfikowali algorytm, wstawiając w pętli warunek not(reszta > i) zamiast obecnego testu, to otrzymany algorytm byłby całkowicie poprawny w strukturze liczb rzeczywistych ze względu na specyfikację < x>0, result = [Öx]}>.

Analiza częściowej  i całkowitej poprawności  programu nie jest rzeczą banalną. Samo zrozumienie jak "działa" instrukcja przypisania często nastręcza dużo kłopotów.

Przykład 4.3

Instrukcja {x:= 5;} ma oczywiste konsekwencje: po jej wykonaniu wartością x jest 5, a wartość żadnej innej zmiennej nie ulega zmianie. Jeżeli instrukcja przypisania ma postać {x := x+ 5;}, to po wykonaniu tej instrukcji wartość zmiennej x zwiększyła się o 5 w stosunku do starej wartości x. Skomplikujmy teraz nieco sytuację   zakładając, że x > y (wartość zmiennej x jest większa od wartości pewnej zmiennej y) tuż przed wykonaniem instrukcji {x := x+5;}. Jaka zależność między x i y jest spełniona po wykonaniu tej instrukcji? Warto się samodzielnie zastanowić nad tym pytaniem i dlatego odpowiedź jest ukryta pod przyciskiem.

Dowodzenie poprawności złożonego algorytmu jest bardziej skomplikowane. Będziemy postępowali zgodnie z ideą Floyda opisów programów. Skorzystamy przy tym ze strukturalnej budowy algorytmu. Aby udowodnić poprawność algorytmu postaci {P1;P2;} ze względu na specyfikację <wp, wk>, będziemy się starali znaleźć taką własność pośrednią a, że algorytm {P1} jest poprawny ze względu na specyfikację <wp, a>, a algorytm {P2} jest poprawny ze względu na specyfikację <a, wk>.

Jeszcze gorzej jest w przypadku, gdy program zawiera pętle.  Jedną z metod analizy algorytmów stosowanych w tym wykładzie, jest metoda niezmienników Hoare. Przypomnijmy najpierw definicję niezmiennika.

Przykład 4.4

Problem: Znaleźć największy wspólny dzielnik dwóch danych liczb naturalnych x, y. Niech specyfikacja poszukiwanego algorytmu ma postać:

wp ={x+y > 0},        wk = {result | x Ù result | y Ù ( " z)(z½x i z½y ® z £ result)}.

Warunek początkowy gwarantuje, że x i y nie są równocześnie równe 0, w warunek końcowy, że uzyskany wynik (wartość zmiennej result) jest dzielnikiem zarówno x jak i y, oraz każdy inny wspólny dzielnik x i y ma mniejszą od niego wartość. Znany wszystkim algorytm Euklidesa rozwiązuje postawiony w tym przykładzie problem. 

Niezmiennikiem pętli w tym algorytmie jest formuła  nwd(x,y) = k. Uzasadnienie: nwd(x,y) = nwd(x-y,y), gdy x>y oraz nwd(x,y) = nwd(y-x,x), gdy y>x. Zatem niezależnie od tego, którą część instrukcji warunkowej wykonamy, największy wspólny dzielnik nowych wartości zmiennych x i y jest taki sam, jak liczb przypisanych tym zmiennym przed wykonaniem programu.

Nie na wiele przyda nam się niezmiennik, jeżeli nie jest on prawdziwy przed wykonaniem programu. Jeżeli jednak jest prawdziwy przed wejściem do pętli i pozostaje prawdziwy po każdej iteracji, to, o ile algorytm się zatrzyma, uzyskane wartości zmiennych również go spełniają. Pozwala nam to często zrozumieć co robi program i uzasadnić jego częściową poprawność.

Wróćmy na chwilę do przykładu poprzedniego. Niech k będzie największym wspólnym dzielnikiem danych liczb naturalnych x i y.  Jeżeli x*y = 0, to jedna z liczb x lub y musi być zerem, ale wtedy k jest równe sumie tych liczb. Jeżeli obie liczby x i y są różne od zera i  przed wykonaniem pętli mamy nwd(x,y) = k, to własność ta nie zmienia się w kolejnych iteracjach pętli. W momencie, wyjścia z pętli  mamy (nwd(x,y) = k Ù x=y), z czego wynika, że zmienna result ma wartość k, a więc wartość największego wspólnego dzielnika danych liczb.  Pozostaje jeszcze pytanie, czy ten algorytm zatrzymuje się dla wszystkich danych spełniających warunek początkowy. Zauważmy, że suma  (x + y) jest w tym algorytmie zawsze liczbą naturalną różną od zera. Co więcej, wartość tej sumy jest w każdym następnym kroku równa większej z wartości x i y w kroku poprzednim. Zatem ciąg wartości sum (x + y) jest ściśle malejący, a więc nie może być nieskończony. To dowodzi, że po skończonej liczbie kroków algorytm Euklidesa zatrzyma się.

Przykładem niech będzie algorytm {x:=0; while  not (x=y) do x := x+1 od}. W strukturze liczb naturalnych ten algorytm zawsze się zatrzymuje,  bo każdą liczbę naturalną można otrzymać z zera przez dodawanie jedynki. Ten algorytm ma więc własność stopu w strukturze liczb naturalnych.

 Pytanie 4  Czy własność  (Wartością zmiennej result  jest największa z liczb {x₁,...,x_i-1}  oraz  i £ n ) jest niezmiennikiem pętli w algorytmie max?

« poprzedni punkt

następny punkt »