Poprawność algorytmu

Poprawność składniowa

Poprawność semanty-

czna

Poprawność algorytmu

Wypisywanie zdań z języka

poprawnych składniowo

Poprawne wartościowanie zdań języka, np.

w języku programowania – skutki wystąpienia wyróżnionych części

programu, jak definicje typów, deklaracje stałych i zmiennych, zmian wartościowania

zmiennych będących instrukcjami programu.

Algorytm jako napis może być poprawny składniowo, ale niepoprawny semantycznie, co jest równoznaczne z

niemożnością poprawnego deklarowania i wartościowania zmiennych.

Powody:

 w wyrażeniu występuje argument nie należący do typu związanego z tym wyrażeniem (np. w wyniku działania funkcji otrzymujemy liczbę rzeczywistą, a funkcja miała zwracać wartości całkowite);

wystąpienie w algorytmie pętli o wyrażeniu logicznym stale

wartościowanym jako prawdziwe (pętla będzie wykonywana bez końca);

końcowe wartościowanie zmiennych nie odpowiada oczekiwaniom (program poprawnie kończy obliczenia, ale wyniki nie rozwiązują postawionego zadania).

Niech

A –oznacza algorytm-program,

 -warunek (warunki), jakie powinny spełniać dane wejściowe (początkowe wartościowania zmiennych) algorytmu A,

 -warunek, jaki powinny spełniać końcowe wartościowania zmiennych (własności danych wyjściowych i ich związek z danymi wejściowymi)

Semantyczna poprawność nazywana jest też inaczej pełną poprawnością. Dowodzenie jest trudne. Niekiedy zadowalamy się sprawdzeniem elementów tej definicji.

Semantyczna poprawność

Częściowa semantyczna

poprawność

Własność określoności

dla warunku początkowego

 Własność

stopu

Definicje elementów:

Dowodzenie

Indukcja

Metoda

niezmienników

Własność

stopu

Przykład. Rozważmy algorytm przeszukiwania drzewa binarnego DB zadanego przez wskaźnik na korzeń DB określonego przez zmienną typu el_drzewa

zdefiniowanego następująco:

W dowodzeniu indukcyjnym semantycznej poprawności algorytmu

przeprowadza się zwykle indukcję względem liczby powtórzeń instrukcji iteracyjnej lub poziomu zagnieżdżenia realizacji procedury rekurencyjnej.

struct element {

int wartosc;

element *pien;

element *konar_lewy;

element *konar_prawy;

}

typedef element, *el_drzewa;

struct element {

int wartosc;

element *pien;

element *konar_lewy;

element *konar_prawy;

}

typedef element, *el_drzewa;

int preorder (el_drzewa korzen, int x) {

//{ : korzen !=NULL}

int pom=0;

if ((*korzen).wartosc==x) return 1;

if ((*korzen).konar_lewy!=NULL) //2 pom=preorder((*korzen).konar_lewy,x);

if (pom) return 1; //3 else

if ((*korzen).konar_prawy!=NULL) //4 pom=preorder((*korzen).konar_prawy,x);

if (pom) return 1; //5 else return 0;

//{ : funkcja zwraca 1, gdy "x jest elementem drzewa"}, // zwraca 0, gdy "x nie jest elementem drzewa".}

}

Rozważmy następujący algorytm przeszukiwania drzewa binarnego:

Własność.

Dla dowolnego drzewa binarnego o wysokości wd będącej liczbą naturalną wd>0, algorytm preorder dla danych spełniających  w skończonej liczbie kroków dochodzi do wartościowania końcowego i to wartościowanie spełnia .

Dowód przeprowadzimy indukcyjnie względem parametru określającego wysokość drzewa.

Oznaczmy wysokość drzewa przez wd.

Dla dowodu poprawności semantycznej algorytmu preorder sformułujmy własność:

Krok 1 – sprawdzenie poprawności algorytmu dla początkowej wartości. Należy pokazać, że preorder(korzen) poprawnie określa wynik końcowy dla dowolnego drzewa binarnego o określonym adresie korzenia i wysokości wd=1.

Istotnie, jeśli (*korzen).wartosc==x, to nastąpi koniec wartościowania funkcji i wartością funkcji będzie 1, co będzie oznaczać zajście .

Jeśli (*korzen).wartosc!=x, to wobec  i założenia, że wd=1 mamy

(*korzen).konar_lewy==NULL oraz (*korzen).konar_prawy==NULL. Zatem wobec początkowego wartościowania zmiennej pom=0, nie wykona się żadna z pięciu instrukcji warunkowych i funkcja zwróci 0, co będzie oznaczało zajście .

Ponieważ jedynym miejscem – elementem w drzewie, gdzie może znajdować się pole wartościujące równe x jest pole korzenia, zatem dla wd=1 program jest semantycznie poprawny.

