Analiza algorytmów
Poprawność semantyczna
Analiza algorytmów
Etapy projektowania algorytmów:
Sformułowanie problemu, wybór ADT,
Specyfikacja algorytmu,
Analiza algorytmu,
Testowanie programów implementujących algorytmy.
Aspekty analizy algorytmów:
Złożoność obliczeniowa.
Poprawność semantyczna.
ASD LJ S
1
Poprawność algorytmów
Sposoby dowodzenia poprawności:
Metoda empiryczna (testy funkcjonalne),
Formalne dowodzenie poprawności.
Specyfikacja danych wejściowych i wyników:
Warunki początkowe w odniesieniu do danych wejściowych - asercja
poczÄ…tkowa (precondition).
Warunki końcowe w odniesieniu do wyników - asercja końcowa (postcondition).
Algorytm jest poprawny, gdy dla każdego zestawu danych wejściowych
spełniających asercję początkową wykona się i wyprowadzi wynik spełniający
asercję końcową.
ASD LJ S
Poprawność algorytmów
Metoda empiryczna.
Metoda empiryczna polega na testowaniu pełnej i poprawnej implementacji
poprzez testy funkcjonalne. Dla wielu złożonych algorytmow może to być
przeszkoda, przeważnie chcemy określić poprawność oraz efektywność
algorytmu zanim zainwestujemy w jego implementacjÄ™.
Formalne dowodzenie poprawności algorytmu.
Formalny dowód poprawności algorytmu opiera się na jego formalnej
specyfikacji, która jest niezależna od kodu. W celu udowodnienia poprawności
algorytmu posługujemy się formułami logicznymi zwanymi asercjami, które
związane będą z wybranymi kontrolnymi punktami algorytmu.
ASD LJ S
2
Poprawność semantyczna
Celem dowodu formalnego jest pokazanie, że jeśli dane spełniają wymagane
warunki określone jako warunki początkowe to wynik działania algorytmu będzie
spełniał warunek końcowy.
Należy udowodnić za pomocą formalizmu logicznego i matematycznego, że
algorytm dla właściwych danych wejściowych wyprowadza właściwe wyniki
(zgodność z def. algorytmu).
Specyfikacja danych wejściowych sprowadza się do określenia ich typów oraz
dodatkowego warunku początkowego spełnianego przez te dane (asercja
poczÄ…tkowa).
Specyfikacja wyników (podobnie jak dla danych wejściowych) sprowadza się do
określenia typów danych dla wyników oraz określenia warunku końcowego, który
jest przez te wyniki zawsze spełniony (asercja końcowa).
ASD LJ S
Poprawność semantyczna
Algorytm jest poprawny semantycznie jeśli:
1. Ma własność określoności obliczeń (definiteness property) względem warunków
początkowych, co oznacza dla każdego zestawu danych spełniających warunki
poczÄ…tkowe obliczenia sÄ… wykonywalne (nie sÄ… przerywane).
2. Ma własność stopu (halting property) względem warunków początkowych co
oznacza, że dla każdego zestawu danych spełniających te warunki obliczenia są
skończone (algorytm nie zapętla się).
3. Jest częściowo poprawny (partial corectness) jeżeli dla każdego zestawu danych
wejściowych spełniających warunki początkowe, obliczenia zakończą, a wyniki
spełniają warunki końcowe.
ASD LJ S
3
Niezmienniki pętli
Metoda niezmienników pętli (loop invariants).
Niezmienniki pętli - warunki określane przez zmienne i struktury danych na
początku lub końcu każdego przebiegu pętli.
Niezmiennik pętli formułuje się precyzyjnie aby stwierdzić, że po wyjściu z
pętli algorytm wyprowadzi prawidłowe wyniki.
Etapy dowodzenia poprawności:
1. Wybór niezmiennika pętli,
2. Dowód prawdziwości niezmiennika względem liczby przebiegów pętli.
ASD LJ S
Indukcja matematyczna
Indukcja matematyczna (mathematical induction) - technika dowodzenia.
Przykład.
S(n) - formuła obliczeniowa:
n
S(n)= =
"k n(n+1)
2
k=0
Etapy dowodu indukcyjnego:
1. Przypadek podstawowy (basis case): S(0) - prawdziwa formuła.
2. Krok indukcyjny (inductive step): jeśli dla wszystkich n e" n0 e" 0
S(n) jest prawdziwe to formuła S(n+1) jest prawdziwa.
Zakładając prawdziwość formuły S(n) należy udowodnić, że formuła S(n+1) jest
prawdziwa. S(n) - hipoteza indukcyjna (inductive hypothesis).
ASD LJ S
4
Indukcja matematyczna
Dowód prawdziwości formuły:
n
n(n+1)
S(n) = =
"k
2
k=0
Przypadek podstawowy:
S ( 0 ) = 0
Krok indukcyjny:
?
n ( n + 1 ) ( n + 1)( n + 2 )
S ( n ) = S ( n + 1) =
2 2
Ò!
Ò!
Ò!
Ò!
n (n + 1) (n + 1)( n + 2 )
S ( n + 1) = S (n ) + (n + 1) = + (n + 1) =
2 2
Ð!
Ð!
Ð!
Ð!
(n + 1)(n + 2) n(n + 1)
S (n + 1) = = + (n + 1) = S (n) + (n + 1)
2 2
ASD LJ S
Poprawność algorytmów
Schemat dowodzenia poprawności algorytmu:
Określenie asercji i wybór punktów kontrolnych algorytmu,
Sprawdzenie spełnialności asercji dla algorytmicznych konstrukcji:
- pętli (iteracji),
- instrukcji podstawienia,
- instrukcji sterujÄ…cych,
- wywołań funkcji.
ASD LJ S
5
Niezmiennik pętli
WHILE (warunek) {
Instrukcja
Asercja poczÄ…
Ä…tkowa
Ä…
Ä…
}
inicjowanie
Niezmiennik pÄ™
ętli
Ä™
Ä™
Asercja koń
Å„cowa
Å„
Å„
warunek
warunek
Tak
Nie
Tak
Nie
instrukcje
instrukcje
modyfikacja
ASD LJ S
Poprawność algorytmów
Aby udowodnić, że konkretna formuła jest niezmiennikiem pętli należy wykazać, że:
1. Formuła jest prawdziwa przed pierwszym wykonaniem pętli, (prawdziwość
wynika z warunków początkowych),
2. Jeśli założymy, że formuła jest prawdziwa przed dowolnym przebiegiem pętli, i że
pętla zostanie wykonana ponownie (a więc warunek pętli jest spełniony), to czy
formuła będzie prawdziwa po wykonaniu tej pętli (krok indukcyjny).
ASD LJ S
6
Poprawność algorytmu
n
n(n +1)
S (n) = k =
"
SUM (n)
2
k =0
{
// dane wejściowe:n liczba całkowita
// asercja poczÄ…tkowa: Ä…: ne"
Ä… e"
Ä… e"0
Ä… e"
1. k=0;
n
2. S=0;
// niezmiennik pÄ™tli Å‚: S(k=½k(k+1)'" d"n
Å‚ '" d"
Å‚ '"kd"
Å‚ '" d"
S:=0; k:=0
3. WHILE(k d" n){
4. S=S+k;
k d" n
5. k=k+1;
Tak
Nie
}
return(S(n));
S:=S+k
// asercja koÅ„cowa ²: S(n)=½n(n+1)'" e"0
² '" e"
² '"ne"
² '" e"
S
}
k := k + 1
ASD LJ S
Poprawność algorytmu
Niezmiennik ł jest formułą:
 Wartość S(k) jest wartością sumy k liczb naturalnych
