FAKULTA MATEMATIKY, FYZIKY

A INFORMATIKY

UNIVERZITY KOMENSKÉHO

Katedra informatiky

Základy teórie programovania

Zbierka riešených príkladov

Ondrej Jombík

release 0.8.3 build 2004-05-18

Bratislava

2003, 2004

Vďaka zmene systému zo známkovacieho na kreditové, bolo možné zapísať
si Základy teórie programovania v troch po sebe idúcich školských
rokoch.

Treba mať na pamäti, že autori podieľajúci sa na tvorbe tohto

dokumentu, tento predmet aj trikrát zapísaný mali. Z toho vyplýva, že určite
nepatria k absolútnym odborníkom na danú problematiku. Tento dokument
si vytvorili len pre svoju osobnú potrebu ako užitočnú pomôcku pri štúdiu.

Dokument je len doplnkovým materiálom. V žiadnom prípade nemá slúžiť
ako náhrada za dobré skriptá alebo prednášku zo Základov teórie pro-
gramovania. Autori nenesú žiadnu zodpovednosť za prípadné chyby, prek-
lepy alebo nepresnosti, ale privítajú ich opravy či vylepšenia. Rozšírenie
dokumentu o ďalšie príklady a poznámky je taktiež vítané.

Osobitné poďakovanie patrí Ľubomírovi Hostovi za vytvorenie skvelého
pracovného a zostavovacieho rámca pre prácu so systémami LATEX a pdfTEX.

ii

Obsah

1

Programové schémy

2

1.1

Štandardné programové schémy . . . . . . . . . . . . . . . . .

2

1.2

Nerozhodnuteľnosť vlastností schém . . . . . . . . . . . . . . .

6

1.3

Porovnávanie tried programových schém . . . . . . . . . . . .

9

2

Správnosť programov

22

2.1

Metódy dokazovania správnosti . . . . . . . . . . . . . . . . .

22

2.2

Rozširovanie Hoareovských kalkulov . . . . . . . . . . . . . . .

33

3

Sémantika programov

37

Literatúra

39

1

Kapitola 1

Programové schémy

1.1

Štandardné programové schémy

Príklad 1 Máme program P1. Zistite, čo program počíta a napíšte jeho
schému.

P1 : begin [y1, y2] := [1, 1]

1 : if y2 ≥ x then goto end
2 : [y1, y2] := [y1 + 1, (y1 + 1)

2]

3 : goto 1

end [z] := [y1]

Riešenie 1 Po krátkej analýze je zrejmé, že program počíta d

√

xe (hornú

celú časť odmocniny x).

Schéma S, abstrakcia programu vzhľadom na riadiace štruktúry, vyzerá tak-
to:

S : begin [y1, y2] := [a1, a2]

1 : if p(y2, x) then goto end
2 : [y1, y2] := [f1(y1), f2(y1)]
3 : goto 1

end [z] := [y1]

Príklad 2 Napíšte interpretáciu I1 tak, aby sme pomocou nej a predchádza-
júcej schémy S dostali pôvodný program P1, tj. aby platilo P1 = (S, I1).

2

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

3

Riešenie 2 Interpretácia I1 = (D1, i1):

I1 : i1(p(y, x)) = y ≥ x

i1(f1(y)) = y + 1
i1(f2(y)) = (y + 1)

2

i1(a1) = 1
i1(a2) = 1

D1 = N

Príklad 3 Nájdite interpretáciu I2, ktorá spolu s predchádzajúcou schémou
S vytvorí program, ktorý bude počítať dlog2xe.

Riešenie 3 Interpretácia I2 = (D2, i2):

I2 : i2(p(y, x)) = y ≥ x

i2(f1(y)) = y + 1
i2(f2(y)) = 2

y+1

i2(a1) = 1
i2(a2) = 0

D2 = N

Pomocou príkladu sme si ukázali, že nad jednou schémou S môžu byť postavené
viaceré programy (S, I1), (S, I2) . . . (S, In) riešiace odlišné úlohy.

Príklad 4 Je daná programová schéma S.

S : begin [y1, y2] := [x, a]

1 : if p(y1) then goto end
2 : [y1, y2] := [f (y1), g(y1, y2)]
3 : goto 1

end [z] := [y2]

Nájdite interpretácie:

– I1 takú, že program (S, I1) bude počítať x! (faktoriál x)

– I2 takú, že program (S, I2) bude počítať

Px

i=1 i (suma od 1 po x)

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

4

Riešenie 4 Hľadané interpretácie sú zobrazené v nasledujúcich tabuľkách.

I1

N

a

1

p

y1 = 0

f

y1 − 1

g

y1y2

I2

N

a

0

p

y1 = 0

f

y1 − 1

g

y1 + y2

Príklad 5 Napíšte históriu výpočtu pre program P2 = (S, I2) s hodnotou
vstupnej premennej x = 7. Formálne sa ohodnotenie vstupných premenných
zapisuje ako v[x ← 7].

Riešenie 5 Je nutné si uvedomiť, že históriu výpočtu môžeme zapísať vzhľa-
dom na stavy výpočtu, ale taktiež vzhľadom na konfigurácie. V našom riešení
použijeme druhú možnosť, tj. históriu výpočtu vzhľadom na konfigurácie.

[1, 1]

begin

[1, 1]

1

[2, 4]

2

[2, 4]

3

[2, 4]

1

[3, 9]

2

[3, 9]

3

[3, 9]

1

[3]

end

Príklad 6 Zostrojte Herbrandové univerzum pre predchádzajúcu schému S.

Riešenie 6 Herbrandovo univerzum je množina reťazcov symbolov zostro-
jených zo vstupných premenných a funkčných symbolov.

Riešenie začneme tým, že zoberieme všetky vstupné premenné schémy (v na-
šom prípade vstupnú premennú x) a všetky použité konštanty (v našom
prípade a1 a a2).

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

5

”x”, ”a1”, ”a2”

Ďalej zoberieme funkcie f1 a f2 a aplikujeme na všetky dostupné termy, ktoré
doteraz reprezentujú konštanty a1, a2 a vstupná premenná x.

”f1(x)”, ”f1(a1)”, ”f1(a2)”

”f2(x)”, ”f2(a1)”, ”f2(a2)”

Týmto krokom sa nám teraz rozšírila množina termov, takže uvedeným spô-
sobom aplikovania funkcií f1 a f2 na termy pokračujeme ďalej.

”f1(f1(x))”, ”f1(f1(a1))”, ”f1(f1(a2))”
”f1(f2(x))”, ”f1(f2(a1))”, . . .
”f2(f1(x))”, ”f2(f1(a1))”, . . .
”f2(f2(x))”, . . .

Takto je možné pokračovať do nekonečna. Uvedeným postupom sa teda dá
zostaviť množina reťazcov Herbrandového univerza vzhľadom na príslušnú
schému. V našom prípade je táto množina spojená so schémou S.

Keď bližšie preskúmame schému S, zistíme, že napríklad term ”f1(f2(a2))”
nemôže nikdy počas behu výpočtu vzniknúť. Napriek tomu sa však v množine
Herbrandového univerza nachádza.

Príklad 7 Schéma S sa zastaví práve vtedy, keď sa zastaví výpočet pre
každú Herbrandovú interpretáciu schémy S.

Riešenie 7

=⇒: Z definície vieme, že schéma S sa zastaví, ak pre každú interpretáciu I
sa zastaví program (S, I). Program P = (S, I) sa zastaví, ak pre každé
ohodnotenie v vstupných premenných

x je hodnota val(S, I, v) definovaná.

Keďže sme predpokladali, že schéma S sa zastaví, tj. všetky výpočty na nej
sa zastavia, zastavia sa aj všetky výpočty s Herbrandovými interpretáciami.

⇐=: Musíme dokázať, že výpočet sa zastaví pre ľubovoľnú interpretáciu I a
ľubovolné ohodnotenie v vstupných premenných

x. Ku každej dvojici I a v

existuje s nimi zladená Herbrandová interpretácia IH. Z predpokladu sa ale
výpočet pre IH zastaví, takže sa musí zastaviť aj výpočet (S, I, v). Ak sa
zastavia všetky výpočty na schéme S, zastavia sa aj všetky programy (S, I).
Ak sa zastavia všetky programy, potom sa aj schéma S zastaví.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

6

1.2

Nerozhodnuteľnosť vlastností schém

Príklad 8 Máme danú schému S.

S : begin [y1, y2] := [a, a]

