Oto propozycja programu:
\( \{ {\mbox{ n\ge 1}}\} \) k:=1; A[n+1]:=x; \( \{{\mbox{ n\ge 1, k=1, A[n+1]=x}}\} \) <b>while</b> A[k]<> x <b>do</b> \( {\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 – na mocy założenia indukcyjnego \( 1\le k \le 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\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}} \) <b>if</b> A[n]=x <b>then</b> jest := true <b>else</b> <b>begin</b> v:=A[n] // zapamiętujemy ostatnią wartość tablicy k:=1; A[n]:=x; // i teraz możemy ją zamazać bez obawy o jej utracenie <b>while</b> A[k]<> x <b>do</b> // 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!