' $'
&
$
%Petr Hliněný, FI MU Brno 1 IB000 "Úv. Inf.": Dokazování programů
8 Dokazování vlastností programů8 Dokazování vlastností programů
Jak jste asi již poznali, umění programovat není zdaleka jen o tom naučit se syntaxi
programovacího jazyka, ale především o schopnosti vytvářet a správně formálně zapi-
sovat algoritmy. Přitom situace, kdy programátorem zapsaný algoritmus počítá něco
trochu jiného, než si programátor představuje, je určitě nejčastější programátorskou
chybou, o to zákeřnější, že ji žádný ,,chytrý překladač nemůže odhalit.
' $'
&
$
%Petr Hliněný, FI MU Brno 1 IB000 "Úv. Inf.": Dokazování programů
8 Dokazování vlastností programů8 Dokazování vlastností programů
Jak jste asi již poznali, umění programovat není zdaleka jen o tom naučit se syntaxi
programovacího jazyka, ale především o schopnosti vytvářet a správně formálně zapi-
sovat algoritmy. Přitom situace, kdy programátorem zapsaný algoritmus počítá něco
trochu jiného, než si programátor představuje, je určitě nejčastější programátorskou
chybou, o to zákeřnější, že ji žádný ,,chytrý překladač nemůže odhalit.
Proto již na počátku (seriózního) studia informatiky je dobré klást důraz na správné
chápání zápisu algoritmů i na důkazy jejich vlastností a správnosti.
' $'
&
$
%Petr Hliněný, FI MU Brno 1 IB000 "Úv. Inf.": Dokazování programů
8 Dokazování vlastností programů8 Dokazování vlastností programů
Jak jste asi již poznali, umění programovat není zdaleka jen o tom naučit se syntaxi
programovacího jazyka, ale především o schopnosti vytvářet a správně formálně zapi-
sovat algoritmy. Přitom situace, kdy programátorem zapsaný algoritmus počítá něco
trochu jiného, než si programátor představuje, je určitě nejčastější programátorskou
chybou, o to zákeřnější, že ji žádný ,,chytrý překladač nemůže odhalit.
Proto již na počátku (seriózního) studia informatiky je dobré klást důraz na správné
chápání zápisu algoritmů i na důkazy jejich vlastností a správnosti.
Stručný přehled lekce
* Jakými postupy ověřovat, že počítačový program ,,správně funguje ?
* Použití matematické indukce k dokazování vlastností algoritmů.
* Několik konkrétních algoritmů a jejich důkazů.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Dokazování programů
8.1 O ,,správnosti programů8.1 O ,,správnosti programů
Jak se máme přesvědčit, že je daný program ,,správný ?
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Dokazování programů
8.1 O ,,správnosti programů8.1 O ,,správnosti programů
Jak se máme přesvědčit, že je daný program ,,správný ?
ˇ Co třeba ladění programů?
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Dokazování programů
8.1 O ,,správnosti programů8.1 O ,,správnosti programů
Jak se máme přesvědčit, že je daný program ,,správný ?
ˇ Co třeba ladění programů?
Jelikož počet možných vstupních hodnot je (v principu) neohraničený, nelze
otestovat všechna možná vstupní data.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Dokazování programů
8.1 O ,,správnosti programů8.1 O ,,správnosti programů
Jak se máme přesvědčit, že je daný program ,,správný ?
ˇ Co třeba ladění programů?
Jelikož počet možných vstupních hodnot je (v principu) neohraničený, nelze
otestovat všechna možná vstupní data.
ˇ Situace je zvláště komplikovaná v případě paralelních, randomizovaných,
interaktivních a nekončících programů (operační systémy, systémy řízení
provozu apod.). Takové systémy mají nedeterministické chování a opako-
vané experimenty tudíž vedou k různým výsledkům. (Nelze je rozumně ladit,
respektive ladění poskytne jen velmi nedostatečnou záruku správného za ji-
ných okolností chování.)
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Dokazování programů
8.1 O ,,správnosti programů8.1 O ,,správnosti programů
Jak se máme přesvědčit, že je daný program ,,správný ?
ˇ Co třeba ladění programů?
Jelikož počet možných vstupních hodnot je (v principu) neohraničený, nelze
otestovat všechna možná vstupní data.
ˇ Situace je zvláště komplikovaná v případě paralelních, randomizovaných,
interaktivních a nekončících programů (operační systémy, systémy řízení
provozu apod.). Takové systémy mají nedeterministické chování a opako-
vané experimenty tudíž vedou k různým výsledkům. (Nelze je rozumně ladit,
respektive ladění poskytne jen velmi nedostatečnou záruku správného za ji-
ných okolností chování.)
ˇ V některých případech je však třeba mít naprostou jistotu, že program
funguje tak jak má, případně že splňuje základní bezpečnostní požadavky.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Dokazování programů
8.1 O ,,správnosti programů8.1 O ,,správnosti programů
Jak se máme přesvědčit, že je daný program ,,správný ?
ˇ Co třeba ladění programů?
Jelikož počet možných vstupních hodnot je (v principu) neohraničený, nelze
otestovat všechna možná vstupní data.
ˇ Situace je zvláště komplikovaná v případě paralelních, randomizovaných,
interaktivních a nekončících programů (operační systémy, systémy řízení
provozu apod.). Takové systémy mají nedeterministické chování a opako-
vané experimenty tudíž vedou k různým výsledkům. (Nelze je rozumně ladit,
respektive ladění poskytne jen velmi nedostatečnou záruku správného za ji-
ných okolností chování.)
ˇ V některých případech je však třeba mít naprostou jistotu, že program
funguje tak jak má, případně že splňuje základní bezpečnostní požadavky.
Narůstající složitost programových systémů a zvýšené požadavky na jejich
bezpečnost si vynucují vývoj ,,spolehlivých formálních verifikačních metod.
' $'
&
$
%Petr Hliněný, FI MU Brno 3 IB000 "Úv. Inf.": Dokazování programů
Připomenutí našeho formálního popisu algoritmů
ˇ Proměnné nebudeme deklarovat ani typovat, pole odlišíme závorkami p[].
ˇ Přiřazení hodnoty zapisujeme a  b, případně a:=b, ale nikdy ne a=b.
ˇ Jako elem. operace je možné použít jakékoliv aritmetické výrazy v běžném
matematickém zápise. Rozsahem a přesností čísel se zde nezabýváme.
ˇ Podmíněné větvení uvedeme klíčovými slovy if ... then ... else ...
fi , kde else větev lze vynechat (a někdy, na jednom řádku, i fi).
ˇ Pevný cyklus uvedeme klíčovými slovy for ... do ... done , kde část
za for musí obsahovat předem danou konečnou množinu hodnot pro při-
řazování do řídící proměnné.
ˇ Podmíněný cyklus uvedeme klíčovými slovy while ... do ... done .
Zde se může za while vyskytovat jakákoliv logická podmínka.
ˇ V zápise používáme jasné odsazování (zleva) podle úrovně zanoření řídících
struktur (což jsou if, for, while).
ˇ Pokud je to dostatečně jasné, elementární operace nebo podmínky můžeme
i ve formálním zápise popsat běžným jazykem.
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Dokazování programů
8.2 Jednoduché indukční dokazování8.2 Jednoduché indukční dokazování
Příklad 8.1. Zjistěte, kolik znaků 'x' v závislosti na celočíselné hodnotě n
vstupního parametru n vypíše následující algoritmus.
Algoritmus 8.2.
for i  1,2,3,...,n-1,n do
for j  1,2,3,...,i-1,i do
vytiskni 'x';
done
done
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Dokazování programů
8.2 Jednoduché indukční dokazování8.2 Jednoduché indukční dokazování
Příklad 8.1. Zjistěte, kolik znaků 'x' v závislosti na celočíselné hodnotě n
vstupního parametru n vypíše následující algoritmus.
Algoritmus 8.2.
for i  1,2,3,...,n-1,n do
for j  1,2,3,...,i-1,i do
vytiskni 'x';
done
done
Nejprve si uvědomíme, že druhý (vnořený) cyklus vždy vytiskne celkem i znaků
'x'. Proto iterací prvního cyklu (nejspíše) dostaneme postupně 1 + 2 + . . . + n
znaků 'x' na výstupu, což již víme (Příklad 2.6), že je celkem 1
2 n(n + 1).
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Dokazování programů
8.2 Jednoduché indukční dokazování8.2 Jednoduché indukční dokazování
Příklad 8.1. Zjistěte, kolik znaků 'x' v závislosti na celočíselné hodnotě n
vstupního parametru n vypíše následující algoritmus.
Algoritmus 8.2.
for i  1,2,3,...,n-1,n do
for j  1,2,3,...,i-1,i do
vytiskni 'x';
done
done
Nejprve si uvědomíme, že druhý (vnořený) cyklus vždy vytiskne celkem i znaků
'x'. Proto iterací prvního cyklu (nejspíše) dostaneme postupně 1 + 2 + . . . + n
znaků 'x' na výstupu, což již víme (Příklad 2.6), že je celkem 1
2 n(n + 1).
Budeme tedy dokazovat následující tvrzení:
Věta. Pro každé přir. n Algoritmus 8.2 vypíše právě 1
2 n(n+1) znaků 'x'.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.2.
for i  1,2,3,...,n-1,n do
for j  1,2,3,...,i-1,i do
vytiskni 'x';
done
done
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.2.
for i  1,2,3,...,n-1,n do
for j  1,2,3,...,i-1,i do
vytiskni 'x';
done
done
Věta. Pro každé přir. n Algoritmus 8.2 vypíše právě 1
2 n(n + 1) znaků 'x'.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.2.
for i  1,2,3,...,n-1,n do
for j  1,2,3,...,i-1,i do
vytiskni 'x';
done
done
Věta. Pro každé přir. n Algoritmus 8.2 vypíše právě 1
2 n(n + 1) znaků 'x'.
Důkaz: Postupujeme indukcí podle n. Báze pro n = 0 je zřejmá, neprovede se
ani jedna iterace cyklu a tudíž bude vytištěno 0 znaků 'x', což máme dokázat.
Nechť tedy tvrzení platí pro jakékoliv n0 a položme n = n0 + 1. Prvních n0
iterací vnějšího cyklu podle indukčního předpokladu vypíše (ve vnitřním cyklu)
celkem 1
2 n0(n0 + 1) znaků 'x'. Pak již následuje jen jedna poslední iterace
vnějšího cyklu s i  n=n0+1 a v ní se vnitřní cyklus j  1,2,...,i=n iteruje
celkem n = n0 + 1 -krát.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.2.
for i  1,2,3,...,n-1,n do
for j  1,2,3,...,i-1,i do
vytiskni 'x';
done
done
Věta. Pro každé přir. n Algoritmus 8.2 vypíše právě 1
2 n(n + 1) znaků 'x'.
Důkaz: Postupujeme indukcí podle n. Báze pro n = 0 je zřejmá, neprovede se
ani jedna iterace cyklu a tudíž bude vytištěno 0 znaků 'x', což máme dokázat.
Nechť tedy tvrzení platí pro jakékoliv n0 a položme n = n0 + 1. Prvních n0
iterací vnějšího cyklu podle indukčního předpokladu vypíše (ve vnitřním cyklu)
celkem 1
2 n0(n0 + 1) znaků 'x'. Pak již následuje jen jedna poslední iterace
vnějšího cyklu s i  n=n0+1 a v ní se vnitřní cyklus j  1,2,...,i=n iteruje
celkem n = n0 + 1 -krát. Celkem tedy bude vytištěn tento počet znaků 'x':
1
2
n0(n0 + 1) + n0 + 1 =
1
2
(n0 + 1 + 1)(n0 + 1) =
1
2
n(n + 1)
Důkaz indukčního kroku je hotov. 2
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Dokazování programů
Příklad 8.3. Zjistěte, kolik znaků 'z' v závislosti na celočíselné hodnotě n
vstupního parametru n vypíše následující algoritmus.
Algoritmus 8.4.
st  "z";
for i  1,2,3,...,n-1,n do
vytiskni řetězec st;
st  st+st ; (zřetězení dvou kopií st za sebou)
done
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Dokazování programů
Příklad 8.3. Zjistěte, kolik znaků 'z' v závislosti na celočíselné hodnotě n
vstupního parametru n vypíše následující algoritmus.
Algoritmus 8.4.
st  "z";
for i  1,2,3,...,n-1,n do
vytiskni řetězec st;
st  st+st ; (zřetězení dvou kopií st za sebou)
done
Zkusíme-li si výpočet simulovat pro n = 0, 1, 2, 3, 4 . . ., postupně dostaneme
počty 'z' jako 0, 1, 3, 7, 15 . . ..
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Dokazování programů
Příklad 8.3. Zjistěte, kolik znaků 'z' v závislosti na celočíselné hodnotě n
vstupního parametru n vypíše následující algoritmus.
Algoritmus 8.4.
st  "z";
for i  1,2,3,...,n-1,n do
vytiskni řetězec st;
st  st+st ; (zřetězení dvou kopií st za sebou)
done
Zkusíme-li si výpočet simulovat pro n = 0, 1, 2, 3, 4 . . ., postupně dostaneme
počty 'z' jako 0, 1, 3, 7, 15 . . .. Na základě toho již není obtížné ,,uhodnout ,
že počet 'z' bude (asi) obecně určen vztahem 2n - 1. Toto je však třeba
dokázat!
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Dokazování programů
Příklad 8.3. Zjistěte, kolik znaků 'z' v závislosti na celočíselné hodnotě n
vstupního parametru n vypíše následující algoritmus.
Algoritmus 8.4.
st  "z";
for i  1,2,3,...,n-1,n do
vytiskni řetězec st;
st  st+st ; (zřetězení dvou kopií st za sebou)
done
Zkusíme-li si výpočet simulovat pro n = 0, 1, 2, 3, 4 . . ., postupně dostaneme
počty 'z' jako 0, 1, 3, 7, 15 . . .. Na základě toho již není obtížné ,,uhodnout ,
že počet 'z' bude (asi) obecně určen vztahem 2n - 1. Toto je však třeba
dokázat!
Jak záhy zjistíme, matematická indukce na naše tvrzení přímo ,,nezabírá , ale mnohem
lépe se nám povede s následujícím přirozeným zesílením dokazovaného tvrzení:
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.4.
st  "z";
for i  1,2,3,...,n-1,n do
vytiskni řetězec st;
st  st+st ; (zřetězení dvou kopií st za sebou)
done
Věta. Pro každé přirozené n Algoritmus 8.4 vypíše právě 2n -1 znaků 'z'
a proměnná st bude na konci obsahovat řetězec 2n znaků 'z'.
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.4.
st  "z";
for i  1,2,3,...,n-1,n do
vytiskni řetězec st;
st  st+st ; (zřetězení dvou kopií st za sebou)
done
Věta. Pro každé přirozené n Algoritmus 8.4 vypíše právě 2n -1 znaků 'z'
a proměnná st bude na konci obsahovat řetězec 2n znaků 'z'.
Důkaz: Postupujeme indukcí podle n. Báze pro n = 0 je zřejmá, neprovede se
ani jedna iterace cyklu a tudíž bude vytištěno 0 znaků 'z', což máme dokázat.
Nechť tedy tvrzení platí pro jakékoliv n0 a položme n = n0 + 1. Podle indukč-
ního předpokladu po prvních n0 iteracích bude vytištěno 2n0 - 1 znaků 'z' a
proměnná st bude obsahovat řetězec 2n0 znaků 'z'. V poslední iteraci cyklu
(pro i  n=n0+1) vytiskneme dalších 2n0 znaků 'z' (z proměnné st) a dále
řetězec st ,,zdvojnásobíme .
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.4.
st  "z";
for i  1,2,3,...,n-1,n do
vytiskni řetězec st;
st  st+st ; (zřetězení dvou kopií st za sebou)
done
Věta. Pro každé přirozené n Algoritmus 8.4 vypíše právě 2n -1 znaků 'z'
a proměnná st bude na konci obsahovat řetězec 2n znaků 'z'.
Důkaz: Postupujeme indukcí podle n. Báze pro n = 0 je zřejmá, neprovede se
ani jedna iterace cyklu a tudíž bude vytištěno 0 znaků 'z', což máme dokázat.
Nechť tedy tvrzení platí pro jakékoliv n0 a položme n = n0 + 1. Podle indukč-
ního předpokladu po prvních n0 iteracích bude vytištěno 2n0 - 1 znaků 'z' a
proměnná st bude obsahovat řetězec 2n0 znaků 'z'. V poslední iteraci cyklu
(pro i  n=n0+1) vytiskneme dalších 2n0 znaků 'z' (z proměnné st) a dále
řetězec st ,,zdvojnásobíme .
Proto po n iteracích bude vytištěno celkem 2n0 -1+2n0 = 2n0+1 -1 = 2n -1
znaků 'z' a v st bude uloženo 2  2n0 = 2n znaků 'z'. 2
' $'
&
$
%Petr Hliněný, FI MU Brno 8 IB000 "Úv. Inf.": Dokazování programů
8.3 Algoritmy pro relace8.3 Algoritmy pro relace
Relace jsou velice vhodnou strukturou pro algoritmické zpracování.
Algoritmus 8.5. Symetrický uzávěr.
Pro danou relaci R na n-prvkové množině A = {a1, a2, . . . , an} vytvoříme její
symetrický uzávěr