1 : if p(y1) then goto end
2 : [y1] := [f (y1)]
3 : if p(y1) then goto end
4 : [y1, y2] := [f (y1), f (y1)]
5 : if p(y1) then goto 7
6 : goto end
7 : if p(y2) then goto 4
8 : goto 2

end [z] := [a]

Nájdite interpretáciu I1 takú, že program P1 = (S, I1) diverguje.

Riešenie 8 Aby program divergoval, potrebujeme vytvoriť večný cyklus,
čiže zabezpečiť beh programu bez dosiahnutia príkazu na návestí end. Smer
behu programu ovplyvňujú predikáty. Pre náš zámer bude vhodné, ak pre-
dikát p(x) bude dávať napríklad takéto výsledky.

p(a) = f alse

p(f (a)) = f alse

p(f (f (a))) = true

Vždy po vykonaní príkazu na riadku 4 obsahujú premenné y1 a y2 rovnaké
hodnoty. Preto ak výsledok testu na riadku 5 bude true, potom bude true
aj výsledok testu na riadku 7. Pre večný cyklus teda stačí, aby ešte platila
nasledujúca podmienka.

∀n ≥ 2 : p(f n(a)) = true

Hľadaná interpretácia I1 = (D1, i1) môže potom vyzerať takto:

I1 : i1(p(x)) = x ≥ 2

i1(f (x)) = x + 1

i1(a) = 0

D1 = N

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

7

Príklad 9 Dokážte alebo vyvráťte tvrdenie, že pre schému S z predchádza-
júceho príkladu, pre každú konečnú doménu D2 a pre každý interpretačný
morfizmus i platí, že program P2 = (S, (D2, i2)) sa zastaví.

Riešenie 9 Tvrdenie neplatí. Ak na konečnej doméne D2 = {0, 1, 2}
upravíme funkciu f tak, že bude vstupný parameter inkrementovať najnajvýš
po hodnotu 2, dostávame dokonca divergentný program P2.

i2(p(x)) = x ≥ 2

i2(f (x)) = min(x + 1, 2)

i2(a) = 0

Príklad 10 Rozhodnite, či je problém dosiahnuteľnosti príkazu v štandard-
nej schéme rozhodnuteľný. Svoje tvrdenie dokážte.

Riešenie 10 Problém je čiastočne rozhodnuteľný.

1. Nie je (úplne) rozhodnuteľný.

Sporom. Predpokladajme, že je problém rozhodnuteľný. Potom vieme
rozhodnúť aj to, či je dosiahnuteľný príkaz end. Takto by sme ale
vedeli rozhodovať divergenciu schémy a to nasledovným spôsobom:

– ak je end dosiahnuteľný, tak schéma nie je divergentná,

– ak end dosiahnuteľný nie je, tak schéma je divergentná.

2. Je čiastočne rozhodnuteľný.

Zostrojíme procedúru, ktorá povie, že je príkaz dosiahnuteľný ak je
príkaz dosiahnuteľný. Ak je príkaz nedosiahnuteľný procedúra povie, že
je príkaz nedosiahnuteľný alebo nepovie nič (bude bežať donekonečna).

Procedúra simuluje výpočty programov na schéme reprezentovanej stro-
mom. Pri predikátoch existujú dve hrany, inde je hrana len jedna. Čiže
vrcholmi stromu s dvomi hranami sú miesta v schéme, kde sa testujú
predikáty (if . . . then . . .). Koreňom stromu je návestie begin.

Strom prehľadávame do šírky, tj. po rozdelení sledujeme všetky vetvy
stromu súčasne. Výpočet sa rozdelí na n ciest, ale n je vždy konečné
číslo. Koniec behu procedúry môže nastať v dvoch možných prípadoch.

a. V niektorej z ciest prídeme na príkaz, ktorého dosiahnuteľnosť

sme chceli zistiť. Odpovieme, že príkaz je dosiahnuteľný (aspoň
jednou interpretáciou a vstupným ohodnotením).

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

8

b. Všetkých n ciest sa dostane do príkazu end pričom ani jedna

neprešla hľadaným príkazom. Odpovieme, že príkaz nie je do-
siahnuteľný ani jednou interpretáciou s ľubovoľnými vstupnými
hodnotami.

V prípade, že daný príkaz nie je dosiahnuteľný a v programe sa vysky-
tuje cyklus, naša procedúra nikdy neskončí.

Príklad 11 Uvažujme triedu dosiahnuteľných schém D. Je príslušnosť sché-
my k triede D rozhodnuteľný problém? Svoje tvrdenie zdôvodnite.

Riešenie 11 Problém je čiastočne rozhodnuteľný.

Z definície vieme, že dosiahnuteľná schéma obsahuje iba dosiahnuteľné prí-
kazy. Pre každý príkaz v dosiahnuteľnej schéme existuje interpretácia, pri
ktorej sa príkaz vykoná.

V predchádzajúcom príklade sme dokázali, že problém dosiahnuteľnosti prí-
kazu je čiastočne rozhodnuteľný. V našej procedúre, ktorá bude skúmať
príslušnosť schémy k triede D, sa rovnakým spôsobom súčasne opýtame na
dosiahnuteľnosť všetkých príkazov schémy.

Množina príkazov schémy je konečná, takže sa v konečnom čase dozvieme, že:

– buď všetky príkazy schémy sú dosiahnuteľné, potom je aj schéma do-

siahnuteľná a teda patrí do triedy D,

– alebo existuje príkaz, ktorý nie je dosiahnuteľný, potom aj schéma nie

je dosiahnuteľná a teda nepatrí do triedy D,

– alebo sa beh procedúry neskončí a v tomto prípade schéma taktiež

nepatrí do triedy D.

Príklad 12 Uvažujme triedu štrukturovaných schém W. Je problém diver-
gencie pre štruktúrované schémy rozhodnuteľný? Svoje tvrdenie zdôvodnite.

Riešenie 12 Problém je rozhodnuteľný.

Štruktúrované schémy obsahujú iba riadiace štruktúry if a while a neob-
sahujú riadiacu štruktúru goto.

Pre každú štruktúrovanú schému sa dá

vytvoriť interpretácia taká, že pokiaľ návestie end existuje, tak bude dosiah-
nuté. Konštrukcia interpretácie je triviálna – výsledkom každého predikátu
použitého v riadiacej štruktúre while musí byť f alse.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

9

Z toho ale vyplýva, že neexistuje divergentná štruktúrovaná schéma taká, že
obsahuje návestie end. Naopak, ak schéma návestie end neobsahuje, tak
je určite divergentná. Preto je problém divergencie na W rozhodnuteľný.
Odpoveďou pre každú štruktúrovanú schému je, že schéma je divergentná ak
neobsahuje návestie end, inak nie je divergentná.

1.3

Porovnávanie tried programových schém

Príklad 13 Rozhodnite, či je schéma S voľná.

S : begin [y1, y2] := [a, a]

1 : if p(y1) then goto 4
2 : [y1] := [f (y1)]
3 : goto 1
4 : if p(y2) then goto end
5 : [y1, y2] := [g(y1), f (y2)]
6 : goto 4

end [z] := [y1]

Riešenie 13 Z definície vieme, že schéma S je voľná, keď pre každú cestu
vedúcu zo začiatočného príkazu existuje interpretácia I a ohodnotenie vstup-
ných premenných v také, že výpočet (S, I, v) sleduje túto cestu.

Schéma S reprezentuje dva cykly. Na začiatku sa premenné y1 a y2 inicializu-
jú na rovnakú hodnotu. V prvom cykle sa iteruje poďla y1, v druhom cykle
sa iteruje podľa y2. V oboch prípadoch testuje ukončenie cyklu predikát p
aplikovaný na iteračnú premennú. Takže oba cykly budú mať vždy rovnaký
počet opakovaní.

To je ale v rozpore s voľnosťou schémy, pretože nie sú možné výpočty, kde
počet opakovaní prvého cyklu nie je rovnaký ako pri druhom cykle. Takže
sa nedá spraviť napríklad 3-násobné opakovanie prvého cyklu nasledované
2-násobným opakovaním cyklu druhého. Schéma S teda nie je voľná.

Príklad 14 Máme danú Janovovu schému S1.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

10

S1 : begin [y] := [x]

1 : [y] := [f (y)]
2 : if p(y) then goto 6
3 : [y] := [f (y)]
4 : if p(y) then goto 6
5 : goto 2
6 : if q(y) then goto 8
7 : goto 4
8 : [y] := [f (y)]

end [z] := [y]

Nájdite ku schéme S1 ekvivalentnú voľnú Janovovu schému S1

v .

Schému