Zauważmy, że to stwierdzenie jest prawdziwe, przed pierwszym wykonaniem iteracji,
kiedy k jest równe 0. Jest również prawdziwe po każdym możliwym wykonaniu pętli.
Wartość S nigdy nie przekroczy ½n(n+1) ponieważ kiedy iteracja siÄ™ zakoÅ„czy
warunek kd" n nie jest spełniony
Aby udowodnić, że ł jest niezmiennikiem pętli należy wykorzystać zasadę indukcji
matematycznej.
ASD LJ S
7
Poprawność algorytmu
Niezmiennik dwuczęściowy:
1. Część związana z liczbą przebiegu pętli,
2. Część związana z ograniczeniem na zmienną sterującą pętlą.
Dowód prawdziwości niezmiennika za pomocą indukcji względem liczby przebiegów
pętli oraz dowód własności stopu.
Dowodzenie własności stopu oparte jest na wartości wyrażenia:
w = n  k
Wielkość n - k maleje z każdym przebiegu pętli (k rośnie natomiast n nie zmienia się).
Ponieważ niezmiennik tej pętli zawiera fakt, że k d" n, wielkość n  k jest ograniczona
od dołu przez 0, zatem pętla musi zakończyć się.
ASD LJ S
Poprawność algorytmu
Sformułowanie problemu: wyznaczenie ilorazu i reszty z dzielenia
całkowitoliczbowego liczb x,y.
DIV (x,y,q,r)
// dane wejściowe: x,y  liczby całkowite;
// asercja poczÄ…tkowa: Ä…: xe" '" y>0;
Ä… e" '"
Ä… e"0 '"
Ä… e" '"
// wyniki: q,r;
// asercja koÅ„cowa: ²: x=q*y+r '" 0d"
² '" d"
² '" d"r² '" d"
{
. . . . . . . .
}
ASD LJ S
8
Poprawność algorytmu
DIV (x,y,q,r)
{
// dane wejściowe: x,y  liczby całkowite;
// asercja poczÄ…tkowa: Ä…: xe" '" y>0;
Ä… e" '"
Ä… e"0 '"
Ä… e" '"
// wyniki: q,r;
q=0;
r=x;
// niezmiennik pętli ł: x=q*y+r '" re" '" y>0;
Å‚ '" e" '"
Å‚ '" e"0 '"
Å‚ '" e" '"
WHILE (y d" r) {
q=q+1;
r=r y;
}
// asercja koÅ„cowa: ²: x=q*y+r '" 0d"
² '" d"
² '" d"r² '" d"
}
ASD LJ S
Dowodzenie poprawności algorytmu
Prawdziwość warunku ł przed pierwszym wykonaniem pętli:
Å‚
Å‚
Å‚
x=x '" x e" 0 '" y > 0
Niezmienniczość warunku ł :
Å‚
Å‚
Å‚
x = (q+1)*y + (r - y) '" r - y e"0 '" y>0
x = q*y + r '" y d" r '" y > 0
Warunek stopu dla r < y:
x = (q+1)*y + (r - y) '" r e"0 '" y>0 '" r < y Ò! x = q*y + r '" 0 d" r ASD LJ S
9
Poprawność algorytmu
Przeszukiwanie liniowe tablicy.
Dane: A, n, x, (A - tablica n-elementowa, x - wartość poszukiwana)
Wynik: Liczba całkowita ind taka, że:
1 d" ind d" n wtedy A[ind] = x,
ind = 0 wtedy  brak elementu o wartości x w tablicy .
ASD LJ S
Dowodzenie poprawności algorytmu
Search (A,n,x) //A-tablica indeksowana od 1 do n;
{
// asercja poczÄ…tkowa: Ä…: ne"
Ä… e"
Ä… e"1;
Ä… e"
1. ind=1;
// niezmiennik pętli ł: ind=k '" A[i]`" dla i=1,2,...,k-1;
Å‚ '" `"
Å‚ '" `"x
Å‚ '" `"
2. WHILE (indd"n and A[ind]`"x) {
3. ind=ind+1;
4. }
5. IF (ind>n) ind=0;
// asercja koÅ„cowa ²: (ind=0 '" A[i]`" dla i=1,2,...n) ("
² '" `" ("
² '" `"x ("
² '" `" ("
(ind=i '" A[i]=x dla 1d" d" n);
'" d" d"
'" d"id"
'" d" d"
}
Dla każdego k=1,2,...,n+1, jeśli sterowanie dociera do linii 2 po raz k-ty, to spełniony
jest następujący niezmiennik pętli: ind = k '" A[i] `"x dla i=1,2,...,k-1.
ASD LJ S
10
Dowodzenie poprawności algorytmu
1. Przypadek podstawowy:
Niech k=1. Wówczas ind=k=1 i nie istnieje i2. Krok indukcyjny:
Jeżeli warunki te są spełnione dla pewnego kk+1.
Na podstawie założenia indukcyjnego, gdy linia 2 wykonywana jest po raz k-ty
to:
ind=k '" A[i] `"x dla 1d"i< k,
Jeśli warunki w linii 2 sprawdzane są po raz (k+1)-szy to wnioskujemy, że były
one spełnione po raz k-ty, zatem:
A[ind] `"x '" A[k] `"x.
ASD LJ S
Dowodzenie poprawności algorytmu
Uzasadnienie asercji końcowej.
1. Wynik ind=0 otrzymujemy wtedy i tylko wtedy, gdy k=n+1.
Na podstawie prawdziwości niezmiennika pętli wnosimy:
dla każdego i=1,2,..., n, A[i]`"x.
2. Wynik ind=k d" n otrzymujemy wtedy i tylko wtedy gdy pętla zakończyła się
(A[k] = x).
Pozycją pierwszego wystąpienia wartości x w tej tablicy jest k
ponieważ A[i] `"x dla i=1,2,...k-1.
ASD LJ S
11


Wyszukiwarka

Podobne podstrony:
nw asd w3
nw asd w2
nw asd w9
nw asd w2
nw asd w1
nw asd w6
nw asd w7
nw asd w8
nw asd w5
nw asd w10
nw asd w11
nw asd w4

więcej podobnych podstron