1

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

2

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

).

ASD

LJ

S

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ą.

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ę.

ASD

LJ

S

 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.

3

Poprawność semantyczna

ASD

LJ

S

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).

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

4

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:

2

)

1

(

)

(

0

+

=

=

∑

=

n

n

k

n

S

n

k

Etapy dowodu indukcyjnego:

1. Przypadek podstawowy (

basis case

): S(0) - prawdziwa formuła.

2. Krok indukcyjny (

inductive step

): jeśli dla wszystkich n

≥ n

0

≥ 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

5

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

Indukcja matematyczna

2

)

1

(

)

(

0

+

=

=

∑

=

n

n

k

n

S

n

k

Dowód prawdziwości formuły:

2

)

2

)(

1

(

)

1

(

2

)

1

(

)

1

(

)

(

)

1

(

+

+

=

+

+

+

=

+

+

=

+

n

n

n

n

n

n

n

S

n

S

)

1

(

)

(

)

1

(

2

)

1

(

2

)

2

)(

1

(

)

1

(

+

+

=

+

+

+

=

+

+

=

+

n

n

S

n

n

n

n

n

n

S

⇒

⇒

⇒

⇒

⇐

⇐

⇐

⇐

0

)

0

(

=

S

2

)

1

(

)

(

+

=

n

n

n

S

Przypadek podstawowy:

Krok indukcyjny:

2

)

2

)(

1

(

)

1

(

+

+

=

+

n

n

n

S

?

ASD

LJ

S

6

Niezmiennik pętli

WHILE (warunek) {

Instrukcja

}

Nie

Tak

instrukcje

warunek

Niezmiennik pę

ęę

ętli

Nie

Tak

modyfikacja

instrukcje

inicjowanie

warunek

Asercja począ

ąą

ątkowa

Asercja koń

ńń

ńcowa

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

7

Poprawność algorytmu

Nie

Tak

k := k + 1

S:=S+k

S:=0; k:=0

k

≤ n

n

S

2

)

1

(

)

(

0

+

=

=

∑

=

n

n

k

n

S

n

k

SUM (n)
{

// dane wejściowe:n–liczba całkowita

// asercja początkowa:

α

α

α

α: n≥

≥

≥

≥0

1. k=0;
2.

S=0;

// niezmiennik pętli

γγγγ: S(k=½k(k+1)∧

∧

∧

∧k≤

≤

≤

≤n

3.

WHILE(k

≤ n){

4.

S=S+k;

5.

k=k+1;

}

return(S(n));

// asercja końcowa

β

β

β

β: S(n)=½n(n+1)∧

∧

∧

∧n≥

≥

≥

≥0

}

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 k

≤ n nie jest spełniony

ASD

LJ

S

Aby udowodnić, że

γ

jest niezmiennikiem pętli należy wykorzystać zasadę indukcji

matematycznej.

8

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

≤ 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:

α

α

α

α: x≥

≥

≥

≥0 ∧

∧

∧

∧ y>0

;

// wyniki: q,r;

// asercja końcowa:

β

β

β

β: x=q*y+r ∧

∧

∧

∧ 0≤

≤

≤

≤r<y

;

{

. . . . . . . .

}

ASD

LJ

S

9

Poprawność algorytmu

DIV (x,y,q,r)

{

// dane wejściowe: x,y – liczby całkowite;

// asercja początkowa:

α

α

α

α: x≥

≥

≥

≥0 ∧

∧

∧

∧ y>0

;

// wyniki: q,r;

q=0;

r=x;

// niezmiennik pętli

γγγγ: x=q*y+r ∧

∧

∧

∧ r≥

≥

≥

≥0 ∧

∧

∧

∧ y>0

;

WHILE (y

≤ r) {

q=q+1;

r=r–y;

}

// asercja końcowa:

β

β

β

β: x=q*y+r ∧

∧

∧

∧ 0≤

≤

≤

≤r<y

;

}

ASD

LJ

S

Dowodzenie poprawności algorytmu

Prawdziwość warunku

γγγγ przed pierwszym wykonaniem pętli:

x=x

∧ x ≥ 0 ∧ y > 0

Niezmienniczość warunku

γγγγ

:

x = (q+1)*y + (r - y)

∧ r - y ≥0 ∧ y>0

x = q*y + r

∧ y ≤ r ∧ y > 0

Warunek stopu dla r < y:

x = (q+1)*y + (r - y)

∧ r ≥0 ∧ y>0 ∧ r < y ⇒ x = q*y + r ∧ 0 ≤ r <y

ASD

LJ

S

10

Poprawność algorytmu

Przeszukiwanie liniowe tablicy.

Dane: A, n, x, (A - tablica n-elementowa, x - wartość poszukiwana)

Wynik: Liczba całkowita ind taka, że:

1

≤ ind ≤ 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:

α

α

α

α: n≥

≥

≥

≥1

;

1.

ind=1;

// niezmiennik pętli

γγγγ: ind=k ∧

∧

∧

∧ A[i]≠

≠

≠

≠x dla i=1,2,...,k-1

;

2.

WHILE (ind

≤n

and

A[ind]

≠x) {

3.

ind=ind+1;

4.

}

5.

IF

(ind>n) ind=0;

// asercja końcowa

β

β

β

β: (ind=0

∧

∧

∧

∧

A[i]

≠

≠

≠

≠x dla i=1,2,...n) ∨

∨

∨

∨

(ind=i

∧

∧

∧

∧ A[i]=x dla 1≤

≤

≤

≤i≤

≤

≤

≤ n);

}

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

11

Dowodzenie poprawności algorytmu

1.

Przypadek podstawowy:

Niech k=1. Wówczas ind=k=1 i nie istnieje i<k, dla którego A[i]=x.

2.

Krok indukcyjny:

Jeżeli warunki te są spełnione dla pewnego k<n+1, to zachodzą również dla
k+1.

Na podstawie założenia indukcyjnego, gdy linia 2 wykonywana jest po raz k-ty
to:

ind=k

∧ A[i] ≠x dla 1≤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

≤ 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