WDP Dowodzenie poprawności programów

From Studia Informatyczne

Spis treści

Wprowadzenie

Wiemy, jak bardzo nasze życie zaczyna zależeć od komputerów, a dokładniej od programów komputerowych. Chodzi tu nie tylko o wygodę. Niekiedy działanie komputerów ma krytyczne znaczenie, gdy mówimy o takich zastosowaniach jak transport (nie tylko lotniczy), loty kosmiczne, nadzorowanie życia pacjenta w czasie operacji, dozowanie leków. Wszelkie zastosowania komputerów, gdzie trzeba mieć zaufanie do programu sprawiają, że trzeba zapytać z czego wynika nasze zaufanie, że program komputerowy napisany jest dobrze?

Mija właśnie epoka, w której poprawność programu można było ustalić na podstawie słowa honoru danego przez programistę, że się nie pomylił. Typowym zachowaniem programisty po napisaniu programu to oczywiście jego gruntowne przetestowanie. Gruntowne to nie znaczy całkowite. Rzadko bowiem w czasie testowania mamy wyobraźnię tak bogatą, żeby przedstawić sobie wszystkie możliwe sytuacje, szczególnie wtedy, gdy jest ich potencjalnie nieskończenie wiele. Owszem, testy mogą wykazać, że program jest niepoprawny, ale prawie nigdy (poza przypadkami, kiedy liczba przypadków jest skończona i mała – wielka rzadkość) nie mogą wykazać jego poprawności. Informatycy od dawna próbują skonstruować metody wnioskowania o programach i stają się one coraz popularniejsze, szczególnie że raz udowodnione fragmenty programu mogą być włączane do bibliotek jako poprawne moduły, do których już nie trzeba wracać.

Jak zatem udowodnić, że program robi to, o co nam chodzi? Mniej więcej widać, że gdy wykonamy instrukcję i:=i+1 dla i=1 będziemy mieli i=2. Czy możliwe jest jednak opracowanie ogólnej teorii? Okazuje się, że dla ogromnej większości algorytmów jesteśmy w stanie udowodnić ich poprawność korzystając z metod logiki opracowanych na początku lat 60-tych XX wieku. Jak się wkrótce okaże, ta teoria nie tylko pozwala udowodnić poprawność algorytmu, ale i daje metodologię wymyślania algorytmów. Za jej pomocą będziemy wiedzieli, na czym się skupić, gdy zaczynamy projektować pętle.

Częściowa poprawność programów

Będziemy poszukiwali takiej teorii, która pozwoli nam ustalić pewną relację między trzema obiektami: stanem początkowym, instrukcją i stanem końcowym. Relacja ta intuicyjnie ma oznaczać, że jeśli w pierwszym stanie, zwanym początkowym, wykonamy badaną instrukcję, to przejdziemy do stanu drugiego, który nazwiemy końcowym. W rzeczywistości, żeby móc wnioskować o nieskończonej przestrzeni stanów, będziemy agregować wiele z nich za pomocą formuł logicznych. Zatem będziemy rozważali pewien zbiór stanów początkowych, instrukcję oraz pewien zbiór stanów końcowych, które będą względem siebie w odpowiedniej relacji. Stany początkowe i końcowe będziemy określali za pomocą formuł.

Przykładowo możemy sobie wyobrazić formułę \varphi_1 =k\ge 0, instrukcję j:=k+1 oraz formułę \varphi_2 =j > 0 i próbować udowodnić dość oczywisty fakt, że jeśli stan początkowy spełnia formułę \varphi_1, to po wykonaniu naszej instrukcji stan końcowy będzie spełniał formułę \varphi_2. Wprowadźmy zatem oznaczenie

Formuła częściowej poprawności programu P   
Trójka (\{\varphi_1\},P, \{\varphi_2\}) to formuła logiczna, która jest prawdziwa wtedy i tylko wtedy, gdy 
zachodzi następujący warunek. Dla każdego stanu spełniającego \varphi_1, jeżeli program P  
zakończy swoje działanie, to stan końcowy będzie spełniał formułę \varphi_2.