napíšte a stručne zdôvodnite, prečo je schéma S1

v

voľná a ekvivalentná

so schémou S1.

Riešenie 14 Riešením je schéma S1

v .

S1

v :

begin [y] := [x]

1 : [y] := [f (y)]
2 : if p(y) then goto 4
3 : goto 1
4 : if q(y) then goto 6
5 : goto 5
6 : [y] := [f (y)]

end [z] := [y]

Voľnosť: Ak predikát p(y) platí, tak sa už ďalej netestuje. Ak neplatí, tak
pred ďalším testom toho istého predikátu sa zmení premenná y. Predikát q(y)
sa testuje len raz. Pre každú cestu existuje interpretácia I1

v

a valuácia v1

v

taká, že výpočet (S1

v ,

I1

v ,

v1

v ) sleduje túto cestu, takže schéma je voľná.

Ekvivalencia: Oproti pôvodnej schéme sme zmenili príkaz 7 : goto 4 na nový
príkaz 5 : goto 5. V pôvodnej schéme bol tento príkaz dosiahnuteľný iba ak
na riadku 4 platil predikát p(y) a na riadku 6 neplatil predikát q(y), čoho
dôsledkom bol opäť skok na riadok 4 a rovnaké testy s rovnakými hodnotami,
čiže večný cyklus.

Cyklusom 5 : goto 5 sme teda dosiahli ekvivalentnú

schému.

Taktiež sme vynechali podmienku na riadku 4, pretože môže byť nahradená
ekvivalentnou podmienkou na riadku 2 pôvodnej schémy. Nakoniec sme zre-
dukovali príkazy na riadkoch 1 a 3 pôvodnej schémy, pretože sa po malých
úpravách novej schémy dajú nahradiť jedným príkazom.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

11

Príklad 15 Daná je štandardná schéma S2.

S2 : begin [y] := [x]

1 : if p(y) then goto end
2 : if q(y) then goto 6
3 : [y] := [f1(y)]
4 : if p(y) then goto 2
5 : goto end
6 : if p(y) then goto 10
7 : [y] := [f2(y)]
8 : if q(y) then goto end
9 : goto 1

10 : [y] := [f3(y)]
11 : goto 8

end [z] := [y]

Nájdite ku schéme S2 ekvivalentnú voľnú schému S2

v .

Riešenie 15 Riešením je schéma S2

v .

S2

v :

begin [y] := [x]

1 : if p(y) then goto end
2 : if q(y) then goto 6
3 : [y] := [f1(y)]
4 : if p(y) then goto 10
5 : goto end
6 : [y] := [f2(y)]
7 : if q(y) then goto end
8 : if p(y) then goto end
9 : goto 3

10 : if q(y) then goto 12
11 : goto 3
12 : [y] := [f3(y)]
13 : goto 7

end [z] := [y]

Schému S2

v

sme našli pomocou vytvorenia vývojového diagramu pôvodnej

schémy S2 a jeho následných modifikácií vedúcich k zvoľneniu pri zachovaní
ekvivalencie. Tento postup je štandardný. Nedoporučuje sa písať programový
kód výslednej schémy priamo1.

1pretože to ide naozaj len veľmi ťažko

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

12

Príklad 16 Daná je štandardná schéma S3.

S3 : begin [y] := [x]

1 : if p(y) then goto 9
2 : if q(y) then goto 5
3 : if p(y) then goto 8
4 : goto 2
5 : [y] := [f1(y)]
6 : if q(y) then goto 1
7 : goto end
8 : [y] := [f2(y)]
9 : [y] := [f3(y)]

end [z] := [y]

Nájdite ku schéme S3 ekvivalentnú voľnú schému S3

v .

Riešenie 16 Riešením úlohy je teda schéma S3

v .

S3

v :

begin [y] := [x]

1 : if q(y) then goto 4
2 : if p(y) then goto 8
3 : goto 3
4 : if p(y) then goto 8
5 : [y] := [f1(y)]
6 : if q(y) then goto 1
7 : goto end
8 : [y] := [f3(y)]

end [z] := [y]

Príklad 17 Máme danú štandardnú schému S.

S : begin [y1, y2] := [x, a]

1 : if p(y1) then goto end
2 : [y1, y2] := [f (y1), g(y1, y2)]
3 : goto 1

end [z] := [y2]

Nájdite ku schéme S ekvivalentnú rekurzívnu schému R.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

13

Riešenie 17 Ekvivalentnú rekurzívnu schému R zostrojíme pomocou štan-
dardného postupu. Návestia štandardnej schémy prepisujeme pomocou fun-
kčných premenných φi (simulácia toku riadenia) tak, aby v ich rekurzívnych
definíciach vektory vstupných argumentov y zodpovedali vektorom pracov-
ných premenných (simulácia zmenu stavu výpočtu).

φb(y1, y2) = z = φ1(x, a)
φ1(y1, y2) = if p(y1) then φe(y1, y2) else φ2(y1, y2)
φ2(y1, y2) = φ3(f (y1), g(y1, y2))
φ3(y1, y2) = φ1(y1, y2)
φe(y1, y2) = y2

Jednoduchým dosadením do funkčných premenných φi dosiahneme zjednoduše-
nie systému rekurzívnych definícií a výslednú schému R.

R : begin [y1, y2] := [x, a]

φ1(y1, y2) ⇐= if p(y1) then y2 else φ1(f (y1), g(y1, y2))

end [z] := [φ1(x, a)]

Príklad 18 Daná je štandardná schéma S.

S : begin [y] := [x]

1 : if p(y) then goto end
2 : [y] := [f (y)]
3 : if q(y) then [y] := [g(y)]
4 : if p(y) then goto 2
5 : goto 1

end [z] := [y]

Nájdite rekurzívnu schému R, ktorá je ekvivalentná so schémou S. Upravte
nájdenú schému tak, aby mala minimálny počet funkčných premenných.

Riešenie 18 Keďže ide o úlohu rovnakého typu ako v predchádzajúcom
príklade, aj náš postup bude obdobný. Najskôr vytvoríme základnú sústavu
rekurzívnych definícií.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

14

φb(y) = z = φ1(x)
φ1(y) = if p(y) then φe(y) else φ3(f (y))
φ2(y) = φ3(f (y))
φ3(y) = if q(y) then φ4(g(y)) else φ4(y)
φ4(y) = if p(y) then φ2(y) else φ5(y)
φ5(y) = φ1(y)
φe(y) = y

Minimálny počet funčných premenných dosiahneme nasledovnými krokmi:

– Zrušením φ2 a dosadením φ3 na príslušné miesta vo φ1 a φ4.

– Zrušením φe a dosadením y na príslušné miesto vo φ1.

– Zrušením φ5 a dosadením φ1 na príslušné miesto vo φ4.

– Zrušením φ4 a dosadením príkazu if na príslušné miesta vo φ3.

Po týchto úpravách dostávame výslednú rekurzívnu schému R, ktorá je ek-
vivalentá so schémou S.

R : begin [y] := [x]

φ1(y) ⇐= if p(y) then y

else φ3(f (y))

φ3(y) ⇐= if q(y) then if p(g(y)) then φ3(f (g(y)))

else φ1(g(y))

else if p(y) then φ3(f (y))

else φ1(y)

end [z] := [φ1(x)]

Príklad 19 Máme danú štandardnú schému S.

S : begin [y] := [x]

1 : [y] := [f (y)]
2 : if p(y) then goto 5
3 : [y] := [g(y)]
4 : goto 1
5 : if p(y) then [y] := [h(y)]
6 : if p(y) then goto end
7 : goto 5

end [z] := [y]

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

15

Nájdite ku schéme S ekvivalentnú rekurzívnu schému R.

Riešenie 19 Do tretice je uvedený príklad rovnakého typu, tj. úloha na
prevod štandardnej schémy do rekurzívnej. Tentoraz však iba s výslednou
podobou rekurzívnej schémy. Čitateľ si tak môže aspoň porovnať výsledok.

R : begin [y] := [x]

φ1(y) ⇐= if p(f (y)) then φ5(f (y))

else φ1(g(f (y)))

φ5(y) ⇐= if p(y) then if q(h(y)) then h(y)

else φ5(h(y))

else if q(y) then y

else φ5(y)

end [z] := [φ1(x)]

Príklad 20 Máme danú rekurzívnu schému R.

R : begin [. . .] := [. . .]

φ(y) ⇐= if p(y) then f (y) else h(φ(g(y)))

end [z] := [φ(a)]

Zistite, či existuje k tejto schéme štandardná schéma S. V prípade, že exis-
tuje, nájdite ju.

