3. Poprawność programu

3.1. Wprowadzenie

Programiści dzielą się na dwie kategorie: tych, którzy piszą programy, i tych, którzy piszą działające programy. Książka ta jest przeznaczona dla należących do tej drugiej kategorii lub do tego aspirujących.
Istnieją dwa sposoby przekonania się o poprawności napisanego kodu. Są to testowanie programu z zastosowaniem takich metod, jak "analiza na sucho" (sprawdzanie pracy programu przez analizę tekstu bez wykorzystania komputera), kontrola drobiazgowa struktury programu lub testy funkcjonalne oraz weryfikacja programu, polegająca na przeprowadzeniu logicznego dowodu poprawności kodu we wszystkich przypadkach. Zazwyczaj programiści znają pierwszą grupę metod, ale bywają słabo zorientowani w drugiej. Niniejszy rozdział dotyczy właśnie weryfikacji programów.
Weryfikacja programu opiera się na jego specyfikacji, która jest czymś niezależnym od kodu programu. Specyfikacja wyraża, co program ma robić, i określa związek między jego danymi wejściowymi i wyjściowymi. Powinna być przy tym krótsza i łatwiejsza do zrozumienia niż sam kod. Weryfikacja powinna przede wszystkim potwierdzić, że kod programu jest zgodny z jego specyfikacją. Ten fragment procesu weryfikacji jest zwany sprawdzaniem częściowej poprawności.
Oprócz pokazania, że program jest zgodny ze specyfikacją, zwykle chcielibyśmy też dowieść, że program zakończy działanie, jeśli jego dane wejściowe będą poprawne, czyli wykazać tak zwaną własność stopu programu.
Na początku tego rozdziału pokazujemy, jak dowodzić częściowej poprawności programów nie zawierających pętli, a następnie, jak uzasadniać poprawność pętli. W dalszej części rozdziału omawiamy sposób dowodzenia własności stopu.

3.2. Warunki wstępne i końcowe

Specyfikacja programu składa się z dwóch części. Powinna zawierać warunek dotyczący danych wejściowych, który musi być spełniony na początku programu.
48
Warunek ten nosi nazwę warunku wstępnego (ang. precondińon) lub asercji początkowej. Jeżeli dane wejściowe nie spełniają tego warunku, to nie ma gwarancji, że program będzie działał poprawnie ani nawet, że się zatrzyma. Warunek końcowy (ang. postcondition) lub asercja końcowa opisuje, co program oblicza, przy założeniu, że się zatrzyma. Jest to warunek dotyczący wyjścia programu, który jest zawsze prawdziwy po wykonaniu programu, jeśli zachodził warunek wstępny. Rozważmy dla przykładu następujący program:

#include
#include

main()
{
double x;

scanf ( "%1f " , &x) ;
printf("%1f", sqrt(x));
}

Warunkiem wstępnym jest to, że wejście, stdin, zawiera na początku liczbę nieujemną, a końcowym jest to, że program wypisze pierwiastek kwadratowy pierwszej liczby z wejścia. Jeśli warunek wstępny nie jest spełniony, to nie ma gwarancji, jak program będzie działał.
Aby wykazać, że program jest zgodny ze specyfikacją, trzeba podzielić ją na wiele kroków, podobnie jak dzieli się na kroki sam program. Każdy krok programu ma własny warunek wstępny i końcowy. Warunek wstępny będziemy zapisywać jako komentarz przed danym krokiem, a warunek końcowy jako komentarz po danym kroku. Na przykład wiersz

/* A */ s /* B */

oznacza, że A jest warunkiem wstępnym, S - kodem danego kroku, a B - jego warunkiem końcowym. Krokiem może być dowolna jednostka w programie: pojedyncza instrukcja przypisania, blok, pętla, funkcja albo cały program.
Przyjrzyjmy się najpierw prostej instrukcji przypisania v = x;, gdzie v jest zmienną, a x pewnym wyrażeniem. Aby wykazać, że warunek końcowy jest spełniony po wykonaniu tego kroku, jeśli prawdziwy był warunek wstępny, zastępujemy każde wystąpienie zmiennej v w warunku końcowym B wyrażeniem x. Jeśli ta nowa formuła wynika z warunku wstępnego A, to specyfikacja jest poprawna. Oto przykład zawierający warunek wstępny, instrukcję przypisania i warunek końcowy:

/*x>=0*/x = x+1; /* x >= 1*/

Dowodzimy poprawności specyfikacji przez podstawienie wyrażenia x + 1 pod każde wystąpienie x w warunku końcowym. Daje to formułę x + 1 >= 1, która wynika z warunku wstępnego x >= 0. Zatem specyfikacja dla tej instrukcji podstawienia jest poprawna.


49

Istnieją cztery sposoby łączenia prostych kroków w celu otrzymania kroków bardziej złożonych. Są to: stosowanie instrukcji złożonych (bloków instrukcji wykonywanych sekwencyjnie), stosowanie instrukcji wyboru, stosowanie instrukcji powtarzania (pętli) i wywołania funkcji. Każdej z tych metod budowania kodu odpowiada metoda przekształcania warunku wstępnego i końcowego w celu wykazania poprawności specyfikacji kroku złożonego. Najprostszy jest przypadek sekwencyjnego wykonywania instrukcji. Jeśli dane są dwa kolejne kroki i warunek wstępny drugiego kroku wynika z warunku końcowego kroku pierwszego, to warunek końcowy kroku drugiego będzie zachodził po wykonaniu obu kroków, o ile warunek wstępny kroku pierwszego był spełniony. Jeśli na przykład mamy

/* x >= 1 */ y = x; /* y >= 1 */
/* y >= 1 */y = y+1; /* y >= 2 */
to najpierw sprawdzamy, że specyfikacja każdego kroku z osobna jest poprawna. Podstawienie x w miejsce y w warunku końcowym pierwszego kroku dowodzi prawdziwości jego specyfikacji, a dowód dla drugiego kroku jest analogiczny do zamieszczonego wyżej. Ponieważ warunek wstępny drugiego kroku wynika z warunku końcowego pierwszego kroku (faktycznie jest identyczny), dowiedliśmy, że
/*x>=1*/y = x;y = y+1; / * y >= 2 * /

jest poprawną specyfikacją.
Aby wykazać prawdziwość specyfikacji instrukcji wyboru, takiej jak instrukcja i f, należy dowieść, że warunek końcowy wynika z warunku wstępnego i warunku testu w każdym z przypadków instrukcji wyboru. Rozważmy instrukcję i f wraz z częścią else. Mamy tu dwa przypadki: test jest zdaniem prawdziwym albo nie. Aby udowodnić poprawność tej instrukcji, musimy wykazać, że kiedy test jest spełniony, wykonanie instrukcji następującej za testem implikuje warunek końcowy, przy założeniu warunku wstępnego i prawdziwości testu. Z drugiej strony musimy także wykazać, że warunek końcowy zachodzi po wykonaniu instrukcji następującej po else, jeśli był spełniony warunek wstępny, a test - nie. Rozważmy na przykład następującą instrukcję wyboru:

