Metody dowodzenia poprawności cz II 1

METODY DOWODZENIA POPRAWNOŚCI CZĘŚĆ II

Dowód poprawności całkowitej:

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.

Próba formalizacji dowodzenia poprawności algorytmów:

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ść.