Riešenie 20 Štandardným postupom hľadania ekvivalentnej rekurzívnej sché-
my k štandardnej schéme je:

1. Zistiť akého tvaru je výstupná premenná rekurzívnej schémy a rozhod-

núť, či môže existovať štandardná schéma dávajúca rovnaké výsledky.

2. V prípade kladnej odpovede v predchádzajúcom bode už ostáva iba túto

schému nájsť. V mnohých prípadoch to ide, nie však vo všeobecnosti.

Výstupná premenná z schémy R je tvaru hnf gn(a), kde hodnota n vyjadru-
je hĺbku rekurzívneho vnorenia. V triede štandardných schém S existuje
schéma S ekvivalentná s R generujúca výstupné premenné uvedeného tvaru.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

16

S : begin [y1, y2] := [a, a]

1 : if p1(y1) then goto 4
2 : [y1] := [g(y1)]
3 : goto 1
4 : [y1] := [f (y1)]
5 : if p(y2) then goto end
6 : [y1, y2] := [h(y1), g(y2)]
7 : goto 5

end [z] := [y1]

Obsah pracovných premenných [y1, y2] v príkaze begin bol [a, a], pred
riadkom 4 bol [gn(a), a], po riadku 4 bol [f gn(a), a] a nakoniec v príkaze end
bol obsah pracovných premenných [hnf gn(a), gn(a)]. Výstupnej premennej z
sa priraďuje hodnota y1, ktorej obsah je v žiadanom tvare.

Príklad 21 Uvažujme triedu štruktúrovaných schém Wb. Trieda Wb je obo-
hatená o booleovské premenné a dobre otypované priradenie do booleovských
premenných. Ktorú z uvedených konštrukcií je alebo nie je možné preložiť
do ekvivalentnej schémy z triedy Wb? Zdôvodnite prečo.

W1 : while b1 ∧ b2 do S od
W2 : while b1 ∨ b2 do S od
W3 : while ¬b do S od

Riešenie 21 Začneme konštrukciou W2, ktorá ide preložiť do triedy W.
Z toho vyplýva, že určite pôjde preložiť aj do triedy Wb. Použitie booleovských
premenných a priradení je však v tomto prípade nepotrebné.

W

0

2 :

while b1 do S;
while b2 do

while b1 do S;

Pre nasledujúce programové konštrukcie však už bude použitie booleovskej
premennej nevyhnutné. Máme teda možnosť použitia premennej bool, do ktorej
môžeme priraďovať hodnoty iných booleovských premenných, ako je napr. b1
alebo b2. Tiež je možné priamo priraďovať booleovské konštanty true a f alse.
Je nutné si ale uvedomiť, že trieda Wb nie je čiastočne interpretovaná vzhľa-
dom na použitie logických operátorov ∧ (AND), ∨ (OR) alebo ¬ (NOT).

Nájdime teda konštrukciu W

0

1 ∈ W

b ekvivalentnú s W

1.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

17

W

0

1 :

[bool] := f alse;
if b1 then

if b2 then [bool] := true;

while bool do

S;
[bool] := f alse;
if b1 then

if b2 then [bool] := true;

od

Viac elegancie v riešení je možné získať nahradením konštrukcií

[bool] := f alse;
if b1 then

if b2 then [bool] := true;

za jednoduchšie

if b1 then [bool] := [b2]

else [bool] := [b1]

Uvedeným spôsobom sa dá dokonca vyhnúť použitiu konštánt true a f alse.
To už však nie je možné pri zostávajúcej konštrukcii W

0

3 ∈ W

b, ktorá je

ekvivalentná s W3.

W

0

3 :

[bool] := true;
if b then [bool] := f alse;
while bool do

S;
[bool] := true;
if b then [bool] := f alse;

od

Príklad 22 Uvažujme triedu voľných schém V, triedu rekurzívnych schém R
a triedu dosiahnuteľných schém D. Sformulujte a zdôvodnite vzťahy medzi
uvedenými triedami schém a triedou štandardných schém S na základe relácií
podtrieda ⊆, preložiteľná trieda v a efektívne preložiteľná trieda

E.

Riešenie 22

S, V – porovnanie tried štandardných a voľných schém

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

18

S /

⊆ V Existuje štandardná schéma, ktorá nie je voľná.

S /

v V Vo všeobecnosti neexistuje postup, pomocou ktorého sa dá spraviť ek-

vivalentná voľná schéma ku každej štandardnej schéme, aj keď v mno-
hých prípadoch to ide. Pre kontrapríklad pozri tvrdenie D /

v V.

S /

E V Priamo vyplýva z tvrdenia S /

v V.

V ⊆ S, V v S, V E S

Tvrdenia sú zrejmé, vyplývajú priamo z definícií.

S, R – porovnanie tried štandardných a rekurzívnych schém

S /

⊆ R Ide o syntakticky odlišné schémy, takže principiálne nemôžu byť nav-

zájom podtriedami.

S v R Štandardná schéma sa dá previesť na ekvivalentnú rekurzívnu schému.

S E R Existuje štandardný postup, pomocou ktorého sa dá previesť štandard-

ná schéma na ekvivalentú rekurzívnu. Niekoľko ukážok sa nachádza aj
v tejto zbierke príkladov.

R /

⊆ S Ide o syntakticky odlišné schémy, takže principiálne nemôžu byť nav-

zájom podtriedami.

R /

v S Existuje rekurzívna schéma ku ktorej neexistuje ekvivalentná štandard-

ná schéma. V niektorých prípadoch sa však rekurzívna schéma dá pre-
viesť na ekvivalentú štandardnú (viz. napríklad úlohu v tejto zbierke).

R /

E S Priamo vyplýva z tvrdenia R /

v S.

S, D – porovnanie tried štandardných a dosiahnuteľných schém

S /

⊆ D Existuje štandardná schém, ktorá nie je dosiahnuteľná. Kontraprík-

ladom je schéma obsahujúca jeden alebo viac komponetov nesúvislosti
(tzv. ostrovčeky).

S v D Odstránením komponentov nesúvislosti zo štandardnej schémy sa stane

schéma dosiahnuteľnou.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

19

S /

E D Odstraňovanie komponetov nesúvislosti však nemôže ísť spraviť efek-

tívne. Ak by to išlo, vedeli by sme rozhodovať divergenciu štandard-
ných schém. Každú schému z triedy S by sme previedli na ekvivalentnú
schému z triedy D a spýtali sa na dosiahnuteľnosť návestia end.

D ⊆ S, D v S, D E S

Tvrdenia sú zrejmé, vyplývajú priamo z definícií.

Príklad 23 Uvažujme triedu dosiahnuteľných schém D, triedu priechod-
ných schém P a triedu Janovových schém J .

Sformulujte a zdôvodnite

vzťahy medzi uvedenými triedami schém a triedou voľných schém V na zák-
lade relácií podtrieda ⊆, preložiteľná trieda v a efektívne preložiteľná trie-
da

E.

Riešenie 23

V, D – porovnanie tried voľných a dosiahnuteľných schém

V /

⊆ D Komponenty nesúvislosti neodporujú voľnosti, nakoľko do nich nevedie

cesta zo začiatku schémy.

Odporujú však dosiahnuteľnosti schémy.

Preto existuje schéma, ktorá je voľná, ale nie je dosiahnuteľná.

V v D Vyplýva z tvrdení V ⊆ S ∧ S v D.

V E D Keďže voľné schémy sú orientované grafy a na orientovaných grafoch

existuje algoritmus odstraňujúci komponenty nesúvislosti, potom sa dá
každá voľná schéma efektívne preložiť do ekvivalentnej dosiahnuteľnej
schémy. Algoritmus je lineárny vzhľadom na počet hrán a kvadratický
vzhľadom na počet príkazov schémy.

D /

⊆ V Existuje dosiahnuteľná schéma, ktorá nie je voľná.

i : if p(y) then goto i + 2

i + 1 : if p(y) then goto i + 3
i + 2 : [y] := [y]
i + 3 : . . .

Všetky príkazy v načrtnutej časti schémy sú dosiahnuteľné, ale cesta
z i + 1 do i + 3 nie je voľná.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

20

D /

v V Existuje dosiahnuteľná schéma, ktorá sa nedá previesť na voľnú. Prík-

ladom môže byť napríklad nasledujúca schéma s dvojitým cyklusom dá-
vajúca na výstupe f ngn(a), kde n je počet opakovaní prvého a druhého
cyklu.

begin [y1, y2] := [a, a]