R takto:

R  R ;
for i  1,2,...,n-1,n do
for j  1,2,...,n-1,n do
if (ai, aj)  R  (aj, ai)  R then

R 

R {(aj, ai)} ;
done
done
' $'
&
$
%Petr Hliněný, FI MU Brno 8 IB000 "Úv. Inf.": Dokazování programů
8.3 Algoritmy pro relace8.3 Algoritmy pro relace
Relace jsou velice vhodnou strukturou pro algoritmické zpracování.
Algoritmus 8.5. Symetrický uzávěr.
Pro danou relaci R na n-prvkové množině A = {a1, a2, . . . , an} vytvoříme její
symetrický uzávěr

R takto:

R  R ;
for i  1,2,...,n-1,n do
for j  1,2,...,n-1,n do
if (ai, aj)  R  (aj, ai)  R then

R 

R {(aj, ai)} ;
done
done
Důkaz: Zde není důkaz vůbec obtížný. Relace

R je zřejmě symetrická, neboť
(vnitřní) tělo cyklu pro všechny dvojice (ai, aj)  R přidá i (aj, ai). Z druhé
strany všechny dvojice ,,přidané v

R \R musí být obsaženy podle definice
symetrické relace, takže

R je skutečně symetrickým uzávěrem podle definice
uzávěru relace. 2
' $'
&
$
%Petr Hliněný, FI MU Brno 9 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.6. Tranzitivní uzávěr.
Pro danou relaci R na n-prvkové množině A = {a1, a2, . . . , an} vytvoříme její
tranzitivní uzávěr R+ takto:
R+  R ;
for k  1,2,...,n-1,n do
for i  1,2,...,n-1,n do for j  1,2,...,n-1,n do
if (ai, ak)  R+  (ak, aj)  R+ then
if (ai, aj)  R+ then R+  R+  {(ai, aj)} ;
fi
done
done
' $'
&
$
%Petr Hliněný, FI MU Brno 9 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.6. Tranzitivní uzávěr.
Pro danou relaci R na n-prvkové množině A = {a1, a2, . . . , an} vytvoříme její
tranzitivní uzávěr R+ takto:
R+  R ;
for k  1,2,...,n-1,n do
for i  1,2,...,n-1,n do for j  1,2,...,n-1,n do
if (ai, ak)  R+  (ak, aj)  R+ then
if (ai, aj)  R+ then R+  R+  {(ai, aj)} ;
fi
done
done
Jak by se dala dokázat správnost popsaného algoritmu? Přímá aplikace indukce
podle n nevypadá přínosně. . . (Zkuste si sami!)
' $'
&
$
%Petr Hliněný, FI MU Brno 9 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.6. Tranzitivní uzávěr.
Pro danou relaci R na n-prvkové množině A = {a1, a2, . . . , an} vytvoříme její
tranzitivní uzávěr R+ takto:
R+  R ;
for k  1,2,...,n-1,n do
for i  1,2,...,n-1,n do for j  1,2,...,n-1,n do
if (ai, ak)  R+  (ak, aj)  R+ then
if (ai, aj)  R+ then R+  R+  {(ai, aj)} ;
fi
done
done
Jak by se dala dokázat správnost popsaného algoritmu? Přímá aplikace indukce
podle n nevypadá přínosně. . . (Zkuste si sami!)
Nejkratší cesta k cíli vede použitím indukce (podle proměnné k vnějšího cyklu)
na vhodně zesíleném tvrzení. Pro jeho formulaci si definujeme, že relace S na
A je k-částečně tranzitivní, pokud pro libovolná i, j a pro  k platí, že z
(ai, a ), (a , aj)  S vyplývá (ai, aj)  S.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": Dokazování programů
Věta. Po každých k  0 iteracích vnějšího cyklu Algoritmu 8.6 aktuální
hodnota relace R+ udává k-částečně tranzitivní uzávěr relace R na A.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": Dokazování programů
Věta. Po každých k  0 iteracích vnějšího cyklu Algoritmu 8.6 aktuální
hodnota relace R+ udává k-částečně tranzitivní uzávěr relace R na A.
Důkaz: Báze indukce pro k = 0 jasně platí, neboť věta v tom případě nic neříká.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": Dokazování programů
Věta. Po každých k  0 iteracích vnějšího cyklu Algoritmu 8.6 aktuální
hodnota relace R+ udává k-částečně tranzitivní uzávěr relace R na A.
Důkaz: Báze indukce pro k = 0 jasně platí, neboť věta v tom případě nic neříká.
Předpokládejme nyní, že tvrzení platí pro nějaké k0  0 a dokažme jej i pro
k = k0 +1. Zřejmě stačí uvažovat případ k0 < n. Každá dvojice (ai, aj) přidaná
do R+ uvnitř cyklu musí náležet do k-částečně tranzitivního uzávěru podle
definice. Zbývá zdůvodnit, proč každá dvojice (ai, aj) náležející do k-částečně
tranzitivního uzávěru, ale ne do k0-částečně tranzitivního uzávěru, bude do R+
v k-té iteraci přidána.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": Dokazování programů
Věta. Po každých k  0 iteracích vnějšího cyklu Algoritmu 8.6 aktuální
hodnota relace R+ udává k-částečně tranzitivní uzávěr relace R na A.
Důkaz: Báze indukce pro k = 0 jasně platí, neboť věta v tom případě nic neříká.
Předpokládejme nyní, že tvrzení platí pro nějaké k0  0 a dokažme jej i pro
k = k0 +1. Zřejmě stačí uvažovat případ k0 < n. Každá dvojice (ai, aj) přidaná
do R+ uvnitř cyklu musí náležet do k-částečně tranzitivního uzávěru podle
definice. Zbývá zdůvodnit, proč každá dvojice (ai, aj) náležející do k-částečně
tranzitivního uzávěru, ale ne do k0-částečně tranzitivního uzávěru, bude do R+
v k-té iteraci přidána.
Není těžké ověřit, že (ai, aj) náleží do k-částečně tranzitivního uzávěru, právě
když v relaci R nalezneme takovou cestu ,,po šipkách z ai do aj, která přechází
pouze přes prvky a kde  k. V naší situaci vyplývá, že taková cesta musí
použít i prvek ak (jen jednou!), a proto (ai, ak) i (ak, aj) náleží do k0-částečně
tranzitivního uzávěru R. V k-té iteraci tudíž bude příslušná if podmínka splněná
a (ai, aj) bude přidána do R+. 2
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Dokazování programů
Dokazování konečnosti algoritmu
Všimněte si, že jsme se zatím v důkazech vůbec nezamýšleli nad tím, zda náš algorit-
mus vůbec skončí. (To jistě není samozřejmé a důkaz konečnosti je nutno v obecnosti
podávat!)
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Dokazování programů
Dokazování konečnosti algoritmu
Všimněte si, že jsme se zatím v důkazech vůbec nezamýšleli nad tím, zda náš algorit-
mus vůbec skončí. (To jistě není samozřejmé a důkaz konečnosti je nutno v obecnosti
podávat!)
Prozatím jsme však ukazovali algoritmy využívající jen for cykly, přitom podle naší
konvence obsahuje for cyklus předem danou konečnou množinu hodnot pro řídící pro-
měnnou, neboli náš for cyklus vždy musí skončit. Ale už v příštím algoritmu využijeme
while cyklus, u kterého vůbec není jasné kdy a jestli skončí, a tudíž bude potřebný i
důkaz konečnosti.
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Dokazování programů
Dokazování konečnosti algoritmu
Všimněte si, že jsme se zatím v důkazech vůbec nezamýšleli nad tím, zda náš algorit-
mus vůbec skončí. (To jistě není samozřejmé a důkaz konečnosti je nutno v obecnosti
podávat!)
Prozatím jsme však ukazovali algoritmy využívající jen for cykly, přitom podle naší
konvence obsahuje for cyklus předem danou konečnou množinu hodnot pro řídící pro-
měnnou, neboli náš for cyklus vždy musí skončit. Ale už v příštím algoritmu využijeme
while cyklus, u kterého vůbec není jasné kdy a jestli skončí, a tudíž bude potřebný i
důkaz konečnosti.
Metoda 8.7. Důkaz konečnosti.
Máme-li za úkol dokázat, že algoritmus skončí, postupujeme nejlépe následovně:
ˇ Sledujeme zvolený celočíselný a zdola ohraničený parametr algoritmu
(třeba přirozené číslo) a dokážeme, že se jeho hodnota v průběhu algo-
ritmu neustále ostře zmenšuje.
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Dokazování programů
Dokazování konečnosti algoritmu
Všimněte si, že jsme se zatím v důkazech vůbec nezamýšleli nad tím, zda náš algorit-
mus vůbec skončí. (To jistě není samozřejmé a důkaz konečnosti je nutno v obecnosti
podávat!)
Prozatím jsme však ukazovali algoritmy využívající jen for cykly, přitom podle naší
konvence obsahuje for cyklus předem danou konečnou množinu hodnot pro řídící pro-
měnnou, neboli náš for cyklus vždy musí skončit. Ale už v příštím algoritmu využijeme
while cyklus, u kterého vůbec není jasné kdy a jestli skončí, a tudíž bude potřebný i
důkaz konečnosti.
Metoda 8.7. Důkaz konečnosti.
Máme-li za úkol dokázat, že algoritmus skončí, postupujeme nejlépe následovně:
ˇ Sledujeme zvolený celočíselný a zdola ohraničený parametr algoritmu
(třeba přirozené číslo) a dokážeme, že se jeho hodnota v průběhu algo-
ritmu neustále ostře zmenšuje.
ˇ Případně předchozí přístup rozšíříme na zvolenou k-tici přirozených para-
metrů a dokážeme, že se jejich hodnoty v průběhu algoritmu lexikograficky
ostře zmenšují.
Pozor, naše ,,parametry vůbec nemusejí být proměnnými v programu.
' $'
&
$
%Petr Hliněný, FI MU Brno 12 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.8. Cykly permutace.
Pro danou permutaci  na n-prvkové neprázdné množině A = {1, 2, . . . , n}
vypíšeme její cykly (viz Oddíl 6.4) takto:
U  {1, 2, . . . , n};
while U=  do
x  min(U); (nejmenší prvek množiny)
začínáme výpis cyklu ' ' ;
while xU do
vytiskneme x;
U  U\{x} ; x  (x) ;
done
ukončíme výpis cyklu ' ' ;
done
Jak dokážeme správnost tohoto algoritmu?
' $'
&
$
%Petr Hliněný, FI MU Brno 12 IB000 "Úv. Inf.": Dokazování programů
Algoritmus 8.8. Cykly permutace.
Pro danou permutaci  na n-prvkové neprázdné množině A = {1, 2, . . . , n}
vypíšeme její cykly (viz Oddíl 6.4) takto:
U  {1, 2, . . . , n};
while U=  do
x  min(U); (nejmenší prvek množiny)
začínáme výpis cyklu ' ' ;
while xU do
vytiskneme x;
U  U\{x} ; x  (x) ;
done
ukončíme výpis cyklu ' ' ;
done
Jak dokážeme správnost tohoto algoritmu?
Opět platí, že přímá aplikace indukce podle n nepřinese nic podstatného. Důkaz
si tentokrát rozdělíme na dvě části (podle dvou while cyklů). Všimněte se navíc,
že tentokrát je nezbytnou součástí důkazu správnosti algoritmu i důkaz, že oba
while cykly vždy skončí.
' $'
&
$
%Petr Hliněný, FI MU Brno 13 IB000 "Úv. Inf.": Dokazování programů
while U=  do
........
done
Věta. Za předp., že vnitřní while cyklus pro jakoukoliv poč. volbu x skončí,
vypíše cyklus permutace  obsahující x a odebere všechny prvky tohoto
cyklu z množiny U, Algoritmus 8.8 vždy skončí se správným výsledkem.
' $'
&
$
%Petr Hliněný, FI MU Brno 13 IB000 "Úv. Inf.": Dokazování programů
while U=  do
........
done
Věta. Za předp., že vnitřní while cyklus pro jakoukoliv poč. volbu x skončí,
vypíše cyklus permutace  obsahující x a odebere všechny prvky tohoto
cyklu z množiny U, Algoritmus 8.8 vždy skončí se správným výsledkem.
Důkaz: Postupujeme indukcí podle počtu cyklů v permutaci . Jediný cyklus v
 (báze indukce) je vypsán dle předpokladu věty a množina U zůstane prázdná,