/* x >= 0 */
if (x > 5)
x = x - 2 ;
else
x = x + 1 ;
/* x >= l */

W celu wykazania poprawności tej specyfikacji musimy udowodnić dwie rzeczy:

/*x>=0&&x>5*/x = x-2; / * x >= 1 * /
/*x>=0&&x<=5*/x = x+1; / * x >= 1 * /

50

Zastosowanie reguły dla przypisania do pierwszej instrukcji pokazuje, że specyfikacja jest spełniona w tym przypadku, ponieważ zdanie x - 2 >= 1 wynika z warunku x > 5. Wcześniej już przekonaliśmy się o prawdziwości specyfikacji w drugim przypadku. Zatem warunek końcowy powyższej instrukcji i f jest prawdziwy po jej wykonaniu, jeśli zachodził warunek wstępny.
Funkcje, podobnie jak inne fragmenty kodu, mają swoje warunki wstępne i końcowe. Warunek wstępny określa zależności, jakie muszą spełniać parametry wejściowe i zmienne globalne używane przez funkcję. Warunek końcowy dotyczy zwracanej wartości i wszystkich parametrów wyjściowych funkcji oraz wszystkich modyfikowanych przez nią zmiennych globalnych. Dodatkowo, jeśli funkcja wczytuje jakieś dane, to warunek wstępny wyznacza ograniczenia, jakim muszą one podlegać. Jeśli funkcja zapisuje dane wyjściowe, to warunek końcowy musi określać, co jest zapisywane. Sprawdzanie specyfikacji dla treści funkcji odbywa się tak samo, jak dla każdej specyfikacji w programie.
Kiedy funkcja jest wywoływana przez program główny lub inną funkcję, musimy sprawdzić, że warunek wstępny funkcji wynika z warunku wstępnego kroku wywołania, a warunek końcowy funkcji pociąga za sobą warunek końcowy kroku wywołania.

3.3, Niezmienniki pętli
Wykazanie poprawności specyfikacji dla pętli wymaga użycia niezmiennika pętli. Niezmiennik pętli określa warunki, które są zawsze spełnione przez zmienne w pętli, a także przez wartości wczytane lub wypisane, jeśli pętla zawiera operacje odczytywania lub zapisywania. Warunki te muszą być prawdziwe przed pierwszym wykonaniem pętli oraz po każdym jej obrocie. Mogą one chwilowo stawać się fałszywe w trakcie wykonywania wnętrza pętli, ale muszą ponownie stawać się prawdziwe przy końcu każdej iteracji.
Rozważmy następujący fragment programu:

int i ;