1 : if p(y1) then goto 4
2 : [y1] := [f (y1)]
3 : goto 1
4 : if p(y2) then goto end
5 : [y1, y2] := [g(y1), f (y2)]
6 : goto 4

end [z] := [y1]

D /

E V Priamo vyplýva z tvrdenia D /

v V.

V, P – porovnanie tried voľných a priechodných schém

V /

⊆ P Existuje voľná schéma, ktorá nie je priechodná. Inkriminovaná schéma

obsahuje také komponenty nesúvislosti, ktoré neodporujú voľnosti, ale
odporujú priechodnosti schémy.

V v P Odstránením komponentov nesúvislosti voľnej schémy dostávame ekvi-

valentnú priechodnú schému.

V E P Analogicky ako dôkaz tvrdenia V E D. Je nutné najdenie komponen-

ty súvislosti orientovaného grafu s vrcholom begin reprezentujúceho
voľnú schému a odstránenie ostatných komponentov nesúvislosti.

P /

⊆ V Existuje priechodná schéma, ktorá nie je voľná. Pre kontrapríklad pozri

tvrdenie D /

v V.

P /

v V Existuje priechodná schéma, ktorá sa nedá preložiť do ekvivalentnej

voľnej schémy. Pre kontrapríklad pozri tvrdenie D /

v V.

P /

E V Priamo vyplýva z tvrdenia P /

v V.

V, J – porovnanie tried voľných a Janovových schém

V /

⊆ J Existuje voľná schéma, ktorá nie je Janovova. Je to jednoducho taká,

ktorá obsahuje viac ako jednu pracovnú premennú.

KAPITOLA 1. PROGRAMOVÉ SCHÉMY

21

V /

v J Existuje voľná schéma, ktorá sa nedá preložiť do ekvivalentnej Jano-

vovej schémy. Ako kontrapríklad poslúži voľná schéma, ktorá obsahuje
dve pracovné premenné, pričom obe sú v schéme využívané tak, že sa
nedajú nahradiť jednou pracovnou premennou.

V /

E J Priamo vyplýva z tvrdenia V /

v J .

J /

⊆ V Existuje Janovova schéma, ktorá nie je voľná.

J v V Z každej Janovovej schémy sa dá spraviť ekvivalentná voľná Janovova

schéma. Dôkaz tvrdenia sa nachádza v skriptách.

J E V Každá Janovova schéma sa dá efektívne preložiť do ekvivalentnej voľnej

Janovovej schémy. Popis postupu sa opäť nachádza v skriptách.

Kapitola 2

Správnosť programov

2.1

Metódy dokazovania správnosti

Príklad 24 Uvažujme nasledujúci štandardný program P , ktorý počíta d

√

xe

(hornú celú časť odmocniny x).

P : begin [y1, y2] := [1, 1]

1 : if y2 ≥ x then goto end
2 : [y1, y2] := [y1 + 1, (y1 + 1)

2]

3 : goto 1

end [z] := [y1]

Definujte vstupnú podmienku, výstupnú podmienku a invarianty. Floydovou
metódou dokážte čiastočnú správnosť programu vzhľadom na vstupnú a výs-
tupnú podmienku.

Riešenie 24 Vstupná podmienka presne vymedzuje vstupné hodnoty pre
ktoré dáva program žiadaný výsledok. V našom prípade ide o všetky klad-
né hodnoty. Program by sa dal modifikovať aj tak, aby dával zmysluplné
výsledky pre všetky nezáporné hodnoty, ale prinieslo by nám to isté množst-
vo ďalších komplikácií. Takže vstupná podmienka p vyzerá nasledovne.

p(x) : x > 0

Výstupná podmienka q popisuje z = d

√

xe.

22

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

23

q(x, z) :

d

√

xe = z

(z − 1)

<

√

x

≤ z

(z − 1)2 <

x

≤ z2

Invariantu v príkaze begin zodpovedá vstupná podmienka a invariantu v príkaze
end zodpovedá výstupná podmienka.

IB = p
IE = q

Program obsahuje jeden cyklus. Ideálne miesto pre jeho deliaci bod je tam,
kde sa z cyklu vychádza. V programe P je to rovnaké miesto ako to, kde
sa do cyklu vchádza. Ako deliaci bod teda zvolíme riadok 1. Invariant I1
v tomto bode vyzerá nasledovne.

I1 : (y1 − 1)

2 < x ∧ y

2 = y

2

1

Prvá časť invariantu I1 reprezentuje riadiacu podmienku cyklu. V druhej
časti sa definuje závislosť medzi premennými y1 a y2.

Program P obsahuje tri deliace body medzi ktorými sú tri konečné cesty.

–

cesta B1:

begin

→

riadok 1

–

cesta 11:

riadok 1

→

riadok 1

–

cesta 1E:

riadok 1

→

end

Z definície vieme, že pre každú cestu musíme dokázať verifikačnú podmienku
odvodenú z nasledujúceho všeobecného tvaru.

∀x, y IA(x, y) ∧ RAB(x, y) =⇒ IB(x, rAB(x, y))

cesta B1: Použitím spätnej substitúcie odvodíme podmienku prechodu a mo-
difikáciu pracovných premenných na ceste B1 a dosadíme do príslušnej veri-
fikačnej podmienky.

RB1(y1, y2) = true

rB1(y1, y2) = (1, 1)

IB ∧ true ⇒ I1(1, 1)

x > 0 ∧ true ⇒ (1 − 1)2 < x ∧ 12 = 1
x > 0 ∧ true ⇒ 0 < x ∧ 1 = 1
x > 0 ∧ true ⇒ x > 0

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

24

cesta 11: Podobne ako v predchádzajúcom prípade odvodíme R11 a r11 a
dosadíme do verifikačnej podmienky pre cestu 11.

R11(y1, y2) = true ∧ ¬(y2 ≥ x) = y2 < x

r11(y1, y2) = (y1 + 1, (y1 + 1)

2)

I1(y1, y2) ∧ y2 < x ⇒ I1(y1 + 1, (y1 + 1)

2)

(y1 − 1)

2 < x ∧ y2

1 = y2 ∧ y2 < x

⇒ (y1 + 1 − 1)2 < x ∧ (y1 + 1)2 = (y1 + 1)2

y2

1 = y2 ∧ y2 < x

⇒ y2

1 < x ∧ true

y2

1 < x

⇒ y2

1 < x

cesta 1E: A do tretice aj pre poslednú cestu odvodíme spätnou substitúciou
R1E a r1E a dosadíme do prislúchajúcej verifikačnej podmienky.

R1E(y1, y2) = true ∧ y2 ≥ x

r1E(z) = y1

I1(y1, y2) ∧ y2 ≥ x ⇒ IE

(y1 − 1)

2 < x ∧ y

2 = y

2

1

∧ y2 ≥ x ⇒ (y1 − 1)2 < x ≤ y2

1

(y1 − 1)

2 < x ∧ y2

1 ≥ x

⇒ (y1 − 1)2 < x ∧ y2

1 ≥ x

Pre všetky cesty v programe P sme overili platnosť príslušných odvodených
verifikačných podmienok a tým sme dokázali aj čiastočnú správnosť progra-
mu P vzhľadom na vstupnú podmienku p a výstupnú podmienku q.

Príklad 25 Daný je štandardný program P .

P : begin [y1, y2] := [0, x1]

1 : if y2 < x2 then goto end
2 : [y1, y2] := [y1 + 1, y2 − x2]
3 : goto 1

end [z1, z2] := [y1, y2]

Floydovou metódou formálne dokážte čiastočnú správnosť programu P vzhľa-
dom na nasledujúce podmienky:

• vstupná podmienka – p(x1, x2) : x1 ≥ 0 ∧ x2 > 0

• výstupná podmienka – q(x1, x2, z1, z2) : z1x2 + z2 = x1 ∧ 0 ≤ z2 < x2

Určte deliace body, nájdite k nim prislúchajúce invarianty, zostrojte veri-
fikačné podmienky a ukážte, že platia.

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

25

Riešenie 25 Po krátkej analýze zistíme, že program delí hodnotu vstupnej
premennej x1 hodnotou x2. Deliteľ je uložený do výstupnej premennej z1 a
zvyšok po delení do premennej z2. Výsledok je tak tvaru x1 = z1x2 + z2,
kde z2 < x2 (zvyšok je menší ako hodnota, ktorou delíme).

Máme dva implicitné deliace body v návestiach begin a end. Invariantom
v týchto bodoch zodpovedajú vstupná podmienka p a výstupná podmienka q.
Takže platí IB = p a IE = q.

