[WikiDyd] [TitleIndex] [WordIndex

To jeszcze nie jest gotowe

Algorytmy i struktury danych

Poprawność algorytmów

Na poprawność algorytmu składają się następujące własnoś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;
   }
}

2015-09-23 06:32