tudíž vnější while cyklus skončí po první iteraci a výsledek je správný.
' $'
&
$
%Petr Hliněný, FI MU Brno 13 IB000 "Úv. Inf.": Dokazování programů
while U=  do
........
done
Věta. Za předp., že vnitřní while cyklus pro jakoukoliv poč. volbu x skončí,
vypíše cyklus permutace  obsahující x a odebere všechny prvky tohoto
cyklu z množiny U, Algoritmus 8.8 vždy skončí se správným výsledkem.
Důkaz: Postupujeme indukcí podle počtu cyklů v permutaci . Jediný cyklus v
 (báze indukce) je vypsán dle předpokladu věty a množina U zůstane prázdná,
tudíž vnější while cyklus skončí po první iteraci a výsledek je správný.
Podlě Věty 6.5 se každá permutace dá zapsat jako složení disjunktních cyklů.
Nechť  je tedy složena z > 1 cyklů. Po první iteraci while cyklu zbude
v restrikci permutace  na množinu U celkem - 1 cyklů. Podle indukčního
předpokladu pak tyto zbylé cykly budou správně vypsány a algoritmus skončí.
2
Vidíte, že v tomto důkaze indukcí je indukční krok zcela triviální a důležitý je zde
především základ indukce?
' $'
&
$
%Petr Hliněný, FI MU Brno 14 IB000 "Úv. Inf.": Dokazování programů
while xU do
vytiskneme x;
U  U\{x} ; x  (x) ;
done
Věta. Pokud  je permutace, tak vnitřní while cyklus vždy skončí a
nalezne v  cyklus obsahující libovolný počáteční prvek x  U. Navíc
všechny prvky nalezeného cyklu odebere z množiny U.
' $'
&
$
%Petr Hliněný, FI MU Brno 14 IB000 "Úv. Inf.": Dokazování programů
while xU do
vytiskneme x;
U  U\{x} ; x  (x) ;
done
Věta. Pokud  je permutace, tak vnitřní while cyklus vždy skončí a
nalezne v  cyklus obsahující libovolný počáteční prvek x  U. Navíc
všechny prvky nalezeného cyklu odebere z množiny U.
Důkaz: Zde přímo zopakujeme argument důkazu Věty 6.5: Vezmeme libovolný
prvek x = x1  A a iterujeme zobrazení xi+1 = (xi) pro i = 1, 2 . . ., až dojde
ke zopakování prvku xk = xj pro nejmenší k > j  1. (To musí nastat, neboť
A je konečná.) Jelikož prvek xj byl již odebrán z U, v kroku x = xk dojde k
ukončení našeho while cyklu. Nadto je  prostá, a proto nemůže nastat j > 1,
neboli xk = (xk-1) = xj = (xj-1) při xk-1 = xj-1. Takže skutečně byl
nalezen a odebrán z U cyklus x1, . . . , xk-1 a důkaz je hotov. 2
' $'
&
$
%Petr Hliněný, FI MU Brno 15 IB000 "Úv. Inf.": Dokazování programů
8.4 Zajímavé algoritmy aritmetiky8.4 Zajímavé algoritmy aritmetiky
Například umocňování na velmi vysoké exponenty je základem známé RSA šifry:
Algoritmus 8.9. Binární postup umocňování.
Pro daná číslo a, b vypočteme jejich celočíselnou mocninu (omezenou na zbyt-
kové třídy modulo m kvůli prevenci přetečení rozsahu celých čísel v počítači),
tj. c = ab mod m.
c  1;
while b > 0 do
if b mod 2 > 0 then c  (ca) mod m ;
b  b/2 ; a  (aa) mod m ;
done
výsledek c ;
' $'
&
$
%Petr Hliněný, FI MU Brno 15 IB000 "Úv. Inf.": Dokazování programů
8.4 Zajímavé algoritmy aritmetiky8.4 Zajímavé algoritmy aritmetiky
Například umocňování na velmi vysoké exponenty je základem známé RSA šifry:
Algoritmus 8.9. Binární postup umocňování.
Pro daná číslo a, b vypočteme jejich celočíselnou mocninu (omezenou na zbyt-
kové třídy modulo m kvůli prevenci přetečení rozsahu celých čísel v počítači),
tj. c = ab mod m.
c  1;
while b > 0 do
if b mod 2 > 0 then c  (ca) mod m ;
b  b/2 ; a  (aa) mod m ;
done
výsledek c ;
Zde použijeme k důkazu správnosti algoritmu indukci podle délky binárního
zápisu čísla b.
Věta. Algoritmus 8.9 skončí a vždy správně vypočte hodnotu mocniny
c = ab mod m.
' $'
&
$
%Petr Hliněný, FI MU Brno 16 IB000 "Úv. Inf.": Dokazování programů
c  1;
while b > 0 do
if b mod 2 > 0 then c  (ca) mod m ;
b  b/2 ; a  (aa) mod m ;
done
výsledek c ;
Důkaz: Báze indukce je pro = 1, kdy b = 0 nebo b = 1. Přitom pro b = 0
se cyklus vůbec nevykoná a výsledek je c = 1. Pro b = 1 se vykoná jen jedna
iterace cyklu a výsledek je c = a mod m.
' $'
&
$
%Petr Hliněný, FI MU Brno 16 IB000 "Úv. Inf.": Dokazování programů
c  1;
while b > 0 do
if b mod 2 > 0 then c  (ca) mod m ;
b  b/2 ; a  (aa) mod m ;
done
výsledek c ;
Důkaz: Báze indukce je pro = 1, kdy b = 0 nebo b = 1. Přitom pro b = 0
se cyklus vůbec nevykoná a výsledek je c = 1. Pro b = 1 se vykoná jen jedna
iterace cyklu a výsledek je c = a mod m.
Nechť tvrzení platí pro 0  1 a uvažme = 0 + 1. Pak zřejmě b  2 a
vykonají se alespoň dvě iterace cyklu. Po první iteraci bude a = a2, b = b/2
a c = (ab mod 2) mod m. Tudíž délka binárního zápisu b bude jen 0 a podle
indukčního předpokladu zbylé iterace algoritmu skončí s výsledkem
c = c  a b
mod m = (ab mod 2
 a2 b/2
) mod m = ab
mod m .
2
' $'
&
$
%Petr Hliněný, FI MU Brno 17 IB000 "Úv. Inf.": Dokazování programů
Na závěr lekce si ukážeme jeden netradiční krátký algoritmus a jeho analýzu a
důkaz ponecháme zde otevřené. Dokážete popsat, na čem je algoritmus založen?
Algoritmus 8.10. Celočíselná odmocnina.
Pro dané číslo x vypočteme dolní celou část jeho odmocniny r =

x .
p  x; r  0;
while p > 0 do
while (r + p)2 < x do r  r+p ;
p  p/2 ;
done
výsledek r ;
' $'
&
$
%Petr Hliněný, FI MU Brno 17 IB000 "Úv. Inf.": Dokazování programů
Na závěr lekce si ukážeme jeden netradiční krátký algoritmus a jeho analýzu a
důkaz ponecháme zde otevřené. Dokážete popsat, na čem je algoritmus založen?
Algoritmus 8.10. Celočíselná odmocnina.
Pro dané číslo x vypočteme dolní celou část jeho odmocniny r =

x .
p  x; r  0;
while p > 0 do
while (r + p)2 < x do r  r+p ;
p  p/2 ;
done
výsledek r ;