Keďže program opäť obsahuje jeden cyklus, ako jeho deliaci bod zvolíme
riadok 1. Je to miesto kde sa do cyklu vchádza i vychádza. Konštrukcia
invariantu k tomuto deliacemu bodu programu je nerozhodnuteľným prob-
lémom. Preto sa snažíme vyčítať z vlastností programu i cyklu čo najviac
užitočných informácií a vložiť ich do podmienok invariantu I1.

I1 : x1 = y1x2 + y2 ∧ x2 > 0 ∧ y1 ≥ 0 ∧ y2 ≥ 0

Pre každú z troch ciest odvodíme a dokážeme verifikačnú podmienku.

cesta B1:

RB1(y1, y2) = true

rB1(y1, y2) = (0, x1)

IB ∧ true ⇒ I1(0, x1)

x1 ≥ 0 ∧ x2 > 0 ⇒ x1 = 0x2 + x1 ∧ x2 > 0 ∧ 0 ≥ 0 ∧ x1 ≥ 0
x1 ≥ 0 ∧ x2 > 0 ⇒ x1 = x1 ∧ x2 > 0 ∧ x1 ≥ 0
x1 ≥ 0 ∧ x2 > 0 ⇒ x1 ≥ 0 ∧ x2 > 0

cesta 11:

R11(y1, y2) = true ∧ ¬(y2 < x2) = y2 ≥ x2

r11(y1, y2) = (y1 + 1, y2 − x2)

I1(y1, y2) ∧ y2 ≥ x2 ⇒ I1(y1 + 1, y2 − x2)

x1 = y1x2 + y2 ∧ x2 > 0 ∧ y1 ≥ 0 ∧ y2 ≥ 0 ∧ y2 ≥ x2 ⇒

⇒ x1 = (y1 + 1)x2 + (y2 − x2) ∧ x2 > 0 ∧ y1 + 1 ≥ 0 ∧ y2 − x2 ≥ 0

(zrejme y2 ≥ 0 ∧ x2 > 0 ∧ y2 ≥ x2 ⇒ y2 − x2 ≥ 0)

x1 = y1x2 + y2 ∧ y1 ≥ 0 ∧ y2 − x2 ≥ 0 ⇒

⇒ x1 = y1x2 + y2 ∧ y1 + 1 ≥ 0 ∧ y2 − x2 ≥ 0

(zrejme platí y1 ≥ 0 ⇒ y1 + 1 ≥ 0)

cesta 1E:

R1E(y1, y2) = true ∧ y2 < x2

r1E(z1, z2) = (y1, y2)

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

26

I1(y1, y2) ∧ y2 < x2 ⇒ IE

x1 = y1x2 + y2 ∧ x2 > 0 ∧ y1 ≥ 0 ∧ y2 ≥ 0 ∧ y2 < x2 ⇒

⇒ x1 = y1x2 + y2 ∧ 0 ≤ y2 < x2

x1 = y1x2 + y2 ∧ y2 ≥ 0 ∧ y2 < x2 ⇒

⇒ x1 = y1x2 + y2 ∧ y2 ≥ 0 ∧ y2 < x2

Po overení verifikačných podmienok pre všetky cesty je čiastočná správnosť
programu P dokázaná.

Príklad 26 Daný je štruktúrovaný program P .

P : begin [y1, y2] := [1, 1]

while y2 < x do

[y1, y2] := [y1 + 1, (y1 + 1)

2]

od

end [z] := [y1]

Hoareovou metódou formálne dokážte čiastočnú správnosť programu P vzhľa-
dom na nasledujúce podmienky:

• vstupná podmienka – p(x) : x > 0

• výstupná podmienka – q(x, y) : (z − 1)2 < x ≤ z2

Riešenie 26 Hoareova metóda dokazovania čiastočnej správnosti štruktú-
rovaných programov sa opiera o logický systém založený na jazyku induk-
tívnych formúl {p} P {q}. Pri dokazovaní sa používajú všetky platné formu-
ly špecifikačného jazyka, axióma priradenia a inferenčné resp. odvodzovacie
pravidlá Hoareovského kalkulu.

Pre dôkaz čiastočnej správnosti programu P musíme dokázať platnosť nasle-
dujúcej induktívnej formuly.

{p} P {q}

Krátkou analýzou zistíme, že program P sa skladá z troch častí. Z dostup-
ných inferenčných pravidiel teda aplikujeme pravidlo kompozície a vyriešime
induktívne formuly zodpovedajúce jednotlivým častiam programu P .

{p} P1 {r} {r} P2 {s} {s} P3 {q}

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

27

Ešte pred samotným riešením jednotlivých induktívnych formúl sa pokúsime
prispôsobiť si podmienky r a s. Časť P2 je while cyklus s podmienkou b,
preto uhádneme, ako by mohla vyzerať podmienka s, ktorá platí po jeho
ukončení.

s ≡ r ∧ ¬b

Je nutné podotknúť, že v našom prípade tento postup povedie k úspechu.
Rozhodne však neplatí vo všeobecnosti na všetky štruktúrované programy.

• Induktívna formula {p} P1 {r}: Časť P1 programu P obsahuje jediné

priradenie v návestí begin. Použitím axiómy priradenia nahradíme
v podmienke r obe premenné y1 a y2 hodnotou 1. Určite platí

{r[y1/1, y2/1]} P1 {r}

Ak sa podarí dokázať nasledujúcu implikáciu, bude možné použiť pravid-
lo následku a tým bude induktívna formula {p} P1 {r} dokázaná.

p ⇒ r[y1/1, y2/1]

• Induktívna formula {r} P2 {r ∧ ¬b}: Časť P2 programu P je reprezen-

tovaná cyklusom while. Preto použijeme pravidlo iterácie.

{r ∧ b} P21 {r}

Pre priradenie nachádzajúce sa v cykle while použijeme axiómu pri-
radenia. Určite teda platí

{r[y1/y1 + 1, y2/(y1 + 1)

2]} P

21 {r}

Dokázaním nasledujúcej implikácie dokážeme platnosť celej induktívnej
formuly {r} P2 {r ∧ ¬b}.

r ∧ b ⇒ r[y1/y1 + 1, y2/(y1 + 1)

2]

• Induktívna formula {r ∧ ¬b} P3 {q}: Podobne ako časť P1 aj časť P3

programu P obsahuje len jedno priradenie, tentokrát v návestí end.
Aplikujeme axiómu priradenia. Potom určite platí

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

28

{q[z/y1]} P3 {q}

Ak sa podarí dokázať nasledujúcu implikáciu, bude možné použiť pravid-
lo následku a tým bude induktívna formula {r ∧ ¬b} P3 {q} dokázaná.

r ∧ ¬b ⇒ q[z/y1]

Z troch hlavných častí programu teda dostávame tri implikácie, ktorých plat-
nosť je nutné dokázať.

p(x) ∧ true ⇒ r[y1/1, y2/1]

r ∧ b ⇒ r[y1/y1 + 1, y2/(y1 + 1)

2]

r ∧ ¬b ⇒ q[z/y1]

Musíme sformulovať podmienku r. Podobne ako hľadanie invariantu vo Floy-
dovej metóde, je nájdenie tejto podmienky netriviálny a nedeterministický
proces. Je vhodné a vo väčšine prípadov aj úspešné vychádzať z poslednej
implikácie a odvodiť hľadanú podmienku r od výstupnej podmienky q.

V našom prípade je podmienka r rovnaká, ako prislúchajúci invariant v ek-
vivalentnom štandardnom programe dokazovanom Floydovou metódou.

r ≡ y

2

1 = y2 ∧ (y1 − 1)

2 < x

Poznáme podmienku b cyklu while v časti P2.

b ≡ y2 < x

Výsledné implikácie teda vyzerajú nasledovne.

x > 0 ∧ true ⇒ 12 = 1 ∧ (1 − 1)2 < x

y2

1 = y2 ∧ (y1 − 1)

2 < x ∧ y

2 < x

⇒ (y1 + 1)2 = (y1 + 1)2 ∧ (y1 + 1 − 1)2 < x

y2

1 = y2 ∧ (y1 − 1)

2 < x ∧ y

2 ≥ x

⇒ (y1 − 1)2 < x ≤ y2

1

Samotné dôkazy implikácií sú priamočiare a jednoduché.

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

29

Príklad 27 Daný je štruktúrovaný program P .

P : begin [y1, y2] := [0, x1]

while y2 ≥ x2 do

[y1, y2] := [y1 + 1, y2 − x2]

