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}} \)} 
<b>while</b> (k&lt;n) and (A[k]&lt;&gt; x) <b>do</b> {\( {\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&nbsp;:= A[k]=x
{\( {\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
\( {\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ł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\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.