Dla wykonania całkowitej poprawności trzeba dodatkowo wykazać, że dla każdego napisu S algorytm zatrzyma sie na końcu. O zatrzymaniu decyduje warunek umieszczony w punkcie, gdzie znajduje się asercja 2.
Wprowadzam pojęcie zbieżnika. Za zbieżnik przyjmuje długość napisu X. Na początku ma on pewną wartość, potem jego wartość zmniejsza się o 1 przy każdym obiegu pętli w wyniku wykonania X: = ogon CA. Osiągnięcie zerowej wartości zbieżnika gwarantuje zatrzymanie algorytmu na końcu zgodnie z warunkiem domykającym pętlę (ifX = 0 then...) i jego usytuowaniu (przed STOP). Zatem dla tego prostego algorytmu można przeprowadzić takie dowód poprawności całkowitej.
Spróbujmy sformalizować sposób weryfikacji algorytmów. Mamy warunek początkowy, końcowy i algorytm A rozwiązujący nasze zadanie algorytmiczne. Będziemy chcieli dobrać warunki pośrednie. Okazuje się, że można jedynie sformalizować pomocnicze reguły służące przy konstrukcji asercji. Reguły te zdefiniujemy dla instrukcji wzorowanych na języku PASCAL:
Niech cp — predykat częściowej poprawności u — warunek początkowy w —warunek końcowy asercje
zapis cp (u, A, w) — oznacza, że algorytm A z warunkiem początkowym u i końcowym w jest częściowo poprawny.
1. Instrukcja pusta: cp (u, const, w) u w
2. Instrukcja podstawienia:
cp (u, z: = wyrażenie, w) u (z) w (z / wyrażenie)
gdzie zapis z/wvrażenie oznacza, że w miejsce z podstawiono wartość wyrażenia, predykat oznacza, że z: = w/rażenie jest poprawne częściowo, jeśli z spełnia warunek początkowy, zaś po podstawieniu wartości wyrażenia spełnia warunek końcowy w.
3. Instrukcja sekwencji:
cp (u, begin A1... An end, w) istnieją warunki pośrednie A1 ...An pozwalające na pokazanie, że cp (ui, Ai, wi) dla dowolnego [ = 1....n przy czym u1 = u — pierwszy warunek
Wi = u (i + 1) — i + 1 — warunek pośredni końcowy dla i i początkowy dla i + 1 Wn = W — warunek końcowy
4. Instrukcja warunkowa prosta:
cp (u, if v then I, w) 4=? cp (u and v, I, w) and ((u and not v) w) w — jeśli spełni u i i v — jeśli u i ~v wtedy w
5. Instrukcja warunkowa złożona:
cp (u, if v then 11 else I2, w) 4=4 cp (u and v, 11, w) and cp (u and not v, I2, w)
6. Instrukcja iteracyjna typu while:
cp (u, while v do I, w) 4=4 istnieją warunki pośrednie p1 i p2 takie, że
(u and not v) =4 w (u and v) =4 p1
(p2 and not v) =4 w (wychodzimy z iteracji)
(p2 and v) =4 p1 (wracamy do p1)
cp (p1,1, p2) prawdziwość I z warunku początkowego p1 i końcowego p2
7. Instrukcja iteracyjna typu reoeat — działanie podobne (mogą zapisać na ćwiczeniach — zadania)
I. Czy weryfikacja rozważanego algorytmu może być zautomatyzowana?
1. Trzeba znaleźć wszystkie punkty kontrolne, i z każdym związać niezmiennik
2. Rozmieszczone winny być na: początku, końcu i po jednym w każdej pętli
II. To można zrobić automatycznie!
Ale nie można automatycznie zbudować niezmienników i zbieżników dla dowolnego algorytmu — bo zależą one od algorytmu. DLATEGO NIE MOŻNA DOWODZIĆ AUTOMATYCZNIE PPRAWNOŚCI ALGORYTMU
III. Komputer może natomiast sprawdzać automatycznie czy asercia pozostaje niezmiennicza, co czasami bywa złożone i pracochłonne.
Dlatego do weryfikacji algorytmów najlepiej nadaje się tandem: "człowiek plus maszyna" — człowiek konstruuje asercje dla danego algorytmu, komputer pomaga wybrać punkty kontrolne dla ich umieszczenia i sprawdza ich niezmienniczość.