od

end [z1, z2] := [y1, y2]

Hoareovou metódou formálne dokážte čiastočnú správnosť programu P vzhľa-
dom na nasledujúce podmienky:

• vstupná podmienka – p(x1, x2) : x1 ≥ 0 ∧ x2 > 0

• výstupná podmienka – q(x1, x2, z1, z2) : z1x2 + z2 = x1 ∧ 0 ≤ z2 < x2

Riešenie 27 V predchádzajúcom príklade na dokazovanie čiastočnej správ-
nosti programu P Hoareovou metódou sme použili tzv. postup zhora dole.
Vychádzali sme z induktívnej formuly {p}P {q}, na ktorú sme postupne ap-
likovali inferenčné odvodzovacie pravidlá a axiómu priradenia. Týmto spô-
sobom sme dospeli k niekoľkým implikáciam, ktoré sme dokázali.

Akosi implicitne sme predpokladali, ze dokázaním týchto implikácií sa dokáže
aj induktívna formula {p}P {q} a teda aj čiastočná správnosť programu P .
To je samozrejme pravda, no v skutočnosti má táto induktívna formula stáť
na konci celého procesu odvodzovania a dokazovania a nie na jeho začiatku.
Preto existuje aj spôsob, ako zapísať Hoareovu metódu formálnejšie.

Je nutné zdôrazniť, že oba zápisy sú dobré. Prvý je názornejší, keďže neza-
číname ničnehovoriacim tvrdením, ale známou všeobecnou induktívnou for-
mulou. Druhý zápis je zase formálnejší. Nasledujúci dôkaz čiastočnej správ-
nosti Hoareovou metódou zapíšeme formálnejším spôsobom. Tento spôsob je
používaný taktiež v skriptách.

Zvolíme si invariant.

R(x1, x2, y1, y2) : y1x2 + y2 = x1 ∧ 0 ≤ y2 < x2

1. x1 ≥ 0 ∧ x2 > 0 ⇒ R(x1, x2, 0, x1)

0x2 + x1 = x1 ∧ x1 ≥ 0

2. {R(x1, x2, 0, x1)}

[y1, y2] := [0, x1]

{R(x1, x2, y1, y2)}
axióma priradenia

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

30

3. {x1 ≥ 0 ∧ x2 > 0}

[y1, y2] := [0, x1]

{R(x1, x2, y1, y2)}
pravidlo následku pre 1. a 2.

4. R(x1, x2, y1, y2) ∧ y2 ≥ x2 ⇒ R(x1, x2, y1 + 1, y2 − x2)

y1x2 + y2 = x1 ∧ y2 ≥ 0 ∧ y2 ≥ x2 ⇒

⇒ (y1 + 1)x2 + y2 − x2 = x1 ∧ y2 − x2 ≥ 0

y1x2 + y2 = x1 ∧ y2 ≥ 0 ∧ y2 ≥ x2 ⇒ y1x2 + y2 = x1 ∧ y2 ≥ x2

5. {R(x1, x2, y1 + 1, y2 − x2)}

[y1, y2] := [y1 + 1, y2 − x2]

{R(x1, x2, y1, y2)}
axióma priradenia

6. {R(x1, x2, y1, y2) ∧ y2 ≥ x2}

[y1, y2] := [y1 + 1, y2 − x2]

{R(x1, x2, y1, y2)}
pravidlo následku pre 4. a 5.

7. {R(x1, x2, y1, y2)}

while y2 ≥ x2 do

[y1, y2] := [y1 + 1, y2 − x2]

od

{R(x1, x2, y1, y2) ∧ y2 < x2}
pravidlo iterácie pre 6.

8. {x1 ≥ 0 ∧ x2 > 0}

[y1, y2] := [0, x1]
while y2 ≥ x2 do

[y1, y2] := [y1 + 1, y2 − x2]

od

{R(x1, x2, y1, y2) ∧ y2 < x2}
pravidlo kompozície pre 3. a 7.

9. R(x1, x2, y1, y2) ∧ y2 < x2 ⇒ y1x2 + y2 = x1 ∧ 0 ≤ y2 < x2

y1x2 + y2 = x1 ∧ y2 ≥ 0 ∧ y2 < x2 ⇒ y1x2 + y2 = x1 ∧ 0 ≤ y2 < x2

10. {y1x2 + y2 = x1 ∧ 0 ≤ y2 < x2}

[z1, z2] := [y1, y2]

{z1x2 + z2 = x1 ∧ 0 ≤ z2 < x2}
axióma priradenia

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

31

11. {R(x1, x2, y1, y2) ∧ y2 < x2}

[z1, z2] := [y1, y2]

{z1x2 + z2 = x1 ∧ 0 ≤ z2 < x2}
pravidlo následku pre 9. a 10.

12. {x1 ≥ 0 ∧ x2 > 0}

[y1, y2] := [0, x1]
while y2 ≥ x2 do

[y1, y2] := [y1 + 1, y2 − x2]

od
[z1, z2] := [y1, y2]

{z1x2 + z2 = x1 ∧ 0 ≤ z2 < x2}
pravidlo kompozície pre 8. a 11.

Príklad 28 Uvažujme nasledujúci štruktúrovaný program P .

P : begin [y1, y2, y3] := [1, 0, 0]

while y1 ≤ n do

[y3] := [a[y1]];
if y3 < 0 then

[y3] := [−y3]

fi;
[y1, y2] := [y1 + 1, y2 + y3]

od

end [z] := [y2]

Hoareovou metódou formálne dokážte čiastočnú správnosť programu P vzhľa-
dom na vstupnú a výstupnú podmienku:

• vstupná podmienka – p(a, n) : n ≥ 0

• výstupná podmienka – q(a, n, z) : z =

Pn

i=1 |a[i]|

Riešenie 28 Začíname použitím pravidla kompozície.

{p} P1 {r} {r} P2 {s} {s} P3 {q}

{p} P {q}

Postupne dokážeme všetky tri induktívne formuly. Prvú, tretiu a nakoniec
druhú, ktorá je najobsiahlejšia.

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

32

• Induktívna formula {p} P1 {r}: Vieme, že podľa axiómy priradenia pla-

tí tvrdenie {r[y1/1, y2/0, y3/0]}P1{r}. Musíme teda dokázať nasledu-
júcu implikáciu.

p ⇒ r[y1/1, y2/0, y3/0]

• Induktívna formula {s} P3 {q}: Určite platí {q[z/y2]}P3{q} a tak dokazu-

jeme nasledujúcu implikáciu.

s ⇒ q[z/y2]

• Induktívna formula {r} P2 {s}: Časť P2 programu P obsahuje cyklus

while, pre ktorý je možné použiť pravidlo iterácie. Ešte pred tým si
však musíme upraviť induktívnu formulu pravidlom následku.

{r} while b do P

0

2 od {r ∧ ¬b}

(r ∧ ¬b ⇒ s)

{r} while b do P

0

2 od {s}

{r ∧ b} P

0

2 {r}

{r} while b do P

0

2 od {r ∧ ¬b}

Pre vnútorný príkaz P

0

2 cyklusu while použijeme pravidlo kompozície,

pretože sa skladá z troch osobitných častí.

{r ∧ b} P21 {f } {f } P22 {g} {g} P23 {r}

{r ∧ b} P

0

2 {r}

Časti P21 a P23 sú reprezentované priradeniami. Určite platia tvrdenia
{f [y3/a[y1]]}P21{f } a {r[y1/y1 + 1, y2/y2 + y3]}P23{r}, preto musíme
dokázať nasledujúce implikácie.

r ∧ b ⇒ f [y3/a[y1]]

g ⇒ r[y1/y1 + 1, y2/y2 + y3]

Zostávajúcu časť P22 tvorí riadiaca štruktúra if neobsahujúca vetvu else.
Pre tento účel sa používa upravené pravidlo alternatívy, tzv. pravidlo
pol alternatívy.

{f ∧ c} P221 {g} (f ∧ ¬c ⇒ g)

{f } if c then P221 fi {g}

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

33

Nakoniec axiómou priradenia aplikovanou na časť P221 dostávame posled-
nú implikáciu.

f ∧ c ⇒ g[y3/ − y3]

Pre dokázanie čiastočnej správnosti programu P je teda nutné sformulovať
podmienky r, s, f a g v nasledujúcich implikáciach a tieto implikácie dokázať.

p ⇒ r[y1/1, y2/0, y3/0]

s ⇒ q[z/y2]

r ∧ ¬b ⇒ s

r ∧ b ⇒ f [y3/a[y1]]

