« poprzedni punkt  następny punkt »

2. Kilka słów o niezmiennikach pętli iteracyjnych

W tym podpunkcie zajmiemy się krótko zagadnieniem, które jest istotne m.in. w dowodzeniu poprawności algorytmów. Ta problematyka będzie szczegółowo i znacznie bardziej formalnie przedstawiona w ramach przedmiotu "Algorytmy i struktury danych". Tutaj w sposób możliwie najmniej formalny zwrócona zostanie uwaga na pojęcie niezmienników pętli iteracyjnych i to raczej pod kątem lepszego rozumienia działania (czy nawet sprawniejszego formułowania) pętli iteracyjnych niż dowodzenia ich poprawności.

Rozpatrzymy najpierw pętlę while (jak już wiemy - pętle for łatwo sprowadzić do pętli while), po czym zobaczymy w jaki sposób, można bezpośrednio formułować niezmienniki dla pętli for.

Ogólną postać pętli while można zapisać jako:

inicjacja_zmiennych_używanych_w_pętli
while (warunek_kontynuacji_pętli) {
    ciało_pętli
}

gdzie przez ciało_pętli rozumiemy instrukcje wykonywane w pętli

Niezmiennikiem pętli while nazywamy relację pomiędzy wartościami zmiennych programu, która jest prawdziwa tuż przed rozpoczęciem pętli, przed każdym wykonaniem i po każdym wykonaniu ciała pętli w kolejnych iteracjach  oraz zaraz po zakończeniu pętli iteracyjnej; przy czym przynajmniej niektóre z wartości zmiennych, uczestniczących w tej relacji, zmieniają się w trakcie wykonywania iteracji pętli.
(Uwaga: jest to definicja nieformalna; formalne definicje będą przedstawione w ramach przedmiotu ASD).

Jeśli przez K oznaczymy wyrażenia-warunek kontynuacji pętli, a przez N - wyrażenie-niezmiennik pętli, to prawidłowa konstrukcja pętli powinna wyglądać następująco:

    // N jest prawdziwe
    while (K) {
        // N i K jest prawdziwe
        ciało pętli
        // N jest prawdziwe
     }
    // N jest prawdziwe i jednocześnie K nie jest prawdziwe

przy czym instrukcje ciała pętli powinny zapewniać (w którymś momencie) zanegowanie wyrażenia K (po to, by pętla mogła zakończyć działanie).

Uwaga: w pętli takiej może zdarzyć się, że od początku K nie jest prawdziwe (wtedy pętla nie wykona się ani razu, ale powinny zachodzić pierwszy i ostatni warunki podane w komentarzach).

Spójrzmy na przykład znajdowania minimalnego elementu tablicy n liczb całkowitych.

 static int getMin(int[] a) {
   int n = a.length;
   int vmin = a[0];
   int i = 1;
   while (i < n) {
     if (a[i] < vmin) vmin = a[i];
     i++;
   }
   return vmin;
 }

Zauważmy, że po zakończeniu pętli chcemy, by spełniony był warunek:
wartość zmiennej vmin jest wartością minimalnego elementu tablicy a czyli minimalną wartością spośród wartości zmiennych a[0], a[1], ... a[n-1].

Inaczej mówiąc wartością wyrażenia (zapisanego w pseudokodzie):

vmin == minimum (a[0], ... ,a[n-1])

winno być true.

Na tej podstawie możemy łatwo wydedukować niezmiennik (który - w tym przypadku - bezpośrednio pomaga nam zbudować algorytm działania pętli).

Niezmiennik: dla  każdego i = 1, ... n :  vmin == minimum ( a[0], .., a[i-1] ).

Miejsca w którym warunek ten powinien być spełniony pokazano poniżej za pomocą komentarza  N z dodatkową liczbą 0, 1, 2, 3 - rozróżniającą umiejscowienie warunku:

 static int getMin(int[] a) {
   int n = a.length;
   int vmin = a[0];
   int i = 1;
   // N0
   while (i < n) {
     // N1
     if (a[i] < vmin) vmin = a[i];
     i++;
     // N2
   }
   // N3
   return vmin;
 }