Takie formuły nazywamy trójkami Hoare'a albo formułami częściowej poprawności programu. Zostały wprowadzone przez jednego z największych informatyków, Anthony'ego Hoare'a, w połowie lat 60.

C.A.R. Hoare (1934– )
Enlarge
C.A.R. Hoare (1934– )

Zauważmy, że o poprawności formuły Hoare'a możemy mówić w dwóch przypadkach:

  1. Kiedy dla danych spełniających \varphi_1 program się zatrzyma i dane po zatrzymaniu się programu spełniają \varphi_2
  2. 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.


Instrukcja pusta

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.


Instrukcja przypisania

Umówmy się, że jeśli zmienna z jest parametrem formuły logicznej \alpha(z), zaś E jest wyrażeniem, to 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.

Instrukcja złożona

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.

Instrukcja warunkowa

Podamy dwie reguły: dla instrukcji bez "else" i dla instrukcji z "else".

\frac{\mbox {\{\alpha \land B\} P \{\beta\}, (\alpha \land \neg B) \rightarrow \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.

Instrukcja pętli

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.

  • żeby był spełniony przy wejściu do pętli przed jej pierwszym obrotem
  • żeby jeden obrót pętli nie zmieniał jego wartości (czyli żeby niezmiennik pozostawał prawdziwy)
  • żeby po wyjściu z pętli niezmiennik (nadal prawdziwy!) w koniunkcji z zaprzeczeniem dozoru pętli implikował warunek \beta

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ę.

Wzmacnianie założenia

\frac{\mbox {\alpha \Rightarrow \gamma, \{\gamma\}P \{ \beta\}}}{\mbox {\{\alpha\} P \{\beta\}}}

Osłabianie tezy

\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; 
 for k:=1 to n do if A[k]=x then 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)}}

Wizualizacja

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.

  • Jeśli dodatkowo A[k] \neq x, to możemy powiedzieć równoważnie, że \forall 1\le j < k: A[j] \neq x \land A[k] \neq x, czyli \forall 1\le j \le  k: A[j]\neq x, a to jest równoważne \forall 1\le j <  k+1: A[j]\neq x. Warunek ten obrazuje stan obliczeń po wykonaniu badanej instrukcji warunkowej, gdyż wartość zmiennej jest pozostanie równa false. W jednym kroku pętli wykonuje się jeszcze tylko instrukcja k:=k+1. Po tym przypisaniu warunek nasz będzie spełniony dla nowego k, czyli niezmiennik \neg jest = \forall 1\le j < k: A[j] \neq x zostaje odtworzony.
  • Jeśli natomiast A[k]=x, to wykona się instrukcja jest := true i wtedy, dla nowej wartości k, formuła \forall 1\le j \le  k: A[j]\neq x będzie fałszywa, czyli równoważna wartości \neg jest.


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
while (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)}}
  begin 
    if A[k]=x then jest:=true;
    k:=k+1
  end


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.

Wyszukiwanie liniowe proste

Tym razem musimy założyć, że tablica jest niepusta, czyli że n\ge 1. Oto kolejna wersja rozwiązania problemu wyszukiwania liniowego.


 {{\mbox{ n\ge 1}}}
 k:=1;
 {{\mbox{ k=1, n\ge 1}}}
 while (k<n) and (A[k]<> x) do {{\mbox{(\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n)}}}
    k:=k+1; 
   {{\mbox{ (A[k]=x) \Leftrightarrow ((\exists 1\le j \le n: A[j] = x) \land (1\le k\le n))}}}
   jest := A[k]=x
 {{\mbox{ (jest) \Leftrightarrow ((\exists 1\le j \le n: A[j] = x) \land (k\le n))}}}

Wizualizacja

Ulepszenie polega na uproszczeniu treści pętli. Zauważmy, że pętla przerwie swoje działanie, gdy tylko k dojdzie do n lub A[k] będzie równe x. Możliwe jest też, że pętla przerwie działanie z obu powodów na raz. Pozbywamy się tu też dodatkowej zmiennej logicznej jest i działamy bezpośrednio na elementach tablicy A.

Sprawdzenie, że warunki początkowe dobrze inicjalizują niezmiennik jest proste. Również nieskomplikowany jest dowód niezmienniczości. Najtrudniejsze tym razem będzie pokazanie, że negacja dozoru i niezmiennik implikują warunek