g ⇒ r[y1/y1 + 1, y2/y2 + y3]

f ∧ ¬c ⇒ g

f ∧ c ⇒ g[y3/ − y3]

Po sformulovaní podmienok r, s, f a g a následnom dokázaní všetkých uve-
dených implikácií je čiastočná správnosť programu P vzhľadom na vstup-
nú podmienku p a výstupnú podmienku q dokázaná. Kompletný dôkaz je
prenechaný ako cvičenie pre čitateľa.

2.2

Rozširovanie Hoareovských kalkulov

Príklad 29 Sformulujte inferenčné pravidlo Hoareovského kalkulu pre ria-
diacu štruktúru repeat definovanú nasledujúcim vzťahom.

(repeat S until b) ≡ (S; while ¬b do S od)

Dokážte, že navrhnuté inferenčné pravidlo je zdravé.

Riešenie 29 Riadiaca štruktúra repeat, dobre známa napríklad z progra-
movacieho jazyka Pascal, sa dá jednoducho prepísať pomocou riadiacej štruk-
túry while tak, ako je to zobrazené v zadaní úlohy.

{p} S; while ¬b do S od {q}

{p} repeat S until b {q}

(1)
(2)

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

34

Ak dokážeme tvrdenie (1), budeme mať dokázané aj tvrdenie (2). Obdobný
postup budeme aplikovať aj v ďalších odvodzovaniach rozširovaní Hoare-
ovských kalkulov za pomoci štyroch inferenčných pravidiel.

Tvrdenie (1) sa skladá z dvoch častí. Použijeme pravidlo kompozície.

{p} S {r}

{r} while ¬b do S od {q}

{p} S; while ¬b do S od {q}

Pre cyklus while existuje pravidlo iterácie. Pravidlo však vyžaduje výstupnú
podmienku v konkrétnom tvare. Na dosiahnutie žiadaného tvaru použijeme
pravidlo následku.

{r} while ¬b do S od {r ∧ b}

(r ∧ b ⇒ q)

{r} while ¬b do S od {q}

Teraz je už možné použiť zmieňované pravidlo iterácie pre cyklus while.

{r ∧ ¬b} S {r}

{r} while ¬b do S od {r ∧ b}

Nakoniec sformulujeme inferenčné pravidlo pre riadiacu štruktúru repeat.

{p} S {r}

{r ∧ ¬b} S {r}

(r ∧ b ⇒ q)

{p} repeat S until b {q}

Výsledné inferenčné pravidlo je zdravé, pretože pri jeho odvodzovaní sme
používali už existujúce inferenčné pravidlá Hoareovského dokazovacieho sys-
tému, ktoré sú zdravé.

Príklad 30 Navrhnite inferenčné pravidlo Hoareovho dokazovacieho systé-
mu pre riadiacu štruktúru reprezentujúcu tzv. jeden a pol cyklus.

do

S1;
exit when b;
S2

od

resp.

(loop S1; when b exit; S2 pool) ≡ (S1; while ¬b do S2; S1 od)

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

35

Riešenie 30 Podobne ako v predchádzajúcom príklade budeme používať už
existujúce inferenčné pravidlá Hoareovského kalkulu pre dokázanie žiadaného
tvrdenia.

{p} S1; while ¬b do S2; S1 od {q}

{p} loop S1; when b exit; S2 pool {q}

• pravidlo kompozície

{p} S1 {r} {r} while ¬b do S2; S1 od {q}

{p} S1; while ¬b do S2; S1 od {q}

• pravidlo následku

{r} while ¬b do S2; S1 od {r ∧ b} (r ∧ b ⇒ q)

{r} while ¬b do S2; S1 od {q}

• pravidlo iterácie

{r ∧ ¬b} S2; S1 {r}

{r} while ¬b do S2; S1 od {r ∧ b}

• pravidlo kompozície

{r ∧ ¬b} S2 {s} {s} S1 {r}

{r ∧ ¬b} S2; S1 {r}

Na záver sformulujeme výsledné inferenčné pravidlo.

{p} S1 {r} {r ∧ ¬b} S2 {s} {s} S1 {r} (r ∧ b ⇒ q)

{p} loop S1; when b exit; S2 pool {q}

Príklad 31 Sformulujte inferenčné pravidlo Hoareovského kalkulu pre prog-
ramovú konštrukciu PK.

PK : while c do S od;

while b do

S;
while c do S od;

od

KAPITOLA 2. SPRÁVNOSŤ PROGRAMOV

36

Riešenie 31 Inferenčné pravidlo pre programovú konštrukciu PK vyzerá
nasledovne. Podrobné odvodenie je prenechané ako cvičenie pre čitateľa.

{p ∧ c} S {p} {s ∧ b} S {r} {r ∧ c} S {s} (p ∧ ¬c ⇒ s) (r ∧ ¬c ⇒ s) (s ∧ ¬b ⇒ q)

{p} while c do S od; while b do S; while c do S od; od {q}

Príklad 32 Predpokladajme, že platí nasledujúca formula.

{p ∧ (b ∨ c)} S {p}

Dokážte Hoareovou metódou čiastočnú správnosť programovej konštrukcie PK
z predchádzajúceho príkladu vzhľadom na vstupnú podmienku {p} a výstup-
nú podmienku {p ∧ (¬b ∧ ¬c)}.

Riešenie 32 Pre vyriešenie úlohy stačí dokázať nasledujúci vzťah.1

{p ∧ (b ∨ c)} S {p}

{p} PK {p ∧ ¬b ∧ ¬c}

1V skutočnosti je to však dosť zložité. Komplexné riešenie úlohy je vítané a bude

zaradené do Zbierky riešených úloh zo ZTP.

Kapitola 3

Sémantika programov

Príklad 33 Uvažujme hypotetický iteratívny príkaz loop (b, S1, S2) defino-
vaný sémantickou rovnicou

M[[loop (b, S1, S2)]] =

∞

t

0

{φi}

kde

φ0 = λσ · ⊥

φi+1 = λσ · if W[[b]]σ then φi(M[[S1]]σ)

else M[[S2]]σ

Na základe základných príkazov (priradenie, kompozícia, vetvenie a cyklus)
definujte programový segment S taký, že platí

M[[loop (b, S1, S2)]] = M[[S]]

Tvrdenie dokážte.

Riešenie 33 Analýzou sémantickej rovnice v zadaní vieme vytvoriť progra-
mový segment S skladajúci sa z častí S0 a S2.

S : while b do )

S0

S1

od
S2;

Teda pre programový subsegment S0 platí

M[[while b do S1 od]] =

∞

t

0

{ψi}

37

KAPITOLA 3. SÉMANTIKA PROGRAMOV

38

kde

ψ0 = λσ · ⊥

ψi+1 = λσ · if W[[b]]σ then ψi(M[[S1]]σ)

else σ

Keďže M[[S2]]σ

0

potom pre programový segment S platí

M[[S0; S2]]σ = λσ · M[[S2]](M[[S0]]σ)

Našli sme teda programový segment S. Teraz musíme dokázať ekvivalenciu
s iteratívnym príkazom loop (b, S1, S2).

M[[S]] = λσ · M[[S2]](M[[S0]]σ)

= λσ · M[[S2]](M[[while b do S1 od]]σ)
= λσ · M[[S2]](t

∞
0 {ψi}σ)

Čiže musíme dokázať nasledujúce tvrdenie.

M[[S2]](

∞

t

0

{ψi}) =

∞

t

0

{φi}

Rovnosť rozložíme na dva možné prípady.

1. Nech

t∞

0 {φi} =⊥. To znamená, že ∀φi =⊥. Potom M[[S2]](t

∞
0 {ψi}) =⊥.

Kedy bude φi ⊥? Ak i = 0 alebo ∀i > 0 : W[[b]]σ = true. Rovnako to
platí aj pri ψ. Takže M[[S2]] ⊥=⊥.

2. Nech

t∞

0 {φi} 6=⊥. Potom i 6= 0 resp. i > 0. Určite ∃k : k < i také, že

k-krát bolo W[[b]] true a na k + 1 bolo f alse. Teda

t∞

0

bola M[[S2]]σ.

Pozrieme sa na ψ. Vieme, že k-krát bude true, potom f alse. Vykonal
sa teda rovnaký kód ako pri φ.

t∞

0 {ψi} bola σ. Takže t

∞
0

ľavej strany

priradenia je M[[S2]]σ.

Literatúra

[1] Igor Prívara, Základy teórie programovania, Fakulta matematiky,

fyziky a informatiky UK, Bratislava

39