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