{\mbox{ (A[k]=x) \Leftrightarrow ((\exists 1\le j \le n: A[j] = x) \land (1\le k\le n))}}.

Zanim to zrobimy, zauważmy, że zachodzą następujące tożsamości logiczne.

((p \land q) \Rightarrow r) \Leftrightarrow ((p\Rightarrow r) \lor (q\Rightarrow r)) 
((p \lor q) \Rightarrow r) \Leftrightarrow ((p\Rightarrow r) \land (q\Rightarrow r))

Sprawdzenie prawdziwości tych tautologii pozostawiamy jako ćwiczenie. Są one o tyle ważne, że bardzo często dowodzimy wynikania czegoś z koniunkcji albo alternatywy warunków i tautologie te pozwalają nam zredukować dowody do prostszych przypadków. Zauważmy charakterystyczną zamianę rolami spójników logicznych \land oraz \lor. Kiedy dowodzimy, że coś wynika z koniunkcji warunków, wystarczy że udowodnimy, że wynika z jednego z nich. Natomiast gdy dowodzimy, że coś wynika z alternatywy warunków, wówczas musimy pokazać, że wynika z każdego z nich.

Dowiedziemy zatem prawdziwości następującej formuły:

(((k\ge n)\lor(A[k]=x)) \land (\forall 1\le j < k: A[j] \neq x) \land (k\le n))  \Rightarrow ((A[k]=x) \Leftrightarrow ((\exists 1\le j \le n: A[j] = x) \land (1\le k\le n))).

Lewa strona implikacji to zaprzeczenie dozoru i niezmiennik, a prawa strona implikacji to warunek, który jest nam konieczny do dowodu ostatecznej formuły: wyraża on fakt, że to czy w tablicy A znajduje się wartość x zależy wyłącznie od tego, czy x równa się A[k] po wyjściu z pętli. W poprzedniku implikacji mamy alternatywę i dwie koniunkcje. Korzystając z praw de Morgana rozbijamy alternatywę otrzymując równoważny poprzednikowi implikacji warunek

((k\ge n) \land (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n)) \lor ((A[k]=x) \land (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n)).

Mamy tu do czynienia z postacią właśnie omawianej tautologii, kiedy to z alternatywy p oraz q wynika r. Rolę p pełni tu formuła

((k\ge n) \land (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n)), rolę q

formuła ((A[k]=x) \land (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n)),

zaś rolę r pełni formuła

(A[k]=x) \Leftrightarrow ((\exists 1\le j \le n: A[j] = x) \land (1\le k\le n)).

Osobno udowodnimy więc dwie implikacje:

p \Rightarrow r i q\Rightarrow r.

Zacznijmy od p\Rightarrow r. Załóżmy, że zachodzi p. Wtedy, ponieważ k\le n oraz k\ge n, więc k=n. Skoro tak, to w trzecim czynniku koniunkcji wchodzącej w skład p mamy (\forall 1\le j < n: A[j] \neq x). Zatem istnieje j pomiędzy 1 a n takie, że A[j]=x wtedy i tylko wtedy, gdy A[n]=x, czyli A[k]=x, co było do pokazania. Oczywiście drugi czynnik koniunkcji w formule r jest trywialnie prawdziwy dla k=n.

Pozostało nam do pokazania, że q \Rightarrow r. Z q wynika, że 1\le k \le n oraz że A[k]=x. Zatem istnieje takie j (równe k), że A[j]=x.

Pokazana implikacja kończy cały dowód.

