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

!/01324

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:

6798;:=<>?@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

:

G798G: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

G3F

.

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

G3F

.

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

.