WDP Dowodzenie poprawności programów

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ę, ale 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 skłaniają nas do zapytania, 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ł. Oczywiście typowe zachowanie programisty po napisaniu programu, to 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$, to po wykonaniu jej 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ę za 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.

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\geq 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 nazywamu 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-tych.

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$, to 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:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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$, to 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, to 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 bdziemy zakładali, że istnieje ciąg stanów pośrednich, spełniających pośrednie formuły $\alpha _{1},\ldots ,\alpha _{n}$. Mamy zatem

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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".

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \frac{\mbox {\{\alpha \land B\} P \{\beta\}, (\alpha \land \neg B) \rightarrow \beta}}{\mbox {\{\alpha\}{\tt if B then P } \{\beta\}}} }    Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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ę wyprowadzić z niej. Idea reguły dowodzenia leży w wymyśleniu warunku, który będzie zawsze spełniony na początku pętli. Taki warunek będziemy nazywali 'niezmiennikiem' pętli. Od niezmiennika będziemy wymagali trzech rzeczy.

• żeby był spełniony na początku pętli
• ż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.

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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ę warunek $N$, jakby znikąd. Musimy go sami wymyśleć i jeżeli uda się nam znaleźć $N$ takie, żeby spełniało wszystkie 3 przesłanki, to 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

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \frac{\mbox {\alpha \Rightarrow \gamma, \{\gamma\}P \{ \beta\}}}{\mbox {\{\alpha\}{\tt P} \{\beta\}}}}

Osłabianie tezy

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \frac{\mbox {\{\alpha\} P \{ \gamma\}, \gamma \Rightarrow \beta}}{\mbox {\{\alpha\}{\tt 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\geq 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\geq 0$ jest rónoważne $k+1\geq 1$ i stosując regułę dla instrukcji przypisania otrzymujemy, że $j\geq 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\geq 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  Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{\not 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
 Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox {\not 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

$(\not jest\Leftrightarrow \forall 1\leq j<k:A[j]\neq x)\land (1\leq k\leq 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\geq 0$ oraz $k=1$ mamy też $1\leq k\leq 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 kwartość zmiennej jest równa sie false, to na mocy założenia indukcyjnego zachodzi

$\forall 1\leq 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\leq j<k:A[j]\neq x\land A[j]\neq x$, czyli $\forall 1\leq j\leq k:A[j]\neq x$, a to jest równoważne $\forall 1\leq j<k+1:A[j]\neq x$. Warunek ten obrazuje stan obliczeń po wykonaniu badanej instrukcji warunkowej, gdyż wartość zmiennej {\tt 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 $\not jest=\forall 1\leq 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\leq j\leq k:A[j]\neq x$ będzie fałszywa, czyli równoważna wartości $\not jest$.

Podobnie gdy zmienna jest ma wartość true, to na mocy założenia istnieje $1\leq j<k$ takie że $A[j]=x$. Niezależnie od tego, czy przypisanie jest :=true zostanie wykonane w ramach instrukcji warunkowej, czy nie, po wykonaniu instrukcji k:=k+1 niezmiennik się również odtworzy. To swtierdzenie 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\leq 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

$(\not jest=\forall 1\leq 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\leq 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  Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{\not 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\geq 1$. Oto kolejna wersja rozwiązania problemu wyszukiwania liniowego.

 Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{ n\ge 1}}}

 k:=1;
 Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{ k=1, n\ge 1}}}

 while (k<n) and (A[k]<> x) do Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{(\forall 1\le j < k: A[j] \neq x) \land (1\le k\le n)}}}

    k:=k+1; 
   Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{ (A[k]=x) \Leftrightarrow ((\exists 1\le j \le n: A[j] = x) \land (1\le k\le n))}}}

   jest := A[k]=x
 Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{ (jest) \LeftRightarrow ((\exists 1\le j \le n: A[j] = x) \land (k\le n))}}}

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

Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\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.

 Parser nie mógł rozpoznać (błąd składni): {\displaystyle ((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\geq n)\lor (A[k]=x))\land (\forall 1\leq j<k:A[j]\neq x)\land (k\leq n))\Rightarrow ((A[k]=x)\Leftrightarrow ((\exists 1\leq j\leq n:A[j]=x)\land (1\leq k\leq 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$, czy nie, 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\geq n)\land (\forall 1\leq j<k:A[j]\neq x)\land (1\leq k\leq n))\lor ((A[k]=x)\land (\forall 1\leq j<k:A[j]\neq x)\land (1\leq k\leq 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\geq n)\land (\forall 1\leq j<k:A[j]\neq x)\land (1\leq k\leq n))$, rolę $q$

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

zaś rolę $r$ pełni formuła

$(A[k]=x)\Leftrightarrow ((\exists 1\leq j\leq n:A[j]=x)\land (1\leq k\leq 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\leq n$ oraz $k\geq n$, więc $k=n$. Skoro tak, to w trzecim czynniku koniunkcji wchodzącej w skład $p$ mamy $(\forall 1\leq 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\leq k\leq 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\geq 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łaby 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\geq 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:

 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{ {\mbox{ n\ge 1}}\}}

 k:=1;
 A[n+1]:=x;
 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{{\mbox{ n\ge 1, k=1, A[n+1]=x}}\}}

 while A[k]<> x do  Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\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; 
 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{{\mbox{ (k\le n) \Leftrightarrow (\exists 1\le j \le n: A[j]=)}}\}}

 jest := k<=n
 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{{\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, to podobnie, jak zeszłym razem odtworzenie klauzuli

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

przy jednokrotnym obrocie pętli jest dość oczywiste, tak jak w poprzednim programie. 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\leq n+1$. Dowód tego faktu polega na zauważeniu, że gdy wchodzimy do pętli to – na mocy założenia indukcyjnego $1\leq k\leq n+1$ - to mamy z poprzedniego obrotu pętli – oraz że $A[k]\neq x$ - to mamy z dozoru pętli. Stąd po uwzględnieniu tego, że $A[n+1]=x$ dostajemy, że $k\neq n+1$. A skoro $1\leq k\leq n+1$ oraz $k\neq n+1$, to oznacza, że $1\leq k<n+1$, czyli Parser nie mógł rozpoznać (nieznana funkcja „\lek”): {\displaystyle 2 \lek+1 < n+2} , z czego wnioskujemy że $1\leq k+1\leq n+1$, co po przypisaniu {\tt k:=k+1} staje się z powrotem $1\leq k\leq 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\leq j<k:A[j]\neq x)\land (1\leq k\leq n+1)\land (A[n+1]=x))\Rightarrow ((k\leq n)\Leftrightarrow (\exists 1\leq j\leq 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\leq n$ oraz $\exists 1\leq j\leq n:A[j]=x$, więc osobno pokażemy obie implikacje.

Pierwsza z nich

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

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

Druga implikacja:

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

jest prawdziwa: ponieważ $(\exists 1\leq j\leq 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\leq 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.

 Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\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ść
 Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\mbox{ (jest) \LeftRightarrow (\exists 1\le j \le n: A[j] = x)}}}

Czasem bardzo proste pomysły są niezwykle skuteczne!