Matematyka Dyskretna
Andrzej Szepietowski
25 czerwca 2002 roku
Rozdział 1
Poprawno´s´c programów
Je˙zeli projektujemy algorytmy lub piszemy programy, to wa˙zne jest pytanie, czy nasz al- gorytm lub program jest poprawny, czy nie zawiera bł˛edów. Konkretniej, mo˙zemy spyta ´c, czy nasz program jest napisany zgodnie z regułami j˛ezyka programowania i czy liczy to, co chcemy.
1.1 Poprawno´ s´ c syntaktyczna
Je˙zeli program jest napisany zgodnie z regułami j˛ezyka programowania, to mówimy, ˙ze jest poprawny pod wzgl˛edem syntaktycznym, a wykroczenia przeciwko składni j˛ezyka nazywaj ˛a si˛e bł˛edami syntaktycznymi. Przykładami takich bł˛edów w j˛ezyku Pascal s ˛a:
u˙zycie zmiennej, która wcze´sniej nie została zadeklarowana, lub postawienie ´srednika przed słowemelsew instrukcji warunkowej.
Poprawno´s´c syntaktyczna nie jest wielkim problemem. J˛ezyki programowania maj ˛a bardzo ´scisłe reguły składni, okre´slaj ˛ace, jak budowa´c poprawne programy, i konstrukto- rzy tych j˛ezyków zadbali o to, aby mo˙zna było łatwo wykry ´c bł˛edy syntaktyczne. Istnie- j ˛a kompilatory, które automatycznie sprawdzaj ˛a poprawno´s´c syntaktyczn ˛a programów.
Kompilatory niektórych j˛ezyków s ˛a do´s´c skomplikowanymi programami i oprócz komu- nikatu o bł˛edzie daj ˛a tak˙ze wskazówki, jak bł ˛ad usun ˛a´c.
1.2 Poprawno´ s´ c semantyczna
Du˙zo powa˙zniejszym problemem jest poprawno´s´c semantyczna, czyli stwierdzenie, czy program lub algorytm liczy to, co powinien. Problem zaczyna si˛e ju˙z wówczas, gdy spy- tamy, co to znaczy „liczy to, co powinien”.
Zajmiemy si˛e teraz jednym z mo˙zliwych podej´s´c do problemu poprawno´sci. Program przekształca dane wej´sciowe w dane wyj´sciowe i dlatego mo˙zemy go traktowa´c jak funk- cj˛e ze zbioru danych wej´sciowych w zbiór danych wyj´sciowych. Na przykład dla algo- rytmu Euklidesa (porównaj rozdział o teorii liczb) danymi wej´sciowymi s ˛a pary liczb
3
4 Rozdział 1. Poprawno´s´c programów
naturalnych, a danymi wyj´sciowymi s ˛a pojedyncze liczby naturalne. W algorytmie sor- tuj ˛acym danymi wej´sciowymi i wyj´sciowymi s ˛a ci ˛agi liczb. ˙Zeby okre´sli´c „co program robi” definiuje si˛e warunki: jeden warunek mówi, jakie powinny by ´c dane wej´sciowe, a drugi warunek okre´sla, jakie powinny by´c dane wyj´sciowe.
Problem algorytmiczny mo˙zemy wi˛ec zdefiniowa´c przez podanie:
zbioru danych wej´sciowych , zbioru danych wyj´sciowych ,
predykatu (funkcji zdaniowej) , który okre´sla warunki pocz ˛atkowe; przyj- muje warto´s´c prawda, je˙zeli dane wej´sciowe s ˛a poprawnie zbudowane,
predykatu , który okre´sla relacj˛e pomi˛edzy danymi wyj´sciowymi i wej´sciowymi;
ma warto´s´c prawda, je˙zeli dane wyj´sciowe s ˛a prawidłow ˛a odpowiedzi ˛a
algorytmu na dane wej´sciowe . W przykładzie algorytmu Euklidesa:
dane wej´sciowe to pary liczb naturalnych
, dane wyj´sciowe to zbiór liczb naturalnych , warunek pocz ˛atkowy !#"%$&('*)+,"-$. ,
relacja !/ 01 324 okre´sla, ˙ze2 jest najwi˛ekszym wspólnym dzielnikiem liczb i . Zadanie algorytmiczne sortowania mo˙ze by´c zdefiniowane w nast˛epuj ˛acy sposób (dla prostoty zakładamy, ˙ze sortujemy ci ˛agi ró˙znowarto´sciowe):
i to zbiory wszystkich ci ˛agów długo´sci5 , warunek mówi, ˙ze ci ˛ag jest ró˙znowarto´sciowy:
6 798;:=<>?@A< BC>ED
F@1A
warunek G okre´sla, ˙ze ci ˛ag jest rosn ˛acy i zawiera dokładnie te same ele- menty co ci ˛ag :
G 798G:0< >< BH*:0<*@A<B />
1@ and 8;:=<><B4I;:6(>KJL.>NM :O=P
Takiego typu warunki nazywaj ˛a si˛e specyfikacj ˛a algorytmu lub programu. Jednym słowem, specyfikacja mówi nam, co program ma robi´c. Program działa poprawnie, je˙zeli dla ka˙zdych danych wej´sciowych , spełniaj ˛acych warunek wej´sciowy, daje wynik
, który spełnia warunek wyj´sciowy G 3F .
Zwykle dowód poprawno´sci programu rozbija si˛e na dwa poddowody. Osobno dowo- dzi si˛e poprawno´sci przy zało˙zeniu, ˙ze program zawsze si˛e zatrzyma, a osobno dowodzi si˛e, ˙ze program zatrzymuje si˛e dla ka˙zdych poprawnie zbudowanych danych wej´scio- wych.
1.3. Niezmienniki 5
Definicja 1.1 Program jest cz˛e´sciowo poprawny wzgl˛edem warunków i , gdy dla ka˙z- dych danych wej´sciowych spełniaj ˛acych zachodzi nast˛epuj ˛aca implikacja: je˙zeli program zatrzymuje si˛e na danych i daje wynik , to zachodzi warunek G 3F .
Program jest całkowicie poprawny, je˙zeli jest cz˛e´sciowo poprawny i ponadto zatrzy- muje si˛e dla ka˙zdych danych wej´sciowych spełniaj ˛acych warunek.
Jedn ˛a z metod dowodzenia cz˛e´sciowej poprawno´sci programu jest metoda niezmien- ników lub asercji indukcyjnych.
1.3 Niezmienniki
Metoda niezmienników polega na wyznaczeniu w programie kilku punktów kontrolnych i zwi ˛azaniu z tymi punktami asercji, czyli pewnych warunków. W´sród punktów kontrol- nych dwa s ˛a szczególne: jeden punkt zaraz na pocz ˛atku programu z asercj ˛a pocz ˛atkow ˛a i jeden punkt na ko ´ncu programu z asercj ˛a ko ´ncow ˛a. Asercja pocz ˛atkowa zwykle zawie- ra sformułowania obejmuj ˛ace warunki na dane pocz ˛atkowe . Asercja ko ´ncowa opisuje relacj˛e wi ˛a˙z ˛ac ˛a dane wej´sciowe z wyj´sciowymi. Po wyznaczeniu punktów i asercji dowodzimy, ˙ze ka˙zda asercja jest spełniona zawsze wtedy, gdy wykonanie programu doj- dzie do odpowiadaj ˛acego jej punktu kontrolnego. W ten sposób dowodzimy, ˙ze je˙zeli na pocz ˛atku był spełniony warunek pocz ˛atkowy i potem program dojdzie do punktu ko ´n- cowego, to b˛edzie spełniony warunek . Dowód poprawno´sci mo˙ze przebiega´c w ten sposób, ˙ze dla poszczególnych par punktów kontrolnych i (niekoniecznie ró˙znych) dowodzimy nast˛epuj ˛ac ˛a implikacj˛e: je˙zeli w punkcie spełniona jest asercja , a na- st˛epnie wykonanie programu przejdzie z punktu do , to w punkcie b˛edzie spełniona asercja .
Niektóre punkty kontrolne mog ˛a by´c w trakcie wykonywania programu osi ˛agane wie- lokrotnie (na przykład punkty znajduj ˛ace si˛e wewn ˛atrz p˛etli). Tak wi˛ec asercja powinna by´c spełniona za ka˙zdym odwiedzeniem punktu kontrolnego. Z tego powodu asercje te nazywamy niezmiennikami.
Sposób rozmieszczenia punktów kontrolnych i przypisania tym punktom asercji nie jest prosty i nie ma uniwersalnych reguł w tym wzgl˛edzie. Podobnie jak z dowodzeniem twierdze´n, sposób dowodu poprawno´sci programu jest oryginalnym pomysłem autora do- wodu. Istniej ˛a w tym wzgl˛edzie pewne reguły heurystyczne, niektóre nawet bardzo zło-
˙zone, ale nie ma uniwersalnych reguł, które pozwol ˛a udowodni ´c poprawno´s´c lub niepo- prawno´s´c ka˙zdego programu.
1.4 Liczniki
Aby udowodni´c, ˙ze algorytm zawsze si˛e zatrzyma, mo˙zemy u˙zy´c liczników. Najpierw, podobnie jak poprzednio, wyznaczamy punkty kontrolne i pewn ˛a zmienn ˛a, zwan ˛a licz- nikiem lub zbie˙znikiem, która mo˙ze przyjmowa´c tylko warto´sci całkowite nieujemne.
Nast˛epnie dowodzimy, ˙ze po ka˙zdym odwiedzeniu jakiego´s punktu kontrolnego warto´s´c licznika maleje.
6 Rozdział 1. Poprawno´s´c programów
Nie ma miejsca w tej ksi ˛a˙zce na rozwijanie teorii dowodzenia poprawno´sci progra- mu. Zajmiemy si˛e tylko dwoma przykładami. Pierwszy to algorytm Euklidesa, który był przedstawiony w rozdziale z teorii liczb i tam te˙z przedstawiono dowód jego poprawno´sci.
Teraz tylko sformułujemy go w j˛ezyku asercji.
1.5 Algorytm Euklidesa jeszcze raz
Oto jeszcze raz algorytm Euklidesa opisany w j˛ezyku Pascal:
var a,b,p,q:integer;
begin
readln(a,b);
{A}
p:=a;q:=b;
while p<>q do {C}
if p>q then p:=p-q else q:=q-p;
{B}
writeln(’NWD(’,a,’,’,b,’)=’,p) end.
W programie umie´scili´smy trzy punkty kontrolne. Punkt na pocz ˛atku, zaraz za instrukcj ˛a readln(a,b). Asercja zwi ˛azana z punktem orzeka, ˙ze i to dwie dodatnie liczby całkowite.
Punkt znajduje si˛e na ko ´ncu programu, tu˙z przed instrukcj ˛awriteln. Asercja zwi ˛azana z tym punktem orzeka, ˙ze zawiera najwi˛ekszy wspólny dzielnik liczb i.
Trzeci punkt kontrolny jest wewn ˛atrz p˛etli, tu˙z przed instrukcj ˛a warunkow ˛aif.
Asercja orzeka, ˙ze para liczb i ma taki sam najwi˛ekszy wspólny dzielnik co para
i .
Dowodzimy cztery implikacje:
je˙zeli wykonanie programu jest w punkcie i spełniona jest asercja , a nast˛ep- nie program przejdzie do punktu , to spełniona b˛edzie asercja ,
je˙zeli wykonanie programu jest w punkcie i spełniona jest asercja , a nast˛ep- nie program ponownie przejdzie do punktu , to spełniona b˛edzie asercja , je˙zeli wykonanie programu jest w punkcie i spełniona jest asercja , a nast˛ep- nie program przejdzie do punktu , to spełniona b˛edzie asercja ,
je˙zeli wykonanie programu jest w punkcie i spełniona jest asercja , a nast˛ep- nie program przejdzie do punktu , to spełniona b˛edzie asercja .
1.6. Pot˛egowanie 7
Naszkicujmy tylko dowód drugiej implikacji, pozostałe dowodzi si˛e podobnie. Załó˙z- my, ˙ze wykonanie programu znajduje si˛e w punkcie i ˙ze zmienne i maj ˛a wtedy warto´sci : i : . Je˙zeli w wyniku dalszego wykonania program ponownie dojdzie do punktu , to znaczy, ˙ze : D
: , bez straty ogólno´sci mo˙zemy zało˙zy´c, ˙ze : " : . Wtedy nowe warto´sci zmiennych i maj ˛a warto´sci
: : oraz
: . Z faktu,
˙ze warto´sci : i : spełniaj ˛a asercj˛e E : : , wynika, ˙ze para : i : ma taki sam naj- wi˛ekszy wspólny dzielnik jak para wej´sciowa i . W rozdziale o teorii liczb pokazano,
˙ze para ma taki sam zbiór wspólnych dzielników jak para : : . Tak wi˛ec tak˙ze para
ma taki sam najwi˛ekszy wspólny dzielnik jak para , wi˛ec spełnia asercj˛e . Aby pokaza´c, ˙ze program zatrzymuje si˛e dla ka˙zdych danych spełniaj ˛acych warunek
#" $ , wprowadzimy licznik dla punktu kontrolnego . Licznikiem tym jest warto´s´c
&
. Jest jasne, ˙ze warto´s´c licznika jest zawsze liczb ˛a całkowit ˛a nieujemn ˛a i ˙ze zmniejsza si˛e przy ka˙zdym ponownym odwiedzeniu punktu . Wykonanie programu nie mo˙ze wi˛ec trwa´c w niesko´nczono´s´c.
1.6 Pot˛egowanie
Drugim przykładem niech b˛edzie program na podnoszenie liczby dwa do pot˛egi5 . var n,x,y:integer;
begin
readln(n);
{A}
y:=1;
x:=n;
while x>0 do begin {C}
x:=x-1;
y:=y+y end;
{B}
writeln(y) end.
W tym programie te˙z s ˛a trzy punkty kontrolne. Punkt na pocz ˛atku, zaraz za instruk- cj ˛areadln, z asercj ˛a:
5 %$.AP
Punkt na ko ´ncu programu, tu˙z przed instrukcj ˛awriteln, z asercj ˛a:
L
B
AP
Trzeci punkt kontrolny jest wewn ˛atrz p˛etli, tu˙z przed instrukcj ˛ax:=x-1, z asercj ˛a:
B
=P
8 Rozdział 1. Poprawno´s´c programów
Dowód poprawno´sci programu polega teraz na dowodzie tych samych czterech impli- kacji, które znajduj ˛a si˛e w podrozdziale 10.5.
Aby udowodni´c, ˙ze program zawsze si˛e zatrzyma, wystarczy jako licznik przyj ˛a ´c zmienn ˛a , która przyjmuje warto´sci nieujemne i zmniejsza swoj ˛a warto´s´c przy ka˙zdym kolejnym odwiedzeniu punktu .
1.7 Czekery
W przypadku gdy udowodnimy, ˙ze jaki´s program działa poprawnie, wówczas mamy pew- no´s´c, ˙ze dla ka˙zdych danych wej´sciowych uzyskany wynik b˛edzie dobry. Inn ˛a metod ˛a sprawdzania, ˙ze program działa poprawnie, s ˛a czekery. Zamiast dowodzi ´c, ˙ze program zawsze zadziała dobrze, czekery sprawdzaj ˛a, czy zadziałał on dobrze w konkretnych przy- padkach. Do zadania algorytmicznego projektowane s ˛a dwa programy. Program główny , który rozwi ˛azuje zadanie, oraz program , zwany czekerem lub weryfikatorem, który po ka˙zdym zadziałaniu programu sprawdza, czy odpowied´z programu jest popraw- na. Zakłada si˛e przy tym, ˙ze działanie czekera jest du˙zo prostsze ni˙z działanie programu . W dodatku program mo˙ze by´c traktowany jak czarna skrzynka, gdzie nie mamy wgl ˛adu w to, jak program działa, tylko dostajemy ostateczne odpowiedzi. Przyjrzyjmy si˛e pomysłowi czekerów na przykładach.
We´zmy znowu algorytm Euklidesa, ale teraz wygodniej jest wzi ˛a ´c wersj˛e, gdzie pro- gram bierze par˛e liczb i i zwraca trzy liczby:2 ! A oraz i , takie ˙ze
. 0
2 . ˙Zeby sprawdzi´c, czy program dobrze obliczył dane wyj´sciowe, wystarczy sprawdzi´c, czy2 dzieli i, oraz czy
O-
2/P
Inny przykład to czeker dla programu obliczaj ˛acego zaokr ˛aglenie w gór˛e pierwiastka kwadratowego z liczby naturalnej5 . Przykład takiego programu przedstawiono w roz- dziale 3.5. Je˙zeli program główny oblicza dla warto´sci wej´sciowej5 warto´s´c wyj´sciow ˛a
, to zadanie czekera polega na sprawdzeniu dwóch rzeczy, czy
L5
oraz czy
JL5KP
1.8 Zadania
1. Udowodnij poprawno´s´c programu (przedstawionego w podrozdziale 6.6), który dla danych liczb , " $ oblicza
A oraz liczby całkowite , spełniaj ˛ace
równo´s´c /
A.