Oczywiście możemy tu narzekać, że dość prosty program, którego poprawność była "oczywista", miał tak skomplikowany dowód poprawności. Nie zapominajmy jednak, że

  • Po pierwsze, gdy już udowodnimy poprawność takiego kodu, możemy opakować go w procedurę i więcej do niego nie zaglądać, wiedząc, że na pewno dobrze zadziała.
  • Po drugie, co można zaproponować poza takim dowodem? Solenne przyrzeczenie programisty, że się nie pomylił?
  • Po trzecie, jak się wkrótce okaże, technika niezmienników służy nie tylko do dowodzenia poprawności programów, ale też do prawidłowego konstruowania pętli.
  • Po czwarte, często przeprowadzając dowody nie zauważa się szczególnych przypadków. W analizowanym programie na przykład można łatwo przeoczyć konieczność założenia n\ge 1. Puste tablice też się zdarzają i akurat w naszym przypadku mógłby wystąpić błąd na samym początku przy sprawdzaniu pierwszego dozoru pętli. Jest tam bowiem wyrażenie A[k]=x i gdyby wartość A[1] była nieokreślona, to mógłby wystąpić błąd. Również po zakończeniu pętli zaglądamy do A[1] i jeśli przypadkiem znajdzie się tam x, to otrzymamy błędną odpowiedź (powinna być false, a byłaby true). Co gorsza, tego typu błąd może w żadnych testach nie wyjść!

Zauważmy, że dla n\ge 1 wszystko jest w porządku: wszędzie tam, gdzie odwołujemy się do indeksu tablicy A, mieści się on w zakresie określoności [1..n], a gwarantuje nam to właśnie niezmiennik. Zapamiętajmy

Ilekroć odwołujemy się do tablicy, powinniśmy móc udowodnić, że indeks tablicy
mieści się w dziedzinie określoności.

Wyszukiwanie liniowe ze strażnikiem

Podany wyżej algorytm wydaje się tak prosty, że trudno jest cokolwiek uprościć. Pokażemy jego dość istotne ulepszenie, którego wiele odmian stosuje się w podobnych sytuacjach. Zauważmy, że gdybyśmy wiedzieli, że x znajduje się gdzieś w tablicy i na przykład chcieli poznać jego indeks, to nie trzeba byłoby się zabezpieczać przed końcem tablicy i jedynym warunkiem dozoru byłoby A[k]<>x. Pomysł jest następujący. Dodajmy jeden element na końcu tablicy deklarując ją na początku dłuższą o 1 niż potrzeba. Zatem tablica będzie miała zakres [1..n+1], ale prawdziwe wartości, wśród których będziemy szukali x, będą tylko pomiędzy 1 a n.

Oto propozycja programu:

 \{ {\mbox{ n\ge 1}}\}
 k:=1;
 A[n+1]:=x;
 \{{\mbox{ n\ge 1, k=1, A[n+1]=x}}\}
 while A[k]<> x do  {\mbox{\{(\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n+1) \land (A[n+1]=x)}}\}
  k:=k+1; 
 \{{\mbox{ (k\le n) \Leftrightarrow (\exists 1\le j \le n: A[j]=x)}}\}
 jest := k<=n
 \{{\mbox{ (jest) \Leftrightarrow (\exists 1\le j \le n: A[j] = x) }}\}


Zobaczmy jak uprościł się nam program. W warunku dozoru zniknęła koniunkcja oraz konieczność wyliczania jednego warunku logicznego ( k<n). Przez to dowód poprawności też będzie prostszy. Skupmy się na samej pętli. Widać, że przy wejściu do pętli niezmiennik jest prawdziwy – wynika wprost z warunku wstępnego.

Jeśli chodzi o niezmienniczość w czasie wykonywania pętli, podobnie jak zeszłym razem odtworzenie klauzuli

(\forall 1\le j < k: A[j] \neq x)

przy jednokrotnym obrocie pętli jest dość oczywiste. Ostatni warunek A[n+1]=x cały czas zachowuje prawdziwość, bo nic się w tablicy nie zmienia w czasie wykonywania pętli. Najbardziej ambitne będzie pokazanie, że k\le n+1. Dowód tego faktu polega na zauważeniu, że gdy wchodzimy do pętli, to po pierwsze 1\le k \le n+1 - co wynika z poprzedniego obrotu pętli i z założenia indukcyjnego, a po drugie, że A[k] \neq x,co wynika z dozoru pętli. Stąd po uwzględnieniu tego, że A[n+1]=x dostajemy, że k \neq n+1. A skoro 1\le k \le n+1 oraz k\neq n+1, to oznacza, że 1\le k < n+1, czyli 2 \le k+1 < n+2, z czego wnioskujemy, że 1\le k+1 \le n+1, co po przypisaniu k:=k+1 staje się z powrotem 1\le k \le n+1 na mocy reguły przypisania.

