Matematyka Dyskretna
Andrzej Szepietowski
25 czerwca 2002 roku
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łowem
else
w 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, ˙ze
2
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´sci
5
,
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 ˛
a
writeln
. 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 ˛
a
if
.
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˛egi
5
.
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 ˛
a
readln
, z asercj ˛
a:
5 %$.AP
Punkt
na ko ´ncu programu, tu˙z przed instrukcj ˛
a
writeln
, z asercj ˛
a:
L
B
AP
Trzeci punkt kontrolny
jest wewn ˛
atrz p˛etli, tu˙z przed instrukcj ˛
a
x:=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, czy
2
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 naturalnej
5
. Przykład takiego programu przedstawiono w roz-
dziale 3.5. Je˙zeli program główny
oblicza dla warto´sci wej´sciowej
5
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
.