i = 0;
while (i <= 12) {
printf("Witaj świecie!\n");
i = i + 1;

Co otrzymamy w wyniku działania tego programu?
W pierwszym odruchu wielu programistów stwierdzi, że ta pętla spowoduje wypisanie zdania "Witaj świecie! \n" 12 razy. Uważniejsi, a i pozostali po krótkiej analizie, odpowiedzą, że zdanie to jest w rzeczywistości wypisywane 13 razy. Fakt, że nawet ten króciutki kawałek kodu jest niełatwy do właściwego odczytania, ilustruje trudności, jakie sprawiają pętle.

51
Jak możemy przekonać kogoś, że powyższa pętla spowoduje, iż zdanie "Witaj świecie !\n" zostanie wypisane 13 razy? Argumentacja wygląda zwykle następująco:
Jasne jest, że podczas każdego wykonania pętli wypisuje się zdanie "Witaj świecie ! \n" . Ponieważ zmienna i przebiega wartości od O do 12, pętla wykonuje się 13 razy. Zatem zdanie zostanie wypisane 13-krotnie.
Aby związek między zmienną i a liczbą wykonań pętli uczynić wy raźniej szy m, moglibyśmy wskazać, że wartość i jest zawsze równa temu, ile razy zostało wykonane wnętrze pętli; pętla zawsze ma za sobą i obrotów. Ponieważ i jest równe 13, kiedy pętla się kończy, więc pętla wykona się trzynaście razy, a za każdym razem program wypisze zdanie "Witaj świecie! \n".
To, ile razy pętla się wykona, interesuje nas jedynie jako droga do wywnioskowania, co zostanie wypisane. Możemy sformułować związek między wartością i a tym, ile razy zostało wypisane zdanie "Witaj świecie ! \n" , jako:
Zdanie "Witaj świecie!\n" jest wypisane i razy.
Zauważmy, że to stwierdzenie jest prawdziwe, zanim pętla zostanie choć raz wykonana, kiedy i jest równe O, a zdanie nie zostało ani razu wypisane. Jest również prawdziwe po każdym wykonaniu wnętrza pętli, kiedy zdanie zostaje wypisane kolejny raz, a wartość i zwiększa się o 1. Stwierdzenie staje się jednak chwilowo fałszywe podczas wykonywania wnętrza pętli. Konkretnie, kiedy zdanie zostało już wypisane, ale wartość zmiennej nie została jeszcze powiększona, stwierdzenie staje się nieprawdziwe. Drugi wiersz wnętrza pętli powoduje jednak, że staje się ono znowu prawdziwe. Powyższy argument wykazuje w zasadzie, że nasze stwierdzenie jest niezmiennikiem. W dalszej części rozdziału powiemy bardziej szczegółowo, jak dowodzić, że jakieś zdanie jest niezmiennikiem.
Pokażemy, że wartość i wynosi 13, kiedy pętla kończy działanie, formułując niezmiennik dotyczący maksymalnej wartości i. Wartość i nigdy nie przekracza 13, a podczas ostatniego przebiegu pętli i staje się równe 13. Ponieważ stwierdzenie to jest prawdziwe po każdym wykonaniu pętli, więc pozostaje prawdziwe, gdy pętla się zakończy. Kiedy pętla się kończy, warunek pętli i < 12 musi być fałszywy, a więc i > 12. Ponieważ i jest liczbą całkowitą większą od 12, ale nie przekraczającą 13, musi być równe 13. Zatem kiedy pętla się kończy, wartość i wynosi 13, a zdanie "Witaj świecie! \n" jest wypisane i, czyli 13 razy.
Kompletnym niezmiennikiem tej prostej pętli jest:
Zdanie "Witaj świecie! \n" jest wypisane i razy oraz i < =13.
Chociaż nie wiemy jeszcze, jak uzasadnić, że to stwierdzenie jest niezmiennikiem pętli, wiemy jednak, że nim jest. Możemy wykazać, iż to stwierdzenie wraz z zaprzeczeniem warunku pętli dowodzą, że pętla powoduje wypisanie zdania 13 razy.
Może się wydawać, że włożyliśmy mnóstwo pracy w wykazanie, że tak prosta pętla działa poprawnie. Tak łatwo jednak popełnić pomyłkę, nawet w najprostszej

52

pętli, że opłaca się trud zapisania zdania opisującego zmienne pętli, wejście i wyjście, sprawdzenia, że jest ono niezmiennikiem, i wykorzystania jego prawdziwości w dowodzie, że pętla jest poprawna.

3.3.1.Dowodzenie niezmienników

Aby udowodnić, że zdanie jest niezmiennikiem pętli, wykorzystamy zasadę indukcji matematycznej. Mówi ona, że jeśli (1) pewne zdanie jest prawdziwe dla liczby O oraz (2) z tego, że jest ono prawdziwe dla pewnej liczby n >= O wynika, że musi też być prawdziwe dla liczby n + 1, to (3) zdanie to jest prawdziwe dla wszystkich liczb nieujemnych. Intuicyjnie wydaje się to słuszne, ponieważ zdanie jest prawdziwe dla liczby O, na podstawie (1). Ponieważ jest prawdziwe dla O, więc z (2) wynika, że musi być prawdziwe dla liczby 1. Ponieważ jest prawdziwe dla 1, znowu na podstawie (2), musi być prawdziwe dla liczby 2 i tak dalej. Indukcja matematyczna jest sposobem na zastąpienie zwrotu "i tak dalej" logicznie spójnym argumentem.
Zasada indukcji służy do dowodzenia faktów prawdziwych dla wszystkich liczb naturalnych. Przez indukcję można na przykład udowodnić następujące twierdzenie o sumie szeregu arytmetycznego dla wszystkich liczb naturalnych n:

(3.1) Sigma(#i=0;^n)[i] = [n(n+1)]/2

Najpierw musimy wykazać, że twierdzenie jest prawdziwe dla n = 0. Tę część
nazywamy podstawą indukcji. Dla n = 0 wzór przybiera postać Sigma(#i=0;^0)[i]=[0(0+1)]/2, więc obie strony są równe 0. Teraz musimy wykazać, że jeżeli twierdzenie zachodzi dla n>=, a więc Sigma(#i=0;^n)[i]=[n(n+1)]/2, to musi być również prawdziwe dla n+1, czyli Sigma(#i=0;^n+1)[i]=[(n+1)(n+2)]/2.
Zakładamy, że wzór jest spełniony dla n. Założenie to zwane jest założeniem indukcyjnym. Aby udowodnić, że
Sigma(#i=0;^n+1)[i]={(n+1)(n+2)]/2 zaczynamy od przekształcenia lewej strony. Rozbijamy sumę na dwie części: Sigma(#i=0;^n+1[i]={Sigma(#i+0;^n)[i]} + (n+1).
Pierwszy składnik tej sumy jest równy sumie występującej w założeniu indukcyjnym,
a więc mamy Sigma(#i=0;^n+1)[i]=[n(n+1)]/(2) + (n+1). Możemy na koniec uprościć prawą stronę wzoru, otrzymując Sigma(#i=0;^n+1)[i] = [(n+1)(n+2)]/2, co mieliśmy wykazać. Stosując indukcję matematyczną, udowodniliśmy prawdziwość wzoru dla wszystkich liczb naturalnych n.
Zasadę indukcji matematycznej można w naturalny sposób wykorzystać do dowodu, że jakieś zdanie jest niezmiennikiem pętli. Jeżeli (1) zdanie jest prawdziwe po


53

zerowej liczbie przebiegów pętli, to znaczy zanim pętla zostanie wykonana, ale po dokonaniu całej inicjacji, oraz (2) z prawdziwości zdania po n przebiegach wynika jego prawdziwość po n+ l przebiegach, jeśli wystąpiło n+ 1 przebiegów, to na mocy zasady indukcji zdanie musi być prawdziwe po każdym przebiegu, włącznie z tym kończącym pętlę. W celu udowodnienia, że dane stwierdzenie jest niezmiennikiem pętli, musimy wykazać, że:
=> Stwierdzenie jest prawdziwe przed pierwszym wykonaniem pętli, ale po dokonaniu całej inicjacji; wynika ono z warunku wstępnego pętli.
=> Jeśli założymy, że stwierdzenie jest prawdziwe przed jakimś przebiegiem pętli i że pętla zostanie wykonana ponownie, a więc warunek pętli jest spełniony, to stwierdzenie będzie nadal prawdziwe po kolejnym wykonaniu wnętrza pętli.
Jeżeli spełnione są obydwa powyższe warunki, to stwierdzenie jest niezmiennikiem pętli i będzie prawdziwe po jej zakończeniu. Niezmiennik i fakt, że pętla się zakończyła, kiedy warunek pętli stał się fałszywy, powinny dowodzić, że pętla wykonuje to, co powinna, a więc implikować jej warunek końcowy.
Powróćmy teraz do naszej prostej pętli powodującej wypisanie tekstu i udowodnijmy, że stwierdzenie, o którym twierdziliśmy, iż jest jej niezmiennikiem, jest nim rzeczywiście.
1. Zanim pętla zostanie wykonana, i=0, a zdanie nie zostało ani razu wypisane. Zatem zdanie zostało wypisane i razy, a i<= 13.
2. Załóżmy, że stwierdzenie jest prawdziwe i pętla będzie wykonana ponownie, a więc zachodzi warunek pętli i <=12. Przyjrzyjmy się, co się dzieje podczas kolejnego wykonania pętli. Ponieważ zdanie zostało wypisane i razy przed tym przebiegiem, a teraz jest wypisywane jeszcze raz, po czym i jest zwiększane o 1, w dalszym ciągu prawdą jest, że zdanie zostało wypisane i razy. Ponieważ pętla była wykonywana, musiało być i<=12. Wartość i została zwiększona o 1, więc teraz i<=13. Stąd stwierdzenie pozostaje prawdziwe po kolejnym przebiegu pętli.
Stwierdzenie jest zatem niezmiennikiem pętli i, co już widzieliśmy, fakt, że jest ono prawdziwe, kiedy pętla się kończy, oraz fakt, że po zakończeniu pętli i>12, dowodzą, że wykonanie pętli spowoduje wypisanie zdania dokładnie 13 razy.
Jako drugi przykład niezmiennika pętli rozważmy następującą funkcję:

int what (int a, int b)
/* Warunek wstępny: b >= 0 . */
{

int m;

m = 0;
while (l <= b) {
m = m + a;
b = b - 1
}
retrun m;
}






54

Pytanie: czym jest wartość m zwracana przez funkcję? W ogólności, kiedy piszemy kod programu, powinniśmy wiedzieć, co on robi. Ten przykład pokazuje, w jaki sposób niezmiennik pętli dowodzi, że program oblicza poprawny wynik. Aby uzyskać wskazówkę, co powinno być niezmiennikiem, spróbujemy wykonywać powyższy program ręcznie. Ponieważ jednak nie znamy wartości zmiennych a i b, musimy wykonywać instrukcje podstawienia symbolicznie, z użyciem aa i b() jako reprezentacji wartości początkowych odpowiednio dla a i b. (Będziemy stosowali tę konwencję w dalszym ciągu książki).
Na rysunku 3.1 widać wartości zmiennych przed rozpoczęciem wykonywania się pętli i po każdym z pierwszych czterech jej przebiegów.
a; b; m;
a#0; b#0; 0;
a#0; b#0-1; a#0;
a#0; b#0-2; 2*a#0;
a#0; b#0-3; 3*a#0;
a#0; b#0-4; 4*a#0;

Rys. 3.1. Wartości zmiennych a, b i m po czterech przebiegach pętli

Jak łatwo zauważyć, wartość zmiennej a jest stała, natomiast wartości b i m zmieniają się za każdym razem, przy czym zachodzi między nimi związek. Dla pewnego i mamy b = b#0-i oraz m = i*a#0, czyli po wyznaczeniu / oraz podstawieniu otrzymamy m=(b#0-b)*a#0. To stanowi jedną część niezmiennika. Druga jest wspólna dla wszystkich pętli tego typu i odnosi się do ograniczenia na zmienną sterującą pętli. W naszym przypadku najmniejszą wartością, jaką może przyjmować b, jest O, kiedy to pętla się kończy. Tak więc twierdzimy, że pełnym niezmiennikiem jest:

(3.2) a=a#0, m=(b#0-b)*a#0 i 0<=b

Udowodnimy przez indukcję, że to zdanie faktycznie jest niezmiennikiem.

=>Przed wykonaniem pętli a = a#0 i b = b#0 z definicji, a m = 0 w wyniku inicjacji.
Zatem m=(b#0-b)*a#0, bo O = (b#0 - b(#0) * a#0. Warunek wstępny procedury mówi, że b>=0, więc druga część zdania jest również prawdziwa.
=>Jeśli stwierdzenie jest prawdziwe przed wykonaniem wnętrza pętli, a pętla jest
wykonywana ponownie, to a = a#0, m=(b#0-b)*a#0 i 1 <= b. Jest to warunek wstępny dla wnętrza pętli m = m + a; b = b-1;. Musimy wykazać, że dowodzony niezmiennik jest warunkiem końcowym dla wnętrza pętli. Podstawiając wtedy wartości wyrażeń w miejsce zmiennych (możemy wykonać oba podstawienia jednocześnie, ponieważ są niezależne), otrzymujemy m + a = (b#0-(b- 1))*a#0 i O <=b - 1. Po stosownych algebraicznych uproszczeniach z wykorzystaniem faktu, że a = a#0, wzory te uzyskują postać m=(b#0-b)*a#0 i 1<=b, co stanowi część warunku wstępnego. Zatem niezmiennik zostaje odtworzony przez instrukcje wnętrza pętli.
Kiedy pętla zakończy działanie, oprócz tego, że znamy niezmiennik, wiemy też, że b<1 (zaprzeczenie warunku pętli). Ponieważ 0<=b, a b jest liczbą całkowitą, to b = 0. Wstawienie tego do drugiej części niezmiennika oznacza, że m = a#0*b, czyli że m, wartość zwracana przez funkcję, jest iloczynem parametrów wejściowych a i b. To właśnie wylicza nasza funkcja, chociaż są oczywiście prostsze sposoby wykonania tego obliczenia.-


55

3.3.2. Najczęstsze niezmienniki pętli
Proste pętle mają zazwyczaj proste niezmienniki. Pętle dzielimy na trzy kategorie: pętle z wartownikiem, pętle z licznikiem i pętle ogólne. Pętla z wartownikiem czyta i przetwarza dane aż do napotkania szczególnego, niedozwolonego elementu. Wartownik to wartość powodująca zakończenie działania pętli. Nie jest ona przetwarzana, a pętla zostaje przerwana. Pętla z wartownikiem wymaga wczytania danej przed pierwszym wykonaniem testu. Tę operację będziemy nazywali odczytem początkowym. Pseudokod pętli z wartownikiem może wyglądać następująco:

wczytaj daną
while dana nie jest wartownikiem {
przetwórz daną
wczytaj daną
}
Niezmiennik pętli z wartownikiem musi powiązać dane wczytane i przetworzone. W szczególności, wszystkie wczytane wartości zostały przetworzone, z wyjątkiem ostatniej, która być może jest wartownikiem, lecz nie została jeszcze sprawdzona, więc nie może być przetwarzana. Ponieważ pętla zatrzymuje się, kiedy wczytany został wartownik, jedynie ostatnia z wejściowych wartości może być wartownikiem lub, innymi słowy, żadna z wczytanych wartości, prócz być może ostatniej, nie jest wartownikiem. Poniższe dwa stwierdzenia stanowią niezmiennik pętli z wartownikiem:

Wszystkie wartości wejściowe, oprócz ostatniej, zostały przetworzone. Żadna z wartości wejściowych, oprócz być może ostatniej, nie jest wartownikiem.



56

Możemy z łatwością dowieść, że jest to niezmiennik dla ogólnej postaci pętli z wartownikiem:
1. Przed wykonaniem pętli została wczytana tylko jedna wartość. Ponieważ nie ma wczytanych wartości, oprócz ostatniej, każde zdanie na ich temat jest prawdziwe. W szczególności prawdziwa jest pierwsza część stwierdzenia: wszystkie zostały przetworzone. Analogicznie, żadna wartość nie została wczytana (oprócz ostatniej), więc żadna nie mogła być wartownikiem.
2. Zakładamy, że stwierdzenie jest prawdziwe i że pętla jest wykonywana kolejny raz. Oznacza to, że ostatnia wartość wejściowa nie jest wartownikiem. Przetwarzamy tę wartość i wczytujemy kolejną. Nadal jest prawdą, że wszystkie wartości wejściowe, oprócz ostatniej, zostały przetworzone. Ponieważ żadna wartość, prócz być może ostatnich dwóch, nie może być wartownikiem, a właśnie bezpośrednio sprawdziliśmy, że przedostatnia wejściowa wartość nim nie jest, więc żadna wczytana wartość, oprócz być może ostatniej, nie jest wartownikiem.
A zatem stwierdzenie jest niezmiennikiem pętli. Kiedy pętla się kończy, wiemy dodatkowo, że ostatnia wczytana wartość jest wartownikiem. To wraz z niezmiennikiem implikuje, że wszystkie wczytane wartości, oprócz ostatniej, zostały przetworzone i że jedynie ostatnia wartość jest wartownikiem - dokładnie to, czego się spodziewamy po zakończeniu działania pętli z wartownikiem.
Kiedy umieszczamy specjalizowaną pętlę z wartownikiem w programie, możemy także wyspecjalizować niezmiennik. Jeśli na przykład mamy napisać pętlę, która wczytuje ciąg liczb i sumuje je, zatrzymując się na liczbie ujemnej i nie uwzględniając jej w sumie, kod może wyglądać tak:

int n, s;

s = 0;
scanf ( "%d" , &n) ;
while (O <= n) {
s += n;
scanf ( "%d" ,&n) ;
}

Niezmiennikiem tej pętli z wartownikiem jest to, że s jest sumą wszystkich wczytanych liczb z wyjątkiem ostatniej (tzn. wszystkie wczytane wartości poza ostatnią zostały dodane do s) i że wszystkie dotychczas wczytane liczby, z wyjątkiem być może ostatniej, są nieujemne (żadna z wczytanych wartości, oprócz być może ostatniej, nie jest wartownikiem). Niezmiennik ten oraz fakt, że pętla się kończy, kiedy n < O, dowodzą jej poprawności.
Pętle z licznikiem stosuje się w sytuacjach, gdy zawczasu wiadomo, ile razy pętla będzie wykonywana; licznika używamy do kontroli liczby przebiegów pętli. Najczęściej do implementacji pętli z licznikiem wykorzystuje się instrukcję for, chociaż można użyć instrukcji while, aby wyraźnie oddzielić inicjację od testu

57

i treści pętli. Poniższe przykłady pętli z licznikiem demonstrują niezmienniki z użyciem while, chociaż wszystkie nasze komentarze łatwo zaadaptować do wersji z for.
Ogólna postać pętli z licznikiem, w której licznik i zmienia się od a do b, wygląda następująco:

i = a;
while (i <= b) {
przetwórz i-ty element
i++;
}
Ta postać pętli powinna wyglądać znajomo, ponieważ została użyta w przykładzie "Witaj świecie". Podobnie jak w tamtym przykładzie, niezmiennik pętli dzieli się na dwie części. Pierwszą jest to, że elementy od a do i - 1 zostały już przetworzone. Naszym pierwszym kandydatem na drugą część, ograniczenie dotyczące i, jest i <=b+1. Spróbujmy udowodnić ten niezmiennik. Tym razem zaczniemy od drugiej części dowodu.
Przypuśćmy, że niezmiennik jest prawdziwy i że pętla będzie wykonana ponownie. Z niezmiennika wynika, że zostały przetworzone elementy od a do i - 1 . W pętli przetwarzany jest następnie element i-ty, więc teraz są przetworzone elementy od a do i. Zaraz potem i jest zwiększane, więc znów mamy przetworzone elementy od a do i - 1 . Jeśli idzie o drugą część niezmiennika, to ponieważ pętla jest wykonywana kolejny raz, musi być i<=b. Zmienna i jest powiększana o l, więc nadal musi być prawdą, że i <= b + 1 .
Na razie wszystko jest w porządku, ale co z prawdziwością niezmiennika na samym początku? Przed wykonaniem pętli i = a, więc nie ma żadnych elementów w przedziale od a do i - 1 . Dlatego każde dotyczące ich stwierdzenie, z pierwszą częścią niezmiennika włącznie, jest prawdziwe. Druga część niezmiennika mówi, że i<=b+l. Ponieważ i = a, oznacza to, że a<=b+l. Nie ma żadnego powodu, żeby to miało być prawdą, bo nie wiemy nic o wartościach a i b nadanych przed wykonaniem tego fragmentu kodu.
Nasza pierwsza próba sformułowania niezmiennika pętli z licznikiem nie powiodła się z prostego powodu. Jeśli początkowo a>b+1, to pętla nie zostanie ani razu wykonana i wartość zmiennej i pozostanie równa a. Dlatego i w tym przypadku może być większe niż b+1.
Niezmiennik pętli powinien uwzględniać taką możliwość. Pełny niezmiennik pętli z licznikiem jest taki:

Elementy od a do i- 1 zostały przetworzone. Zachodzi a<=i. Jeżeli a<=b, to i<=b+1l. W przeciwnym razie i = a.
O pierwszym stwierdzeniu dowiedliśmy już, że jest niezmiennikiem. To, iż drugie stwierdzenie jest niezmiennikiem, wynika z faktu, że początkową wartością i jest a, natomiast wewnątrz pętli jedynie ją zwiększamy. Trzecie stwierdzenie również jest

58

początkowo prawdziwe, ponieważ i otrzymuje wartość a, i pozostaje prawdą, bo warunek pętli uniemożliwia zwiększenie i ponad b + 1; jeśli pętla jest wykonywana, to i<=b, więc po zwiększeniu wartości zmiennej i nadal nie przekracza ona b+1. Czwarte stwierdzenie jest początkowo prawdziwe i jeśli a>b, to i >=a >b, więc pętla nie będzie wykonana.
Zatem, jeśli a<=b, to gdy pętla się kończy i=b+1. Oznacza to, że elementy od a do b zostały przetworzone. Z drugiej strony, jeśli a>b, żaden element nie został przetworzony. W obu przypadkach program przetworzył elementy od a do b. Ich zbiór jest pusty, jeśli a>b. Jest to dokładnie to, co spodziewaliśmy się otrzymać.
Jeżeli upewniliśmy się zawczasu, że a <= b, przez umieszczenie tego w warunku wstępnym funkcji o parametrach a i b albo przez porównanie wartości a i b, to możemy uprościć niezmiennik, usuwając przesłankę z trzeciego warunku i likwidując czwarty. Jest to częściej stosowana postać niezmiennika.
Rozważmy fragment kodu służący do dodawania liczb całkowitych od m do n. Tutaj w pętli z licznikiem będziemy korzystać z instrukcji for.

/ * m <= n * /
s = 0;
for (i=m; i <= n; i++)
s+= i ;
/* s jest sumą liczb od m do n */

Niezmiennikiem pętli jest to, że s jest sumą liczb od m do i - l oraz że m <= i <= n + 1. Ponieważ jest to szczególny przypadek ogólnego niezmiennika dla pętli z licznikiem, jego poprawność jest już dowiedziona. Zatem kiedy pętla się kończy,
i = n + 1, a s jest sumą liczb od m do n. Jeżeli odrzucimy założenie, że m <= n, nadal możemy wnioskować, że s jest sumą liczb od m do n, ponieważ suma ta wynosi O, gdy założenie nie jest spełnione.
Określenie pętle ogólne obejmuje wszystkie pętle, które nie są ani pętlami z wartownikiem, ani pętlami z licznikiem. Ponieważ nie ma żadnej określonej postaci pętli ogólnej, poza tym że zwykle jest implementowana z użyciem instrukcji while, nie ma dla niej także ogólnej postaci niezmiennika.
3.3.3. Przetwarzanie tablic
Niezmienniki stosuje się także w pętlach przetwarzających tablice. W tym wypadku jedna ze zmiennych jest zazwyczaj wskaźnikiem lub indeksem w tablicy. Niezmiennik zwykle opisuje pewne własności elementów na lewo lub na prawo od indeksu czy wskaźnika (elementów, które zostały już przetworzone). Jako przykład rozpatrzmy implementację wyszukiwania sekwencyjnego:

/* Szukanie w tablicy a[0]. . a[n-1] elementu równego x. */
/* Warunek wstępny: 1 <= n. */
for (ptr=a; ptr/* Warunek końcowy: Jeżeli ptr
59

Niezmiennik dotyczy elementów tablicy a zawartych między a[0] a elementem wskazywanym przez ptr, ale wyłączając ten ostatni. Elementy te zostały sprawdzone i okazało się, że są różne od x. Konkretnie, niezmiennikiem tej pętli jest:

Wartość x nie występuje w tablicy od a[0] do * (ptr-1). Oprócz tego a <= ptr<= a + n.

Niezmiennika wraz z warunkiem pętli można użyć do wykazania, że pętla nie przekroczy zakresu tablicy. W tym wypadku niezmiennik mówi, że a <= ptr, natomiast warunek pętli zapewnia, że ptr < a + n. Zatem powyższa pętla na pewno nigdy nie przekroczy zakresu tablicy.
Niezmienniki pętli oraz specyfikacje pozostałych kroków stosuje się do wykazania, że całkowita specyfikacja programu lub funkcji jest częściowo poprawna: program robi to co powinien, jeśli się zatrzymuje. W dalszej części rozdziału zajmiemy się problemem dowodzenia, że program się zatrzyma.
3.4. Problem stopu
Aby udowodnić, że program się zatrzyma, musimy wykazać, że zakończą działanie wszystkie pętle programu i wszystkie wywołania funkcji rekurencyjnych. (Funkcje rekurencyjne omawiamy w rozdziale 7). Dla pętli z wartownikiem wymaga to umieszczenia w warunku wstępnym tego, że dane wejściowe zawierają wartownika. Dla pozostałych pętli standardową metodą dowodzenia, że pętla się zakończy, jest znalezienie pewnej całkowitoliczbowej wielkości, która w każdym przebiegu pętli się zmniejsza (lub powiększa) i jest ograniczona z dołu (z góry) przez jakąś wartość. Ponieważ żadna całkowitoliczbowa wielkość ograniczona z dołu nie może się zmniejszać w nieskończoność, pętla musi się prędzej czy później zakończyć.
Dla pętli z licznikiem łatwo znaleźć taką wielkość. Rozważmy następującą pętlę:

/* Warunek wstępny: a <= b. */
i = a;
while (i <= b) {
przetwórz i-ty element
i++;
}/* Warunek końcowy: Elementy od a do b zostały przetworzone. */

Wielkość b - i maleje w każdym przebiegu pętli, gdyż i rośnie, a b się nie zmienia. Ponieważ niezmiennik tej pętli zawiera fakt, że i <= b + 1, wielkość b - i jest ograniczona z dołu przez -ł. Zatem pętla musi się zakończyć.

60

3.5. Przykład: wyszukiwanie binarne
Rozważmy bardziej skomplikowany przykład procedury wyszukiwania binarnego. Wyszukiwanie binarne można zastosować, kiedy przeszukiwana tablica jest uporządkowana. Zamiast zaczynać od pierwszego elementu i przeglądać tablicę aż do znalezienia klucza lub dotarcia do jej końca, rozpoczniemy od środkowego elementu tablicy i porównamy go z szukanym kluczem. Jeżeli jest mu równy, to poszukiwanie zostało zakończone. Jeżeli jest on większy niż klucz, to możemy odrzucić dolną połowę tablicy i ograniczyć nasze poszukiwania do elementów powyżej środka. Jeśli natomiast środkowy element jest mniejszy od klucza, to odrzucamy górną połowę i kontynuujemy poszukiwanie jedynie w dolnej połowie.
Zaimplementujemy tę procedurę, przechowując dwa wskaźniki, Iow i high, które będą wyznaczać zakres bieżącego obszaru poszukiwań. Idea polega na tym, że jeśli klucz ma się znajdować w tablicy, to musi mieścić się między elementami wskazywanymi przez Iow i high. Ściślej mówiąc, wszystkie elementy poprzedzające Iow są mniejsze niż klucz, a wszystkie następujące po high są od niego większe, więc mogą być pominięte w dalszym wyszukiwaniu. Stanowi to główną część niezmiennika.
Rysunek 3.2 zawiera kod wyszukiwania binarnego. W tym przykładzie, jeżeli warunek wstępny pewnego kroku jest taki sam, jak warunek końcowy kroku poprzedniego, nie powtarzamy komentarza, a NP oznacza niezmiennik pętli, który zostanie skonstruowany później.
Funkcja comparedbkey (key1, key2) porównuje klucz key1 z key2 i zwraca liczbę ujemną, jeśli key1 < key2, O jeśli keyl = key2, a liczbę dodatnią, jeśli key1l > key2.
Niezmiennik pętli musi uwzględniać wszystkie zmienne występujące w pętli, z wyjątkiem używanych przez nią jedynie wewnętrznie. Znaczenie zmiennej found jest oczywiste. Jeżeli found jest równe 1, to klucz został znaleziony pod indeksem mid. Ostatnia część niezmiennika opisuje związek między zmiennymi Iow a high. Mogłoby się zdawać, że low < high jest niezmiennikiem, ale pętla może się zakończyć, gdy ten warunek jest fałszywy. Zmienna Iow może być większa niż high, jednak nie przekroczy high + 1. Całkowity niezmiennik dla naszej pętli wyszukiwania binarnego wygląda następująco:
1. Klucze w tablicy od db[0] do db[numRecs-1] są uporządkowane.
2. Wszystkie klucze od db[0].key do db[low-l] .key są mniejsze niż key.
3. Wszystkie klucze od db[high+l].key do db[numRecs-1] .key są większe niż key.
4. Jeśli found = l, to db[mid] .key = key.
5. low <= high + 1.
Aby sprawdzić, że niezmiennik jest prawdziwy przed wykonaniem pętli, musimy wykazać, że wynika on z warunku wstępnego po dokonaniu inicjacji. Inicjacja to

61

kilka instrukcji przypisania. Po wstawieniu wartości początkowych (0 dla Iow, numRecs-1 dla high i 0 dla f ound) w miejsce zmiennych w niezmienniku otrzymujemy następujące stwierdzenia:
1. Klucze w tablicy od db[0] do db[numRecs-1] są uporządkowane.
2. Wszystkie klucze od db[0] .key do db[-l] .key są mniejsze niż key.
3. Wszystkie klucze od db[numRecs] .key do db[numRecs-l].key są większe niż key.
4. Jeśli 0 = 1, to db[mid]. key = key.
5. 0 <= numRecs.

/* Warunek wstępny: Klucze w tablicy db[0]. . db[numRecs-1] są uporządkowane. numRecs >= 0. */
int low=0,high=numRecs-1,found=0,mid,cmp;
/* Warunek wstępny: low==0 && high==numRecs-l && found==0 */

/* NP */
while(!found && low<=high) {
/* NP && low <= high */
mid=(low+high)/2;
/* NP && low <= mid <= high */
cmp=comparedbkey(key, dbfmid].key) ;
/* NP && low <= mid <= high && (cmp < 0 wtw key jest mniejszy niż db[mid].key, cmp == 0 wtw key jest równy db[mid].key,
cmp > 0 wtw key jest większy niż db[[mid]. key) . Fragment dotyczący wartości zmiennej cmp nazwiemy stwierdzeniem C. */ if(cmp<0)
/* NP && low <= mid <= high && C && cmp < 0 */
high^mid-1;
/* NP */ else i f(cmp>0)
/* NP && low <= mid <= high && C && cmp > 0 */
low=mid+l;
/* NP */ else /* cmp==0 */
/* NP && low <= mid <= high && C && cmp == 0 */
found=1;
/* NP */
}
Warunek końcowy: NP && (f ound || low > high) */
Warunek końcowy: jeśli f ound == 1, to db[mid]. key jest równe key oraz low <= mid <= high. Jeśli found == 0 , to wartości db[0]. key do db[low-1]. key są mniejsze niż key oraz wartości db[low] .key do db[numRecs-1] .key są większe niż key. */

Rys. 3.2. Przykład wyszukiwania binarnego

62

Pierwsze stwierdzenie nie ulega zmianie. Kolejne dwa są prawdziwe, ponieważ odpowiednie zbiory są puste. Stwierdzenie czwarte jest spełnione w próżni( "Jeśli istnieje największa liczba naturalna, to jest ona równa 100." jest zdaniem prawdziwym. Ponieważ największa liczba naturalna nie istnieje, założenie w tym zdaniu jest fałszywe. Każda implikacja o fałszywym poprzedniku jest prawdziwa, niezależnie od następnika. Tego typu stwierdzenie nazywamy spełnionym w próżni.), a piąte jest częścią warunku wstępnego.
Teraz musimy wykazać, że jeśli niezmiennik jest spełniony, a pętla jest wykonywana ponownie, to niezmiennik pozostaje prawdziwy po kolejnym przebiegu pętli. Wnętrze pętli składa się z trzech instrukcji: dwóch przypisań i instrukcji if. Ponieważ warunki wstępne dla ostatnich dwóch instrukcji są takie same, jak warunki końcowe instrukcji je poprzedzających, więc jeśli każda z tych trzech instrukcji jest poprawna, to całe wnętrze pętli jest poprawne. Poprawności pierwszych dwóch instrukcji przypisania dowodzi się przez podstawienie i przywołanie definicji funkcji comparedbkey. Aby wykazać, że instrukcja if jest poprawna, trzeba udowodnić, że wszystkie trzy testy wartości cmp są prawidłowe. Rozważmy pierwszy test, gdy cmp < 0. Musimy uzasadnić, że instrukcja przypisania high = mid - 1; przywraca niezmiennik pętli. Wstawienie wartości mid - l w miejsce zmiennej high w warunku końcowym NP daje co następuje:
1. Klucze w tablicy od db[0] do db[numRecs-1] są uporządkowane.
2. Wszystkie klucze od db[0] .key do db[low-1] .key są mniejsze niż key.
3. Wszystkie klucze od db[mid].key do db[numRecs-1] .key są większe niż key.
4. Jeśli found = 1, to db[mid] .key = key.
5. low <= mid.
Stwierdzenia pierwsze, drugie i czwarte nie zmieniają się, a więc wynikają z NP, będącego częścią warunku wstępnego tego kroku. Warunek wstępny obejmuje także fakt, że cmp < O, co na mocy stwierdzenia C oznacza, że key jest mniejsze niż db[mid].key. Ponieważ tablica jest uporządkowana, wszystkie klucze od mid do numRecs - 1 są większe niż key, a zatem spełnione jest stwierdzenie 3. Stwierdzenie 5 jest prawdziwe, bo warunek wstępny mówi, że low <= mid <= high. Zatem pierwszy przypadek jest poprawny.
Drugi test, gdy cmp > O, jest podobny do poprzedniego i nie będzie omawiany. Aby wykazać poprawność ostatniego testu, cmp == O, zauważmy, że jedynym stwierdzeniem, które zmienia się po podstawieniu l w miejsce found jest stwierdzenie 4. Ponieważ cmp == O, na mocy stwierdzenia C key == db[mid]. key, a więc wszystkie stwierdzenia w tym wariancie pozostają prawdziwe.
We wszystkich trzech testach niezmiennik pętli wynika z warunku wstępnego oraz wyniku testu. Dlatego instrukcja if jest poprawna, a niezmiennik odtworzony przez wnętrze pętli.

63

Kiedy pętla się kończy, dzieje się tak, gdyż zmienna found przyjmuje wartość logiczną prawda (1) lub Iow > high. W pierwszym przypadku stwierdzenie 4 z niezmiennika informuje, że klucz został znaleziony i znajduje się pod indeksem mi d. Jeśli f ound ma wartość fałsz (0), to pętla musiała się zakończyć, bo Iow > high. Na mocy stwierdzenia 2 klucza nie ma między db[[0].key a db[low-1] .key, a ze stwierdzenia 3 wynika, że nie ma go również między db[high+1] .key a db[numRecs-1]. key. Ponieważ te dwa obszary nakładają się i pokrywają łącznie całą tablicę db, więc jeśli f ound jest fałszem, wartości key nie ma w tablicy. Zatem kod dla wyszukiwania binarnego jest poprawny.
Niezmiennik mówi nam jednak nieco więcej o powyższym kodzie. Jeżeli klucza nie znaleziono, to niewykluczone, że następnym krokiem programu będzie wstawienie go do tablicy. Ponieważ tablica ma pozostać uporządkowana, musimy określić, gdzie powinien on się znaleźć. Nasza procedura binarnego wyszukiwania dokładnie informuje, gdzie umieścić klucz obecnie nie będący w tablicy, a do wskazania tego miejsca możemy użyć niezmiennika.
Konkretnie, jeżeli klucz nie został znaleziony, to pętla się zakończyła, gdyż Iow > high. Ponieważ stwierdzenie 5 niezmiennika jest prawdziwe, a Iow i high są liczbami całkowitymi, to Iow = high + 1. Wstawienie Iow w miejsce high + 1 w stwierdzeniu 3 dowodzi, że wszystkie klucze od db[low].key do db[numRecs-1] .key są większe niż key. Ponieważ z kolei stwierdzenie 2 mówi, iż wszystkie klucze od db[0].key do db[low-1]. key są mniejsze niż key, jest oczywiste, że należy wszystkie klucze, poczynając od Iow, przesunąć o jedną pozycję w prawo, a nowy klucz wstawić na pozycję Iow.
Aby dowieść, że wyszukiwanie binarne zawsze się kończy, musimy określić pewną całkowitoliczbową wielkość, która stale się zmniejsza aż do osiągnięcia swej wartości minimalnej. Procedura na pewno się w końcu zatrzyma, bo albo klucz zostanie znaleziony, co natychmiast zakończy pętlę, albo zabraknie elementów do przeszukiwania. Wymaganą wielkością mogłoby być high - low + 1, ale wartość tego wyrażenia nie zmniejsza się, jeśli w ostatnim przebiegu pętli klucz zostaje znaleziony, ponieważ wówczas Iow i high nie ulegają zmianie. Poprawnym rozwiązaniem jest połączenie tej wielkości ze zmienną found. Za wielkość stale malejącą w pętli weźmiemy (1 - found) * (high - low + 1). Wielkość ta jest ograniczona z dołu przez O, bo high - low + 1 >= O, a found <= 1 (łatwo uzasadnić, że to ostatnie spostrzeżenie jest prawdziwe jako część niezmiennika). Maleje ona w każdym przebiegu pętli, ponieważ albo zmniejsza się przedział między Iow a high, albo wartość f ound zmienia się z 0 na 1. Zatem procedura wyszukiwania binarnego musi się zakończyć.

3.6. Uwagi końcowe
Istnieje wiele innych elementów, które muszą być brane pod uwagę przy dowodzeniu poprawności programu. Weryfikacja programu powinna uwzględniać problem przepełnienia dla wartości całkowitoliczbowych, przepełnienia i niedomiaru dla liczb


64

zmiennopozycyjnych, sprawdzenie, czy nie są przekraczane zakresy tablic oraz czy pliki są otwierane i zamykane we właściwy sposób. Niemniej jednak sprawdzenie poprawności kodu, choćby na tym elementarnym poziomie, przyczynia się w dużym stopniu do usunięcia błędów, nawet przed wykonaniem programu. W dalszej części książki nie podajemy warunków wstępnych i końcowych dla każdego kroku, ale zamieszczamy je dla wszystkich funkcji, a także wypisujemy niezmienniki dla wszystkich nieoczywistych pętli.
3.7. Ćwiczenia

1. Udowodnij poprawność warunku końcowego dla następującego kodu:
/* x > 0 && y > 0 */ x = x * y; /* x > 0 */

2. Wstaw odpowiednie warunki wstępne i końcowe między poszczególne kroki w poniższym kodzie, a następnie udowodnij, że ostatni warunek końcowy jest spełniony. (Przypominamy, że x0 i y0 oznaczają początkowe wartości x i y).
/* */ t = x; x = y; y = t; / * x = y0 && y = x0 */

3. Udowodnij poprawność warunku końcowego dla następującego kodu:
/* */
if (x >= 0)
y = y + x; else
y = y - x ;
/* y = y0 + |x0 | */

4. Udowodnij poprawność warunku końcowego dla następującego kodu:
/* x >= 100 */
if (x>=y)
m = x; else
m = y; /* m >= 100 */

5. Podaj niezmiennik dla poniższej pętli i udowodnij jego poprawność:
/* 1 <=b */ i = 1; c = 1 ; while (i <= b) { c = c * a;


65

6. Napisz program, który wczytuje ciąg liczb dodatnich, zakończony przez -l, oblicza i wypisuje największą z wczytanych liczb dodatnich. Podaj niezmiennik dla pętli w Twoim programie, a następnie udowodnij, że jest on poprawny i że wynika z niego, iż program robi to co powinien.

7. Napisz program, który wczytuje ciąg 100 liczb dodatnich, oblicza i wypisuje największą z wczytanych liczb dodatnich. Podaj niezmiennik dla pętli w Twoim programie, a następnie udowodnij, że jest on poprawny i że wynika z niego, iż program robi to co powinien.

8. Udowodnij, że następująca pętla się kończy:
scan( " %d" , &a) ;
if (a > 0)
while (a > 100) a = a / 2 ;

9. Wykaż, że zdanie found <= l jest niezmiennikiem pętli w wyszukiwaniu binarnym.

10. Czy mid = Iow, kiedy algorytm wyszukiwania binarnego zatrzymuje się, nie znajdując klucza? Odpowiedź uzasadnij.

Bibliografia
[1] Alagić S., Arbib M.A.: Projektowanie programów poprawnych i dobrze zbudowanych.
Warszawa, WNT 1982. [2 J Apt K.R.: Ten Years of Hoare's Logic: A Survey. Association ofthe ACM Transactions on
Programming Languages and Systems, 1981, 3, s. 431-483.
[3] Boyer R.S., Moore J.S.: A Computational l^gic. New York, NY, Academic Press 1979. [4] Dijkstra E.W.: Umiejętność programowania. Warszawa, WNT 1985. [5] Hoare C.A.R.: Ań Axiomatic Basis for Computer Programming. Communications of ACM,
1969, 12, s. 576-583. [6] Manna Z.: Mathematical Theory of Computation. New York, NY, McGraw-Hill 1974.