Algorytmy i struktury danych
Informatyka, sem IV

Wykład 3: Analiza algorytmów II

Poprawność algorytmów
=====================

Na poprawność algorytmu składają się następujące własności:

- algorytm powinien działać w skończonym czasie;
- algorytm powinien zachowywać się przewidywalnie;
- algorytm powinien wykonywać przewidziane czynności.

Oczywiste jest, że własności tych możemy oczekiwać
przy spełnieniu przez dane wejściowe pewnych wymagań.

Formalnie określamy te wymagania jako tak zwany
"warunek początkowy", natomiast "warunek końcowy" określa
własności danych wyjściowych i ich związek z danymi wejściowymi.

Przykład:

Algorytm Euklidesa wyznaczania NWD liczb n i m:

int nwd( int n, int m ) {
int r= n % m;
while( r != 0 ) {
n= m;
m= r;
r= n % m;
}
return m;
}

Warunek początkowy: n i m są dodatnie
Warunek końcowy: zwrócona liczba jest NWD dla n i m

Warunki początkowy i końcowy mogą być w znanych nam dotąd
językach programowania jedynie opisywane nieformalnie.
W jezyku Eiffel takie warunki realizuje się w postaci
formalnych definicji, co jest praktyczną realizacją tak zwanego
"programowania przez kontrakt", które pozwala traktować
algorytm obudowany w funkcję jako czarną skrzynkę.

Formalna definicja kontraktu w postaci zapisu w języku programowania,
ale też w postaci notacji matematycznej pozwala dowodzić
poprawności algorytmów.

Jeżeli określimy warunek początkowy jako alfa, a koncowy jako beta,
to mówimy, że algorytm A jest semantycznie poprawny względem
warunków alfa i beta jeżeli każde jego wykonanie dla danych
spełniających alfa prowadzi (w skończonym rzecz jasna czasie)
do danych spełniających warunek beta.

Rozważmy algorytm:

for( i= 0; i < n; i++ )
v[i]= fabs( v[i] );

Proszę formalnie określić warunki początkowy i końcowy względem których
algorytm jest semantycznie poprawny.

Poprawności algorytmu dowodzimy wykazując trzy jego własności:

1. Własność stopu:
dla każdych danych wejściowych, spełniajacych warunek początkowy
działanie algorytmu jest skończone

2. Własność określoności:
dla każdych danych wejściowych spełniających ...
działanie algorytmu nie będzie przerwane (tzn. zakończy się normalnie)

3. Własność częściowej poprawności:
ze względu na warunki początkowy i końcowy
dla każdych danych wejściowych spełniajacych ...
jeżeli obliczenie dojdzie do punktu końcowego, to dane wynikowe
spełniają warunek końcowy

Przykład 1 -- algorytm Euklidesa jeszcze raz:

int nwd( int n, int m ) {
/* alfa: n > 0, m > 0 */
int r= n % m;
while( r != 0 ) {
n= m;
m= r;
r= n % m;
}
return m;
/* beta: m jest nwd m,n */
}

ad. 1
W pętli mamy do czynienia z obliczaniem kolejnych wartości r_i
zgodnie z zasadą
r_0 = n % m_0;
r_(i+1)= m_i % r_i;
a ponieważ n % m < m, to r_i stanowią ciąg malejący.
Jeżeli więc m > r_0 > r_1 > ..... >= 0 (bo n % m >= 0),
To algorytm musi się zatrzymać w skończonym czasie,
gdyż r są całkowite

ad. 2
Jedynym dzialaniem, które może spowodowac wyjątek jest
operacja obliczania modulo. Wyjątek wystąpiłby, gdyby
w którymś z wyrażeń m == 0, a to nie jest możliwe,
gdyż n % m nalezy do (m,0>, a dla r == 0 pętla while
nie będzie wykonana.

ad. 3
NWD( m, n ) to największa taka liczba, przez którą dzielą się bez
reszty m i n. Jeżeli n = k*m + r i r > 0, to NWD( m, n ) = NWD( m, r ).

Przykład 2 -- dzielenie całkowite:

Ćwiczenie: podać alfa i beta

int intdiv( int n, int m, int *r ) {
int d= 0;
*r= n;
while( *r >= m ) {
d++;
(*r) -= m;
}
return d;
}

ad. 1
Wartość reszty zmienia się w/g nastepującego schematu:
r_0 = n;
r_(i+1) = r_i - m;
dla n,m dodatnich musi to oznaczać zmniejszanie r, a więc
warunek r >= m przestanie w końcu być prawdziwy.

ad. 2
W algorytmie błąd może spowodować tylko "mazanie po pamięci",
które nie może nastąpić, jesli spełniony jest warunek alfa

ad. 3
w każdym momencie algorytmu spełniony jest warunek
n = d *m + r && r >= 0 && d >= 0
jeżeli więc dojdziemy do sytuacji, gdy r < m, to mamy
spełniony warunek beta

Niezmienniki
============

Waunek wyróżniony w punkcie 3 ostatniego wywodu nazywamy "niezmiennikiem".
Niezmienniki są bardzo przydatne przy analizie i dowodzeniu poprawności
pętli.

Przykład 0 -- bisekcja

int member( double v[], int n, double x ) {
int p= 0;
int k= n-1;
int m;

while( p <= k ) {
m= (p+k)/2;
if( x < v[m] )
k= m-1;
else if( x > v[m] )
p= m+1;
else
return m;
}
return -1;
}

Przykład 1 -- wyszukiwanie w liście z wartownikiem

int member( LISTA l, LISTA w, KLUCZ x ) {
LISTA iterator= l;
w->klucz= x;
while( iterator->klucz != x )
iterator= iterator->nastepny;
return iterator != w;
}

Przykład 2 -- wstawianie do listy jednokierunkowej uporządkowanej:

LISTA add( LISTA l, ELEMENT e ) {
if( l == NULL || l->klucz > e.klucz ) {
e.nastepny= l;
return &e;
else {
l->nastepny= add( l->nastepny, e );
return l;
}
}