Niezmiennik ten wyraża określoną relację pomiędzy zmiennymi vmin, a oraz i. Zwróćmy uwagę, że niektóre z tych zmiennych (vmin oraz i) zmieniają swoje wartości  w trakcie iteracji, a jednak wartość wyrażenia stanowiącego niezmiennik powinna być w każdej iteracji taka sama (stąd nazwa niezmiennik!).
Jeżeli możemy teraz wykazać, że wybrany jako niezmiennik warunek jest prawdziwy we wszystkich pokazanych miejscach, pętla kończy działanie, a po jej zakończeniu  z niezmiennika możemy wyprowadzić zamierzony wynik działania pętli, to - nasza pętla jest poprawna (gwoli ścisłości: trzeba jeszcze zapewnić spełnienie jakichś warunków początkowych, w naszym przykładzie będzie to n > 0).

Faktycznie, przed wejściem w pętlę, i=1, vmin = a[0], zatem vmin jest minimum z (a[0]...a[i-1]), bo zbiór ten zawiera tylko jedną liczbę a[0]. Wobec tego w miejscu N0 niezmiennik jest prawdziwy. Jeżeli w miejscu N0 niezmiennik jest prawdziwy, to w pierwszej iteracji - w miejscu N1 również będzie prawdziwy (bo wyrażenie stanowiące warunek kontynuacji nie zmienia wartości i, vmin, oraz elementów tablicy a).
Dalej możemy łatwo wykazać że, jeżeli w jakiejkolwiek iteracji niezmiennik jest prawdziwy w miejscu N1, to będzie również prawdziwy w miejscu N2. Weźmy i-tą iterację. W miejscu N1 zachodzi  vmin == minimum (a[0], ... a[i-1]). Następnie wartość a[i] porównywana jest z wartością vmin, jeśli jest mniejsza, to vmin = a[i], w przeciwnym razie minimum się nie zmienia i w obu przypadkach w miejscu N2 (po zwiększeniu i o 1) znowu zachodzi  vmin == minimum(a[0],  ... . a[i-1]).
Jeśli niezmiennik jest prawdziwy w miejscu N2, to - przy kontynuacji pętli - jest również prawdziwy w miejscu N1. Natomiast gdy warunek kontynuacji nie jest spełniony - prawdziwość w N2 implikuje prawdziwość niezmiennika w N3.
Pętla na pewno skończy działanie, bowiem w każdej iteracji i jest zwiększane, aż osiągnie wartość n.
W miejscu N3 wyrażenie stanowiącc niezmiennik bezpośrednio określa poprawność zamierzonego wyniku działania pętli: otrzymaliśmy minimum ze wszystkich elementów tablicy.

Zobaczmy więc: niezmiennik dobraliśmy tak by "prowadził nas" do końcowego wyniku. Byłoby raczej bez sensu użyć tu jakiegoś innego niezmiennika.
Nie zawsze uda się osiągnąć tak bezpośredni efekt, ale na podstawie dobrze dobranego niezmiennika pętli można znacznie sobie ułatwić  stworzenie poprawnego algorytmu rozwiązania jakiegoś problemu.

No, dobrze, ale czy zawsze musimy przekształcać pętle for do pętli while - by poprowadzić rozumowanie za pomocą niezmienników?
Niekoniecznie. Bardzo często w pętlach for, w których mamy do czynienia z prostą zmianą licznika iteracji  możemy tego nie robić.
Ze względu na konstrukcję takich pętli  (przypomnijmy: inicjacja licznika wykonywana jest raz, warunek kontynuacji sprawdzany jest przed każdym wykonaniem iteracji, a wyrażenie zmieniające licznik wykonywane jest po wykonaniu instrukcji pętli) niezmiennik można "umieścić" na początku każdej iteracji oraz po pętli:

for (.....) {
    // Niezmiennik
    instrukcje pętli
}
// Niezmiennik
     
W naszym przypadku poszukiwania minimum z elementów tablicy moglibyśmy zapisać:

  static int getMin(int[] a) {
    int vmin = a[0];
    for (int i=1; i < a.length; i++) {
      // NIEZMIENNIK: vmin == minimum (a[0],.. a[i-1])
      if (a[i] < vmin) vmin = a[i];
    }
    // NIEZMIENNIK: vmin == minimum (a[0],.. a[i-1])
   return vmin;
     
  }

Łatwo zobaczyć, że niezmiennik jest prawdziwy w każdej iteracji oraz po zakończeniu pętli.


« poprzedni punkt  następny punkt »