Co oznacza poprawność algorytmu?

To, co intuicyjnie rozumiemy jako poprawność algorytmu, formalnie określamy mianem całkowitej poprawnościalgorytm całkowicie poprawnycałkowitej poprawności. Składają się na nią dwa elementy: własność stopu oraz częściowa poprawność.

Aby wyjaśnić znaczenie tych terminów, rozważmy najpierw pojęcie specyfikacji algorytmu. Określamy tak ścisły opis danych wejściowych, danych wyjściowych oraz relacji, jakie między nimi zachodzą.

Algorytm powinien działać w sposób poprawny dla danych, które spełniają warunek początkowy – w tej sytuacji zwróci on dane wyjściowe spełniające warunek końcowy, czyli wynik osiągnięty w sposób opisany przez specyfikację. Nie oznacza to, że algorytm nie będzie działał dla danych niespełniających warunku początkowego - po prostu nie jest on do nich przystosowany i nie można na nim polegać.

Częściowa poprawnośćczęściowa poprawność algorytmuCzęściowa poprawność oznacza, że jeżeli algorytm zakończy się wykonywać, a dane wejściowe spełniały warunek początkowy, to zwrócony przez niego wynik będzie poprawny. Własność stopuwłasność stopuWłasność stopu oznacza, że dla każdych danych wejściowych spełniających warunek początkowy algorytm skończy się wykonywać po skończonej liczbie kroków.

Algorytm jest całkowicie poprawny, jeżeli jest jednocześnie częściowo poprawny oraz ma własność stopu. Oznacza to, że jeżeli otrzymał on poprawne dane, zwróci poprawny wynik po skończonej liczbie kroków.

R1RjKbcOKDX5m

Ilustracja przedstawia trzy bloki z opisami.
Własność stopu: algorytm zakończy wykonywanie się po skończonej liczbie kroków.
Częściowa poprawność: jeżeli algorytm skończy się wykonywać, zwrócony przez wynik będzie poprawny.
Od tych dwóch bloków wychodzi strzałka do bloku trzeciego.
Całkowita poprawność: algorytm po skończonej liczbie kroków zwróci poprawny wynik.

Zagadnienie poprawności omówmy najpierw na podstawie następującego algorytmu.

Specyfikacja problemu:

Dane:

• n – liczba elementów w tablicy; liczba naturalna

• tab – tablica n liczb całkowitych

Wynik:

Algorytm zwraca największą liczbę występującą w tablicy.

Przedstawiony na schemacie blokowym algorytm wygląda następująco:

Ten sam algorytm możemy przedstawić również za pomocą pseudokodu:

tab[1..n] ← wprowadź n liczb całkowitych do tablicy 
i ← 2
maksimum ← tab[1]
dopóki i ≤ n wykonuj:
	jeżeli tab[i] > maksimum:
		maksimum ← tab[i]
	i ← i + 1
zwróć maksimum

Dowodzenie poprawności

Przeprowadzenie dowodu na całkowitą poprawność sprowadza się do udowodnienia częściowej poprawności oraz własności stopu.

By sprawdzić poprawność algorytmu, dzielimy go na fragmenty. Za pomocą zapisów matematycznych sprawdzamy, czy dane wejściowe dają odpowiednie dane wyjściowe.  Uzyskany końcowy wynik powinien być zgodny ze specyfikacją.

Aby przybliżyć istotę tych dowodów, przeanalizujmy działanie podanego wyżej algorytmu dla przykładowych danych:

Na koniec zostaje zwrócona wartość zmiennej maksimum.

Możemy zauważyć, że zwrócona przez algorytm wartość jest poprawna – liczba $10$ jest rzeczywiście największa spośród przykładowych danych wejściowych.

Zachodzi tu pewna prawidłowość – wartość zmiennej maksimum nigdy się nie zmniejsza. Co więcej, możemy stwierdzić, że jej wartość w każdym wykonaniu pętli będzie równa największej liczbie napotkanej do tej pory, czyli w elementach tablicy o indeksach od $1$ do i$-1$.

W momencie, w którym pętla kończy się wykonywać, zmienna maksimum zawiera największą wartość spośród elementów tablicy o indeksach od $1$ do $10$, czyli największą wartość w całej tablicy.

Taką zależność nazywamy niezmiennikiem pętliniezmiennik pętliniezmiennikiem pętli. Jest to warunek, który jeśli jest spełniony przed wykonaniem iteracji, będzie spełniony również po niej. Może zostać on użyty w tzw. metodzie niezmienników, która jest jednym ze sposobów na udowodnienie częściowej poprawności algorytmu.