Dowód:

Przeprowadzimy go metodą indukcji matematycznej.

Krok2 – założenie i teza indukcyjna z dowodem.

Załóżmy, że algorytm preorder jest poprawnie określony dla drzew binarnych o wysokości wd<=n.

Udowodnimy, że jest wtedy poprawnie określony dla drzew binarnych o wysokości wd=n+1.

Zał. ind.

Teza. ind.

Istotnie.

Rozważmy drzewo binarne o wysokości wd=n+1.

Jeśli (*korzen).wartosc==x, to nastąpi koniec wartościowania funkcji i wartością będzie 1, co oznacza zajście .

Jeśli (*korzen).wartosc!=x, to nastąpi ewentualne wykonanie kolejnych instrukcji programu (2,3,4,5).

Wobec założenia indukcyjnego, ponieważ lewe i prawe poddrzewo drzewa o wysokości n+1, będą drzewami o wysokościach mniejszych lub równych n, więc instrukcje 2,3,4 zostaną wykonane poprawnie i spowodują wartościowanie funkcji spełniające .

Instrukcja 5 dokona wartościowania funkcji jako 0, jeśli x nie będzie elementem lewego i prawego poddrzewa, czyli nie będzie elementem drzewa.

Zatem wartością funkcji będzie 1, gdy x jest elementem drzewa, 0 – gdy nie jest elementem drzewa, co oznacza zajście .

Zatem na mocy zasady indukcji matematycznej ma miejsce teza własności dla drzew binarnych o dowolnej wysokości wd, co jest równoważne

całkowitej poprawności semantycznej algorytmu preorder wobec definicji 1.

Przykład. Algorytm obliczający wartość wyrażenia 2

+1

int POTEGA_2(int n)

{ //: n>=0

if((n==0)||(n==1)) return n+2;

return 3*POTEGA_2(n-1)-2*POTEGA_2(n-2);

} //: wartością funkcji jest 2

+1.

Przykład algorytmu rekuren- cyjnego (poprzedni też taki był)

Dowód przeprowadzimy indukcyjnie względem parametru n określającego wykładnik potęgi 2.

Dla dowodu poprawności semantycznej algorytmu POTEGA_2 sformułujmy własność:

Własność.

Dla dowolnego wykładnika potęgi o podstawie 2 będącego liczbą naturalną n>=0, algorytm POTEGA_2 dla danych spełniających  w skończonej liczbie kroków dochodzi do wartościowania końcowego i to wartościowanie spełnia .

Krok 1 – sprawdzenie poprawności algorytmu dla początkowej wartości. Należy

pokazać, że POTEGA_2(n) poprawnie określa wynik końcowy dla potęgi o podstawie 2 i wykładniku n=0 lub n=1.

Istotnie, jeśli n=0, to zachodzi warunek if((n==0)||(n==1)) i nastąpi koniec wartościowania funkcji i wartością funkcji będzie n+2, czyli 2, co będzie oznaczać zajście .

Jeśli natomiast n=1, to również zachodzi warunek if((n==0)||(n==1))

i nastąpi koniec wartościowania funkcji i wartością funkcji będzie również n+2, czyli 3, co także będzie oznaczać zajście .

Zatem dla n=0 lub n=1 program jest semantycznie poprawny.

Dowód:

Przeprowadzimy go metodą indukcji matematycznej.

Krok2 – założenie i teza indukcyjna z dowodem.

Załóżmy, że algorytm POTEGA_2 jest poprawnie określony dla potęgi o podstawie 2 i wykładniku k<=n, n=1,2,3….

Udowodnimy, że jest wtedy poprawnie określony dla potęgi o wykładniku n+1.

Zał. ind.

Teza. ind.

Istotnie.

Rozważmy potęgę o podstawie 2 i wykładniku n+1.

Ponieważ n+1>1, to POTEGA_2(n+1) zwróci wartościowanie funkcji spełniające 3*POTEGA_2 ((n+1)-1)-2*POTEGA_2((n+1)-2).

Policzmy:

3*POTEGA_2((n+1)-1)-2*POTEGA_2((n+1)-2)=3*POTEGA_2(n)-2*POTEGA_2(n-1).

Wobec założenia indukcyjnego, ponieważ POTEGA_2(n) i POTEGA_2 (n-1) będą funkcjami

obliczającymi wartość potęgi dla wykładników mniejszych lub równych n, więc zostaną wykonane poprawnie i spowodują wartościowanie funkcji spełniające .

Zatem POTEGA_2(n) zwróci 2ⁿ+1, a POTEGA_2(n-1) zwróci 2^n-1+1.

Możemy więc napisać:

3*POTEGA_2 ((n+1)-1)-2*POTEGA_2 ((n+1)-2)=

=3*POTEGA_2 (n)-2*POTEGA_2 (n-1) =

=3*(2ⁿ+1)-2*(2^n-1+1) =3*2ⁿ+3-2ⁿ-2=2*2ⁿ+1=2ⁿ⁺¹+1, co oznacza zajście .

Zatem na mocy zasady indukcji matematycznej ma miejsce teza własności dla algorytmu POTEGA_2 dla dowolnego wykładnika potęgi n, co jest

równoważne całkowitej poprawności semantycznej algorytmu POTEGA_2 wobec definicji 1.

Wprowadzimy teraz pojęcie niezmiennika pętli, które jest często wykorzystywane do projektowania algorytmów i dowodzenia ich poprawności. Rozważmy pętlę „while”, która ma postać:

Ostatnie stwierdzenie dotyczące prawdziwości zdania g po zakończeniu pętli jest tak oczywistym, że często się o nim zapomina.

Jednak dostarcza ono ważnych informacji pozwalających uzasadnić semantyczną poprawność algorytmów. Dlatego zostało umieszczone w treści twierdzenia.

k=4;

while(k>=4) k=k+1;

Przykład 1.

Algorytm NWD Euklidesa.

Zapis w pseudokodzie

Jak znaleźć niezmiennik pętli?

Najpierw należy pokazać, że

Ćwiczenie

Przykład 2.

Rozważmy algorytm dzielenia całkowitego liczb naturalnych.

void dzielenie (int x,y)

{ //: 0<=x i 0<=y

int q,r;

q=0;

r=x;

while(y<=r) //p: x=q*y+r i 0<=r i 0<=y {

q=q+1;

r=r-y;

};

} //: x=q*y+r i 0<=r<y.

Pokażemy, że algorytm ten jest częściowo poprawny względem warunku początkowego  i końcowego .

Należy udowodnić pewną własność obliczeń algorytmu, która łączy zachodzenie warunku początkowego z warunkiem końcowym.

Jaki warunek spełniają x, y, q, r w pętli „while” w chwili sprawdzenia warunku „y<=r” sterującego iteracją?

Określamy niezmiennik p.

Wykażemy, że za każdym razem, gdy obliczenie algorytmu

rozpoczyna się stanem spełniającym warunek początkowy oraz dochodzi do warunku iteracji, to spełniony jest warunek p.

void dzielenie (int x,y)

{ //: 0<=x i 0<=y

int q,r;

q=0;

r=x;

while(y<=r) //p: x=q*y+r i 0<=r i 0<=y {

q=q+1;

r=r-y;

};

} //: x=q*y+r i 0<=r<y.

Możemy dojść do p dwiema drogami:

bezpośrednio z początku

algorytmu

z pętli

void dzielenie (int x,y)

{ //: 0<=x i 0<=y

int q,r;

q=0;

r=x;

while(y<=r) //p: x=q*y+r i 0<=r i 0<=y {

q=q+1;

r=r-y;

};

} //: x=q*y+r i 0<=r<y.

Jeśli dojdziemy do p z

początku algorytmu, to q=0, r=x i p jest spełniony, bo zachodzi .

Jeśli już przejdziemy przez pętlę „while” i dojdziemy do p, to wiemy, że y<=r i zaszedł już warunek p: x=q*y+r i 0<=r i 0<=y .

Wtedy zostaje wykonana instrukcja złożona: q’=q+1;r’=r-y.

Trzeba sprawdzić, czy dla q’ i r’

zachodzi warunek p:

p: x=q’*y+r’ i 0<=r’ i 0<=y .

Ale

x=(q+1)*y+(r-y)=q*y+r 0<=r’=r-y, bo y<=r i 0<=y.

void dzielenie (int x,y)

{ //: 0<=x i 0<=y int q,r;

q=0;

r=x;

while(y<=r) //p: x=q*y+r i 0<=r i 0<=y {

q=q+1;

r=r-y;

};

} //: x=q*y+r i 0<=r<y.

Stosując teraz indukcję

względem liczby wykonanych sprawdzeń warunku iteracji

„y<=r”, wnioskujemy, że przy każdym sprawdzeniu warunku iteracji zachodzi p.

Zatem, albo cały czas zachodzi „y<=r”i wtedy nie dochodzimy do , albo w pewnej chwili „y>r” i wtedy dochodzimy do , ale ponieważ p był spełniony, więc musi być spełniony .

Zwróćmy uwagę, że jeśli x=0 i y=0, to obliczenie algorytmu jest nieskończone, a więc według podanych warunków algorytm jest tylko częściowo poprawny i ma własność określoności obliczeń, ale nie ma własności stopu!