Pozostaje udowodnienie, że zaprzeczenie dozoru i niezmiennik razem implikują warunek końcowy, czyli że

((A[k]=x) \land (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n+1) \land (A[n+1]=x)) \Rightarrow ((k\le n) \Leftrightarrow (\exists 1\le j \le n: A[j] = x)).

Tym razem wygodnie będzie nam skorzystać z następującej klasycznej tautologii:

p \Rightarrow (q \Rightarrow r) jest równoważne (p \land q) \Rightarrow r

Ponieważ mamy udowodnić równoważność warunków k\le n oraz \exists 1\le j \le n: A[j] = x, więc osobno pokażemy obie implikacje.

Pierwsza z nich

((A[k]=x) \land (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n+1) \land (A[n+1]=x)) \land (k\le n)) \Rightarrow (\exists 1\le j \le n: A[j] = x).

Ta implikacja jest oczywista: wystarczą trzy warunki z przesłanek: (A[k]=x), 1\le k oraz k\le n, żeby udowodnić tezę.

Druga implikacja:

((A[k]=x) \land (\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n+1) \land (A[n+1]=x)) \land (\exists 1\le j \le n: A[j] = x)) \Rightarrow (k\le n)

jest prawdziwa: ponieważ (\exists 1\le j \le n: A[j] = x), a k jest z przedziału [1..n+1], więc gdyby k było równe n+1, wówczas otrzymalibyśmy sprzeczność z warunkiem mówiącym o tym, że na lewo od k wartości x nie ma, czyli (\forall 1\le j < k: A[j] \neq x), który jest w poprzedniku implikacji.

To kończy dowód poprawności tego algorytmu.

Warto dla dużych tablic przekonać się, że metoda ze strażnikiem jest nieco szybsza niż poprzednia. Przyspieszenie powinno być rzędu kilkunastu procent. Zawsze coś!

Co jednak zrobić, gdy nie mamy wpływu na decyzję o deklaracji tablicy. Ktoś nam daje tablicę, w której mamy namierzyć wartość x i nie ma ekstra elementu o indeksie n+1. Mamy na to sposób.


 {\mbox{ n\ge 1}}
 if A[n]=x then jest := true
 else 
   begin 
   v:=A[n]  // zapamiętujemy ostatnią wartość tablicy
   k:=1;
   A[n]:=x; // i teraz możemy ją zamazać bez obawy o jej utracenie
   while A[k]<> x do // stosujemy znany algorytm ze strażnikiem
     k:=k+1; 
   jest := k<n;   // ten warunek nieco się zmienił
  A[n] := v   // a tutaj odtwarzamy zamazaną wartość
 {\mbox{ (jest) \Leftrightarrow (\exists 1\le j \le n: A[j] = x)}}


Czasem bardzo proste pomysły są niezwykle skuteczne!

Całkowita poprawność programów

Jak na razie umiemy sobie poradzić z programami, które zatrzymają swoje działanie. Problem, czy dany program zatrzyma się dla konkretnych danych jest nierozstrzygalny, więc nie ma ogólnej metody stwierdzania czy nie nastąpi zapętlenie. Nie oznacza to, że jesteśmy bezradni. W wielu przypadkach udowodnić własność stopu możemy i zajmiemy się teraz tym zagadnieniem.

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.

Wizualizacja

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 (\negodd(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.


Liczba obrotów   x    y    z 

0
1
2
3
4

...

-5
-3
-2
-1
-1

 

2
4
8
16
32

 

0
2
6
6
22

 

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;
while (l < p) do
  begin
   s:=(l+p) div 2;
   if x > A[s] then l := s+1
               else p :=s 
  end;
jest := x = A[l]

Wizualizacja

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ą:

if x>=A[s] then l:=s
           else 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; 
while l < p do {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)} 
  begin
   s:=(l+p) div 2;
   if x > A[s] then l:=s+1
               else p:=s
  end;
jest := 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 koniunkcji 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.

Przy okazji 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 przestać zachodzić, 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.