Wiemy już, że wartość zmiennej maksimumzawiera w każdej iteracji pętli największą wartość w pewnym przedziale, więc po wyjściu z pętli będzie ona zawierała największą wartość w całej tablicy. Pytanie brzmi: czy pętla kiedykolwiek się zakończy?

W przypadku omawianego algorytmu własność stopu możemy udowodnić w następujący sposób:

1. Algorytm skończy się wykonywać, kiedy i > n.

2. n ma określoną wartość.

3. W każdej iteracji pętli wartość zmiennej i zwiększa się o $1$.

4. Zatem algorytm zakończy się po skończonej liczbie iteracji – tym samym udowodniliśmy własność stopu.

Sprawdziliśmy, czy nasz algorytm posiada własność stopu – zatrzymuje się w momencie, w którym wartość zmiennej i przekracza wartość n. Korzystając z niezmiennika pętli, wykazaliśmy również jego częściową poprawność. Możemy zatem stwierdzić, że nasz algorytm jest całkowicie poprawny – za tym stwierdzeniem stoi pewna forma dowodu matematycznego.

Dowody na całkowitą poprawność bardziej skomplikowanych algorytmów będą oczywiście odpowiednio dłuższe, lecz na poziomie szkoły ponadpodstawowej analiza na takim poziomie jest wystarczająca.

Przykład algorytmu – obliczanie silni

Silnię liczby naturalnej  n definiujemy jako iloczyn wszystkich liczb naturalnych od $1$ do n, zaś zapisujemy jako n!. Aby obliczyć jej wartość dla pewnego n, możemy wykorzystać następujący algorytm:

Specyfikacja problemu:

Dane:

• n – liczba, której silnię obliczamy; liczba naturalna

Wynik:

Algorytm zwraca wartość silni liczby n.

Zapis algorytmu za pomocą pseudokodu:

n ← wprowadź liczbę naturalną n
wynik ← 1
i ← 2
dopóki i ≤ n wykonuj:
	wynik ← wynik * i
	i ← i + 1
zwróć wynik

Rozważmy działanie tego algorytmu dla liczby n = 5.

Na końcu zostaje zwrócony wynik $120$, co rzeczywiście jest silnią z liczby $5$.

W przypadku tego algorytmu, własność stopu jest analogiczna, jak w algorytmie wyszukiwania największej liczby w tablicy, tj. zmienna i zwiększa się o stałą wartość, więc po skończonej liczbie iteracji przekroczy zmienną n, która również jest wartością stałą i skończoną.

Kluczem do niezmiennika pętli w tym algorytmie jest zmienna wynik. Jest to bowiem silnia z liczby i. Możemy na podstawie tych stwierdzeń udowodnić poprawność tego algorytmu, jak również zademonstrować ją na przykładzie. Możemy też wyjaśnić krok po kroku, dlaczego nasz algorytm zwraca poprawne wyniki.

Inne cechy algorytmów

Poza opisanymi, wynikającymi z definicji, właściwościami całkowitej poprawności, możemy wymienić jeszcze kilka cech poprawności algorytmu.

Aspektem algorytmu, który przyjmujemy za oczywisty, jest jego określoność. Oznacza to, że czytelnik musi być w stanie zrozumieć i dokładnie odwzorować kolejne etapy wykonywania algorytmu. Aby algorytm był niepoprawnie określony, wystarczy jedna błędna instrukcja. Przykładowo: „wczytaj liczby” nie mówi nam nic o tym, jakie liczby mamy wczytać – całkowite, rzeczywiste, zespolone...? Ile liczb trzeba wczytać? W tej instrukcji powinniśmy zawrzeć konkrety, przez co mogłaby ona przyjąć postać, np. „wczytaj liczbę całkowitą X oraz liczbę naturalną N”.

Inną ważną cechą algorytmu jest jego uniwersalność. Oznacza ona, że algorytm powinien działać dla dowolnych danych spełniających warunki specyfikacji. Dotyczy to również liczby danych wejściowych, np. algorytm ma działać dla ciągu n–wyrazowego, a nie dla ciągu zawierającego z góry określoną liczbę wyrazów.

Na szczególną uwagę zasługuje wspomniana wcześniej skończoność algorytmu. W praktyce nie wystarczy, że algorytm kiedyś skończy się wykonywać – chcemy, aby stało się to jak najszybciej, przy jak najmniejszej liczbie kroków lub zużywając jak najmniej zasobów takich jak pamięć, w której przechowywane są zmienne. Dobrze zaprojektowane algorytmy wykonują tylko niezbędne operacje – innymi słowy są efektywne.

Słownik