Wstęp do programowania w języku C/Poprawność programów, niezmienniki

From Studia Informatyczne

Poprawność algorytmu.

Autor algorytmu powinien znać jego przeznaczenie. Czasem ten sam algorytm może być użyty do różnych celów. Niemniej pisząc algorytm K chcemy wypowiedzieć się na temat jego przeznaczenia i zgodności z tym przeznaczeniem.

Na przykład algorytm Euklidesa, o parametrach n i m, ma za zadanie dla dowolnych liczb całkowitych n>0, m>0 wyznaczyć ich największy wspólny dzielnik.

Ogólnie, algorytm K ma zawsze pewien zestaw danych wejściowych D oraz pewien zestaw wyników W. Jednakże nie dla wszystkich możliwych danych z D nasz algorytm K ma działać, na przykład dla n=4, m=0 algorytm Euklidesa nie musi działać poprawnie. Zatem mówiąc o zgodności algorytmu z zalożeniami zadania, mamy zawsze na myśli zestawy danych spełniające warunek początkowy (zwany także warunkiem wejściowym). Podobnie z własnością wyników. Otóż wyniki, aby algorytm był zgodny z założeniami zadania, muszą spełniać warunek końcowy (zwany warunkiem wyjściowym).

Będziemy te warunki zapisywać w następujący sposób:

\begin{array}{c}      \{ \alpha \}\\        K\\      \{ \beta \} \end{array}

a czasem \{ \alpha \} K \{ \beta \}. Oznacza to, że jeśli dane d spełniają warunek wejściowy \alpha oraz algorytm K ma dla tych danych skończone obliczenie, to wyniki w spełniają \beta. Może się zdarzyć, że algorytm K jest częściowo poprawny, a jednak nie zadawala naszych oczekiwań. Na przykład wtedy, gdy jego obliczenie będzie nieskończone. Będziemy zatem zainteresowani własnością algorytmu, która zapewni nas, że nie ma on obliczenia nieskończonego dla interesujących nas zestawów danych.

Podobnie ważną własnością algorytmów jest określoność obliczeń, to znaczy, że algorytm nigdy nie wychodzi poza dziedzinę obliczeń i obliczenie nigdy nie będzie przerwane (np. nie wystąpi dzielenie przez 0).

Bardziej formalnie. Rozważać będziemy zatem następujące ważne własności algorytmów:

  1. Dla danych d spełniających \alpha, jeżeli obliczenie algorytmu K dochodzi do punktu końcowego, to otrzymane wyniki spelniają \beta.
  2. Dla każdych danych d spełniających warunek \alpha obliczenie K nie jest przerwane.
  3. Dla każdych danych d spełniających \alpha obliczenie K nie jest nieskończone.
  • Warunek (1) nazywa się częściową poprawnością.
  • Warunek (2) nazywa się określonością obliczeń.
  • Warunek (3) nazywa się własnością stopu.

Jeżeli zachodzi (1) & (2) & (3), to nazywamy to całkowitą poprawnością algorytmu K względem warunku wejściowego \alpha i wyjściowego \beta. Warunki \alpha i \beta nazywa się też specyfikacją algorytmu. Zatem gdy zachodzi (1) & (2) & (3) mówimy także, że algorytm K jest zgodny ze specyfikacją zadania.

Niezmienniki

Proste algorytmy najczęściej nie wymagają szczegółowej formalnej analizy poprawności. Autor siada, projektuje algorytm i pisze program. Testuje go na komputerze, i po skończonej liczbie znalezionych i usuniętych błędów uznaje, że algorytm (program) jest poprawny.

Taka metoda nie zawsze jest właściwa. Po pierwsze projekt może być zły. Po drugie rozumowania ad hoc mogą mieć błąd pierworodny, trudny do wykrycia już w fazie testowania. Po trzecie testowanie nie jest jedyną możliwą metodą sprawdzania poprawności programu.

Zajmiemy sie najpierw metodami wykazywania częściowej poprawności algorytmu. Pewną wygodną i powszechnie stosowaną metodą wykazywania częściowej poprawności algorytmów jest metoda niezmienników.

Mówimy, że warunek g jest niezmiennikim instrukcji I w algorytmie K w wyróżnionym jej miejscu przy warunku wejściowym \alpha, jeżeli dla każdego obliczenia K spełniającego warunek początkowy \alpha, za każdym razem, gdy obliczenie dochodzi do wyróżnionego miejsca instrukcji I, bieżące wartości zmiennych spełniają warunek g.

Przykład:

Napiszemy program na wyznaczanie potęgi x^n. Danymi wejściowymi są liczba rzeczywista x i naturalna n. Wynik ma być równy x^n..

#include <stdio.h>
 
main()
{
  double x, y, z;
  int n, m;
  printf("Podaj rzeczywiste x i naturalne n: ");
  scanf("%lf %d", &x, &n);
  /* Zakladamy, ze dane sa poprawne. */
 
  /* warunek alfa: n >= 0, x - liczba rzeczywista */
  z=x;
  y=1.;
  m=n;
  do{
   /* Niezmiennik: x^n = y*z^m & m>=0 */
   if ( (m % 2) == 1 )
     y = y*z;
     z = z*z;
     m = m/2;
   /* Niezmiennik: x^n = y*z^m & m>=0 */
  }
  while (m != 0);
  /* warunek beta: y = x^n */
 
  printf("%5.2f^%d = %10.2f\n", x, n, y);
 
  return 0;
 
}

Dowód niezmienniczości g prowadzi się przez indukcję. Dla pierwszego wejścia w pętlę mamy z=x, y=1, m=n, wiec z \alpha wynika g.

Teraz krok indukcyjny. Jeżeli m jest parzyste, to niech z'=z*z, m'=m/2, y'=y będą nowymi wartościami z, m i y, odpowiednio. Czyli, y'*(z')^{m'}=y*(z*z)^{m/2}=y*z^m=x^n z założenia indukcyjnego, oraz m' \geq 0. Jeżeli m jest nieparzyste, to z'=z*z, m'=(m-1)/2, y'=y*z, czyli y'*(z')^{m'}=(y*z)(z*z)^{(m-1)/2}=y*z^m=x^n$ z założenia indukcyjnego, oraz m' \geq 0.

Dla naszego przykładu mamy z niezmiennika na końcu pętli x^n=y*z, czyli warunek końcowy \beta jest spełniony.

W tym algorytmie mamy także poprawność. Własność określoności obliczeń otrzymujemy natychmiast z wykonalności wszystkich operacji. Własność stopu można dowieść ze względu na wartość m. Otoż z niezmiennika g mamy również m\geq 0. W każdym kroku pętli wartość m maleje. Ponieważ nie istnieje ciąg nieskończony i malejący liczb naturalnych, zatem musi być taki krok pętli, w którym m=0. A to dowodzi stopu algorytmu.

Wniosek ogólny z tego przykładu wynika następujący. Dla petli postaci

\{ \alpha \} do \{ g \}  K \{ g \} while ({\it W}) \{ \beta \}

z niezmiennikiem g, aby wykazać częściową poprawność wystarczy pokazać implikację

g \& !W \Rightarrow \beta.

Podobnie dla pętli postaci

\{ \alpha \} while ({\it W}) \{ g \}  K \{ g \} \{ \beta \}

z niezmiennikiem g, aby wykazać częściową poprawność wystarczy pokazać implikację

g \& !W \Rightarrow \beta.