Dowód poprawności algorytmu

Dowód poprawności algorytmu – rozumowanie matematyczne prowadzące do formalnego wykazania, że dany algorytm przy poprawnych danych wejściowych da nam wynik spełniający wymagania, np. że algorytm quicksort po podaniu mu niepustej tablicy elementów porównywalnych na wyjściu da nam tablicę zawierającą te same elementy, ale uporządkowane w kolejności od najmniejszego do największego.

Dowód poprawności algorytmu zawsze składa się z dwóch części:

  • dowód, że jeśli algorytm się zakończy, to da poprawny wynik,
  • dowód, że przy poprawnych danych wejściowych algorytm zawsze się zakończy.

Do dowodzenia poprawności algorytmów wykorzystywane są zazwyczaj pewne formalizmy matematyczne wiążące ze sobą warunek wstępny, kod oraz warunek końcowy. Większość tych formalizmów opiera się na logice Hoare’a.

W ogólnym przypadku pytanie, czy dany algorytm jest poprawny jest nierozstrzygalne, dla większości języków opisu algorytmów nierozstrzygalne są nawet pytania:

  • czy dane dwa algorytmy dają taki sam wynik,
  • czy dany algorytm dla poprawnych danych wejściowych się kończy (nawet przy założeniu, że zawsze jesteśmy w stanie zweryfikować poprawność danych wejściowych).

Są jednak takie języki, w których np. da się udzielić odpowiedzi na drugie pytanie. Do takich języków należą np. niektóre z odmian rachunku lambda takie jak System F.

Podejście formalne

Niech v = [ v 0 , v 1 , … , v n ] T {\displaystyle v=[v_{0},v_{1},\dots ,v_{n}]^{T}} oznacza wektor danych wejściowych algorytmu Φ , w {\displaystyle \Phi ,w} niech będzie wektorem wynikowym w = [ w 0 , w 1 , … , w m ] T . {\displaystyle w=[w_{0},w_{1},\dots ,w_{m}]^{T}.} Przebieg algorytmu Φ {\displaystyle \Phi } dla dowolnych (w granicy zakładanej poprawności) danych jest jednoznacznie wyznaczony przez ciąg przekształceń:

Φ ( v ) = Φ 0 ( v ) = Φ 1 ( v ′ ) = Φ 2 ( v ″ ) = … = Φ k − 1 ( v ( k − 1 ) ) = Φ k ( v ( k ) ) = w , {\displaystyle \Phi (v)=\Phi _{0}(v)=\Phi _{1}(v')=\Phi _{2}(v'')=\ldots =\Phi _{k-1}(v^{(k-1)})=\Phi _{k}(v^{(k)})=w,}

gdzie v ′ , v ″ , … , v ( k ) {\displaystyle v',v'',\dots ,v^{(k)}} są danymi przejściowymi.

W praktyce należy wykazać, że ciąg przekształceń jest zawsze skończony, oraz wektor w {\displaystyle w} zawiera poprawne dane. Najczęściej stosowaną techniką jest indukcja matematyczna, z zastosowaniem niezmienników pętli.

Przykład

Poprawności algorytmu Euklidesa można dowieść, pokazując, że zdanie:

N W D ( a , b ) = N W D ( b , a   m o d   b ) {\displaystyle NWD(a,b)=NWD(b,a\ mod\ b)}

jest niezmiennikiem pętli algorytmu NWD.

Ponieważ 0 ⩽ a   m o d   b < b , {\displaystyle 0\leqslant a\ mod\ b<b,} wartość drugiego argumentu spada po każdej iteracji, więc algorytm zawsze zakończy działanie.

Z niezmiennika pętli wynika:

N W D ( a , b ) = N W D ( b , a   m o d   b = c ) = N W D ( c , b   m o d   c ) = … = N W D ( z , 0 ) = z . {\displaystyle NWD(a,b)=NWD(b,a\ mod\ b=c)=NWD(c,b\ mod\ c)=\ldots =NWD(z,0)=z.}

A więc, po ostatnim przebiegu pętli algorytm N W D {\displaystyle NWD} zwróci wartość N W D ( a , b ) . {\displaystyle NWD(a,b).}

Zobacz też