C.A.R. Hoare (1934– )
Zauważmy, że o poprawności formuły Hoare'a możemy mówić w dwóch przypadkach:
Kiedy dla danych spełniających \( \varphi_1 \) program się nie zatrzyma.
Jest to dość istotny szczegół techniczny, którym się jeszcze zajmiemy.
Jak zatem wnioskować o programach? Za chwilę podamy zbiór reguł dla podstawowych konstrukcji programistycznych, umożliwiający wnioskowanie na podstawie drzewa wywodu programu. Dla każdego węzła drzewa wywodu, albo dokładniej, dla każdej produkcji gramatyki podamy regułę wnioskowania pozwalającą wyprowadzić konsekwencję wykonania instrukcji na podstawie opisu działania instrukcji składowych. Reguły wnioskowania będziemy zapisywali w postaci
\( \frac{\mbox {Przesłanki oddzielone przecinkami}}{\mbox {Wniosek}} \)
Przesłanki tak są dobrane, aby wniosek wyrażał własność, że dana instrukcja jest częściowo poprawna względem dwóch formuł \( \alpha \) i \( \beta \).
Zacznijmy od najprostszej instrukcji pustej:
\( \frac{}{\{\alpha\} \varepsilon \{\alpha\}} \)
Czytamy to tak: bez żadnych warunków wstępnych (pusty "licznik"), jeśli dane początkowe spełniają warunek \( \alpha \), po wykonaniu instrukcji pustej (zauważmy, że nie może się wykonanie takiej instrukcji zapętlić) dane końcowe spełniają warunek \( \alpha \). Dość oczywiste, zważywszy że instrukcja pusta nie robi nic. Mamy tu pusty zbiór przesłanek.
Umówmy się, że jeśli zmienna \( z \) jest parametrem formuły logicznej \( \alpha(z) \), zaś \( E \) jest wyrażeniem, przez \( \alpha(E) \) rozumiemy formułę, która powstaje przez zastąpienie wszystkich wystąpień zmiennej \( z \) w formule \( \alpha \) przez \( E \). Mamy zatem następującą regułę wnioskowania dla instrukcji przypisania:
\( \frac{}{\{\alpha(E)\}{\mbox{\tt z:=E}}\{\alpha(z)\}} \) która mówi nam, że jeśli przed wykonaniem przypisania zachodziła formuła \( \alpha \) dla wyrażenia \( E \), po wykonaniu instrukcji przypisania formuła ta będzie zachodziła dla zmiennej \( z \). Faktycznie, skoro \( z \) przyjęła wartość \( E \), dla której formuła \( \alpha \) była prawdziwa, nie ma powodu, dla którego formuła ta miała by nie zachodzić dla wartości \( z \).
Tym razem musimy wyrazić to co się dzieje, gdy wykonujemy sekwencję instrukcji. Intuicyjnie będziemy zakładali, że istnieje ciąg stanów pośrednich, spełniających pośrednie formuły \( \alpha_1,\ldots,\alpha_n \). Mamy zatem
\( \frac{\mbox {\alpha=\alpha_0,\{\alpha_0\}P1\{\alpha_1\}, \ldots,\{\alpha_{n-1}\} Pn \{\alpha_n\}, \alpha_n=\beta}}{\mbox {\{\alpha\}{\tt begin P1; \dots Pn end} \{\beta\}}} \)
Czyli jeśli umiemy udowodnić, że w stanie \( \alpha_0 \) po wykonaniu P1 przejdziemy do stanu \( \alpha_1 \), w stanie \( \alpha_1 \) po wykonianiu P2 przejdziemy do stanu \( \alpha_2 \dots \), a ze stanu \( \alpha_{n-1} \) po wykonaniu Pn przejdziemy do stanu \( \alpha_n \), to łącznie wykonanie wszystkich instrukcji ze stanu spełniającego \( \alpha_0 \) przeprowadzi nas do stanu spełniającego \( \alpha_n \).
Podamy dwie reguły: dla instrukcji bez "else" i dla instrukcji z "else".
\( \frac{\mbox {\{\alpha \land B\} P \{\beta\}, (\alpha \land \neg B) arrow \beta}}{\mbox {\{\alpha\}{\tt if B then P } \{\beta\}}} \) \( \frac{\mbox {\{\alpha \land B\} P \{\beta\}, \{\alpha \land \neg B\} Q \{ \beta\}}}{\mbox {\{\alpha\}{\tt if B then P else Q } \{\beta\}}} \)
Odczyt tych reguł jest bardzo naturalny i zgodny oczywiście z semantyką instrukcji warunkowych. W pierwszym przypadku bowiem (bez "else") albo instrukcja \( P \) wykona się albo nie, w zależności od prawdziwości warunku \( B \). Wystarczy zatem, żeby dla danych spełniających \( \alpha \) i takich, że warunek \( B \) jest spełniony wykonanie programu P doprowadziło nas do stanu \( \beta \), aby w tym przypadku cała instrukcja warunkowa była poprawna względem \( \alpha \) i \( \beta \). Również gdy dla takich danych warunek \( B \) nie jest spełniony, wówczas żądamy, aby \( \beta \) było automatycznie spełnione bez wykonywania jakiejkolwiek instrukcji – żeby było logiczną konsewkencją \( \alpha \) i \( \neg B \) i w obu przypadkach: odpowiednio wykonując instrukcję \( P \) lub nie, mamy zapewnione spełnienie warunku \( \beta \).
Dla instrukcji warunkowej z "else" mamy jednorodną sytuację: zależnie od tego, czy \( B \) jest spełnione czy nie, żądamy częściowej poprawności albo względem instrukcji \( P \), albo \( Q \).
Gdyby programy składały się tylko z dotychczas omówionych w tym rozdziale instrukcji, wówczas można by automatycznie dowodzić poprawność programów. Instrukcja pętli powoduje, że taka automatyzacja nie jest możliwa. Metoda dowodzenia poprawności pętli ma charakter indukcyjny. Podamy ją tylko dla pętli while, bowiem pozostałe typy instrukcji pętli dadzą się z niej wyprowadzić. Idea reguły dowodzenia leży w wymyśleniu warunku, który będzie zawsze spełniony na początku każdego obrotu pętli. Taki warunek będziemy nazywali 'niezmiennikiem' pętli. Od niezmiennika będziemy wymagali trzech rzeczy.
Ujmijmy nasze żądania w regułę dowodzenia.
\( \frac{\mbox {\alpha \Rightarrow N, \{N\land B\}P \{N\},N\land \neg B \Rightarrow \beta }}{\{\alpha\}{\mbox {\tt while B do P }} \{\beta\}} \)
Zauważmy, że w regule tej pojawia się - jakby znikąd - warunek \( N \). Musimy go sami wymyślić i jeżeli uda się nam znaleźć \( N \) takie, żeby spełniało wszystkie 3 przesłanki, udowodnimy częściową poprawność instrukcji pętli.
Zanim przejdziemy do przykładów zauważmy, że poprawne są również dwa schematy dowodzenia, z których często będziemy korzystali. Nazywane są one regułami osłabiania. Osłabić twierdzenie można albo wzmacniając założenie, albo osłabiając tezę.
\( \frac{\mbox {\alpha \Rightarrow \gamma, \{\gamma\}P \{ \beta\}}}{\mbox {\{\alpha\} P \{\beta\}}} \)
\( \frac{\mbox {\{\alpha\} P \{ \gamma\}, \gamma \Rightarrow \beta}}{\mbox {\{\alpha\} P \{\beta\}}} \)
Podajmy teraz parę przykładów zastosowania podanych reguł dowodzenia zastosowanych do stwierdzania poprawności instrukcji.
Przykład [1]
Na początek prosty przykład. Udowodnijmy, że jeśli \( k\ge 0 \), to po instrukcji j:=k+1 mamy \( j>0 \). Ponieważ mamy po prawej stronie instrukcji przypisania wyrażenie \( k+1 \), więc musimy warunek początkowy zapisać w równoważnej formie, w której miejsce zmiennej \( k \) zajmuje wyrażenie \( k+1 \). Zatem \( k\ge 0 \) jest rónoważne \( k+1\ge 1 \) i stosując regułę dla instrukcji przypisania otrzymujemy, że \( j\ge 1 \), co akurat w przypadku zmiennych całkowitych jest równoważne \( j>0 \). Gdyby jednak zmienne \( k \) oraz \( j \) były typu rzeczywistego, to końcowe stwierdzenie otrzymalibyśmy osłabiając tezę: wszak \( j\ge 1 \) implikuje \( j>0 \).
Przykład [2]
Tym razem spróbujmy przeanalizować fragment programu, w którym chcemy sprawdzić, czy w tablicy A[1..n] of Integer znajduje się zadana wartość \( x \). Zakładamy tu, że nie wiemy nic o uporządkowaniu tablicy, w szczególności nie możemy zakładać posortowania danych. Nie wiemy również, jaka jest wartość \( n \) poza tym, że jest nieujemna (dla n=0 mamy do czynienia z pustą tablicą). Przeszukiwanie zaczniemy od pierwszego elementu i będziemy sprawdzali, czy w kolejnych elementach tablicy jest szukane \( x \). Pierwszy pomysł polega na tym, że pętlą for przejdziemy przez całą tablicę i jeśli znajdziemy \( x \), zmienimy początkową waratość logicznej zmiennej jest z false na true.
jest := false; <b>for</b> k:=1 <b>to</b> n <b>do</b> if A[k]=x <b>then</b> jest:=true
Pomysł tyleż prosty, co niezbyt ambitny: jeśli element \( x \) jest na początku tablicy, to pętla for niepotrzebnie będzie wykonywała dalsze sprawdzanie. Spróbujmy udowodnić jednak, że program ten jest poprawny. Zacznijmy od zapisania go przy użyciu pętli while.
jest := false; k:=1;
jest=false, k=1
while k<=n do \( {\mbox{\neg jest \Leftrightarrow (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n+1)}} \)
begin
if A[k]=x then jest:=true;
k:=k+1
end
\( {\mbox {\neg jest \Leftrightarrow (\forall 1\le j \le n: A[j] \neq x)}} \)
Sprawdźmy, że podany niezmiennik pętli spełnia wszystkie warunki. Oznaczmy przez \( N(k) \) wartość formuły logicznej
\( (\neg jest \Leftrightarrow \forall 1\le j < k: A[j] \neq x) \land (1\le k\le n+1) \).
Zauważmy po pierwsze, że w trywialny sposób inicjalizuje się. Warunek \( N(1) \) jest zawsze prawdziwy: nie ma bowiem żadnej wartości \( j \) większej lub równej 1, a jednocześnie mniejszej od 1, wskutek czego pierwszy czynnik koniunkcji jest trywialnie prawdziwy. Wszelkie stwierdzenia poprzedzone kwantyfikatorem ogólnym dla elementów zbioru pustego są prawdziwe. Oczywiście dla \( n\ge 0 \) oraz \( k=1 \) mamy też \( 1\le k\le n+1 \), więc drugi czynnik też jest prawdziwy.
Po drugie wykonanie jednego obrotu pętli nie zmienia prawdziwości niezmiennika. Jeśli bowiem na początku pętli dla pewnej wartości k wartość zmiennej jest równa się false, to na mocy założenia indukcyjnego zachodzi
\( \forall 1\le j < k: A[j] \neq x \).
Teraz mamy dwa przypadki.
Podobnie gdy zmienna jest ma wartość true, na mocy założenia istnieje \( 1\le j < k \) takie, że \( A[j]=x \). Niezależnie od tego, czy przypisanie jest :=true zostanie wykonane w ramach instrukcji warunkowej, po wykonaniu instrukcji k:=k+1 niezmiennik się również odtworzy. To stwierdzenie kończy dowód niezmienniczości formuły \( N(k) \).
Zostało nam w końcu do udowodnienia, że po wyjściu z pętli, gdy mamy \( k>n \) oraz zachodzi \( N(k) \), otrzymamy tezę. Zatem ze względu na to, że \( k\le n+1 \) dochodzimy do wniosku, że \( k=n+1 \), co łącznie z pierwszym czynnikiem niezmiennika daje nam (po zastosowanu reguły osłabienia tezy) końcowy warunek
\( (\neg jest = \forall 1\le j < n+1: A[j] \neq x) \).
W naszym przypadku niezmiennik opisywał ogólną sytuację po kilku obrotach pętli: zmienna jest ma wartość true wtedy i tylko wtedy gdy na lewo od \( k \) znajduje się wartość \( x \). Kiedy szukamy niezmiennika, staramy się możliwie dokładnie wyobrazić sobie jak może wyglądać sytuacja, gdy już pętla wykona parę obrotów i zapisujemy to w postaci formuły logicznej. Jeśli nie mamy wystarczająco dużo wyobraźni, to niezmiennik wyjdzie za słaby i trudno będzie korzystając tylko z niego i z dozoru pętli jego niezmienniczość udowodnić (choć może być prawdziwy). Również za słaby niezmiennik może być powodem trudności pokazania trzeciej z implikacji, kończącej wywód. W naszym przypadku na przykład nieuwzględnienie w niezmienniku warunku \( k\le n+1 \) spowodowałoby kłopoty z przekształceniem niezmiennika do postaci \( N(n+1) \), z czego wynikała od razu teza. Z kolei za mocny niezmiennik oznacza kłopoty z jego inicjalizacją. Niezmiennik powienien być w sam raz.
Zauważmy jeszcze jedną rzecz. W momencie, gdy zmienna jest przyjmuje wartość true, możemy dalsze przeszukiwanie zakończyć, gdyż na false już zmienić swojej wartości nie może z powrotem. Zatem dozór pętli możemy wzmocnić o dodatkowy warunek tak, aby przerwać obliczenia, gdy tylko \( x \) znajdziemy. Tym razem, ponieważ liczba obrotów pętli będzie dynamicznie zależała od danych, nie można użyć pętli for, tylko od razu użyjemy pętli while.
jest := false; k:=1; jest=false, k=1 <b>while</b> (not jest) and ( k<=n) do \( {\mbox{\neg jest \Leftrightarrow (\forall 1\le j < k: A[j] \neq x \land 1\le k\le n+1)}} \) <b>begin</b> <b>if</b> A[k]=x <b>then</b> jest:=true; k:=k+1 <b>end</b>
Dowód poprawności przebiega identycznie jak poprzednio. Zmienia się tylko złożoność algorytmu: ten wykona być może mniej kroków, choć w najgorszym przypadku – gdy x w tablicy A nie ma - w obu przypadkach wykonamy tę samą liczbę obrotów pętli. Zauważmy, że to są kroki trochę droższe, bo mamy bardziej skomplikowany warunek dozoru. Czy skórka jest warta wyprawki?
Powiedzmy tak: jeśli mamy podejrzenie, że znalezienie x jest prawdopodobne, a danych jest dużo, warto zastosować wcześniejsze przerwanie pętli. Kiedy jednak danych jest niewiele lub przypuszczalnie wartości x nie ma w tablicy, wtedy pętla for jest sensowniejszym rozwiązaniem. Nie ma sensu optymalizować tego typu pętli, gdy mamy np. do czynienia z tablicą kilkunastoelementową. W każdym razie to, od kiedy zaczyna się opłacać robić tego typu optymalizacje, zależy często od testów – wystarczy napisać obie wersje programu i sprawdzić, czy zyskujemy coś na którejś z nich. Na pewno jednak dobry programista powinien umieć napisać obie wersje.
Problem jest co prawda prosty, ale bardzo ważny, więc pokażemy jeszcze dwa ulepszenia tego algorytmu. Oto pierwsze z nich.