8   Dokazování vlastností algoritmů
Jak jste asi jiz poznali, umění programovat není zdaleka jen o tom naučit se syntaxi programovacího jazyka, ale předevsím o schopnosti vytvaret a spravne formaine zapisovat algoritmy. Přitom situace, kdy programatorem zapsaný algoritmus počíta neco trochu jineho, nez si programátor predstavuje, je urcite nejcastejsí programatorskou chybou, o to zakernejsí, zeji zadny „chytry" prekladac nemuze odhalit.
Proto jiz na pocatku (seriozního) studia informatiky je dobre klíst duraz na spravne chípíní zapisu algoritmu i na dukazy jejich vlastností a spevnosti. c
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í algoritmU.
* Nekolik konkretních algoritmu a jejich dukazu.
Petr Hliněný,  FI MU Brno _ Dokazování algoritmů
8.1   O „správnosti" programů
Jak se máme přesvědčit, zeje daný program „správný"?c
• Co třeba ladení programů? c
Jelikož počet možných vstupních hodnot je (v principů) neohraničený, nelze otestovat vsechna možná vstupní data.c
• Situace je zvláste komplikovaný v případe paralelních, randomizovaných, interaktivních a nekoncících programů (operacní sýstemý, sýstemý řízení provozů apod.). Takove sýstemý maji nedeterministicke chovaní a opakovane experimentý tůdíz vedoů k různým výsledkům. (Nelze je rozůmne ladit, respektive ladřen i poskýtne jen velmi nedostateřcnoů zarůků spravneho chovaní za jiných okolností.)c
• V nekterých případech je vsak třeba mít naprostoů jistotů, ze program fůngůje tak jak ma, prípadne ze splnůje zakladní bezpecnostní pozadavký.c Narůstající slozitost programových sýstemů a zvýsene pozadavký na jejich bezpecnost si výnůcůjí vývoj „spolehlivých" formalních verifikacních metod.
Petr Hliněný,  FI MU Brno___FI: IB000: Dokazování algoritn
Připomenutí našeho formálního popisu algoritmů
• Proměnné nebudeme deklarovat ani typovat, pole odlišíme závorkami p[].
• Přiřazeni hodnoty zapisujeme a — b, připadne a:=b, ale nikdy ne a=b.
• Jako elem. operace je moZne pouZ it jakekoliv aritmetické výrazy v beZnem matematickem zapise. Rozsahem a přesnost i C išel se zde nezabývame.
• Podm inene větveni uvedeme kl iCovymi slovy if ... then . . . else . . . fi , kde else vetev lze vynechat (a nekdy, na jednom radku, i fi).
• Pevny cyklus uvedeme kl íCovymi slovy foreach ... do ... done , kde čast za foreach musi obsahovat předem danou koneCnou mnozinu hodnot pro přičazovan í do řídíc i promenne.
• Podmíněný cyklus uvedeme kl icovymi slovy while ... do ... done. Zde se muze za while vyskytovat jakakoliv logicka podm inka.
• V zapise pouz ivame jasne odsazovan i (zleva) podle urovne zanořen ičid icích struktur (coz jsou if, foreach, while).
• Pokud je to dostatecne jasne, elementarn i operace nebo podm inky muzeme i ve formaln ím zapise popsat beznym jazykem.
Petr Hliněný,  FI MU Brno___FI: IB000: Dokazování algoritmů
8.2   Jednoduché indukční dokazování
Příklad 8.1. Zjistěte, kolik znaků 'x' v závislosti na celočíselné hodnote n vstupního parametrů n vypěe následující algoritmus.
Algoritmus 8.2.
foreach   i—1,2,3,...,n-1,n do
foreach   j — 1,2,3,...,i-1,i do vytiskni 'x';
done done □
Nejprve si uvědomíme, že druhý (vnořený) cyklus vzdy vytiskne celkem i znakU
'x'. Proto iterací prvního cyklu (nejspíše) dostaneme postupne 1 + 2+-----+ n
znaků 'x' na výstupu, což již víme (Příklad 2.7), že je celkem \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ě hn{n + l) znaků 'x'.
Petr Hliněný.  FI MU Brn._I: IB000: Dokazování algoritmů
Algoritmus 8.2.
foreach   i—1,2,3,...,n-1,n do
foreach   j — 1,2,3,...,i-1,i do vytiskni 'x';
done done c
Věta. Pro každé přir. n Algoritmus 8.2 vypíše právě \n(n + 1) znaků 'x'.
DUkaz: Postupujeme indukcí podle n. Baze pro n = 0 je zřejmá, neprovede se ani jedna iterace cyklu a tudíZ bude vytiSteno 0 znakU 'x', coZ máme dokázat.c
Necht tedy tvrzení platí pro jakekoliv no a polozme n = n0 + 1. Prvních n0 iterací vnejSího cyklu podle indukcního predpokladu vypiSe (ve vnitrním cyklu) celkem ^no(no + 1) znaků 'x'. Pak již následuje jen jedna poslední iterace vnejSího cyklu s i — n=n0+1 a v ní se vnitřní cyklus j — 1,2,... ,i=n iteruje celkem n = n0 + 1 -krat.   Celkem tedy bude vytisten tento pocet znaku 'x':
^n0(n0 + 1) + n0 + 1 = ^(n0 + 1 + l)(n0 + 1) = ^n(n + 1)
Dukaz indukcního kroku je hotov.
Petr Hliněný,  FI MU Brno_ FI: IB000: Dokazování algoritn
□
r.
^
Příklad 8.3. Zjistěte, kolik znaků 'z' v závislosti na celočíselné hodnotě n vstupního parametrů n vypíSe následující algoritmus.
Algoritmus 8.4.
foreach   i—1,2,3,...,n-1,n do vytiskni řetezec  st;
st  — st+st ;     (zřetezení dvou kopií st za sebou) done c
Zkusíme-li si výpočet simulovat pro n = 0,1,2,3, 4..., postupne dostaneme
pocty 'z' jako 0,1, 3, 7,15 ... .   Na zaklade toho jiz není obtízne „uhodnout",
ze počet 'z' bude (asi) obecne určen vztahem 2n — 1. Toto je vsak treba
Jak záhy zjistíme, matematická indukce na naše tvrzení přímo „nezabírá", ale mnohem lépe se nam povede s nasleduj íc ím přirozeným zes ílen ím dokazovaneho tvrzen í:
st
z ;
dokazat!
Petr Hliněný,  FI MU Brno
I: IB000: Dokazování algoritmů
Algoritmus 8.4. st  — "z";
foreach   i —1,2,3,...,n-1,n do vytiskni řetězec  st;
st  — st+st ;     (zřetězení dvou kopií st za sebou)
done
Veta. 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 retezec 2n znaků 'z'. c
DUkaz: Postupujeme indukcí podle n. Báze pro n = 0 je zrejmá, neprovede se ani jedna iterace cyklu a tudíž bude vytisteno 0 znaku 'z', coz máme dokázat.c
Necht tedy tvrzení platí pro jakekoliv no a polozme n = no + 1. Podle in-dukcního předpokladu po prvních n0 iteracích bude vytisteno 2no — 1 znaku 'z' a promenná st bude obsahovat retezec 2no znaku 'z'. V poslední iteraci cyklu (pro i — n=n0+l) vytiskneme dalsích 2no znaku 'z' (z promenne st) a dále retezec st „zdvojnásobíme".
Proto po n iteracích bude vytisteno celkem 2no — 1 + 2no = 2no+1 — 1 = 2n — 1 znaku 'z' a v st bude ulozeno 2 • 2no = 2rao+1 = 2n znaku 'z'. D
Petr Hliněný,  FI MU Brno _ Dokazování algoritmů
8.3   Algoritmy pro relace
Relace jsou velice vhodnou strukturou pro algoritmické zpracování. Algoritmus 8.5. Symetricky uzáver.
Pro danou relaci R na n-prvkové množině A = [a\,a2,..., an} vytvoříme její symetrický užévěr R takto:
R — R;
foreach   i — 1,2,...,n-1,n do
foreach   j —1,2,...,n-1,n do
if  (ai,aj) € R A (aj,ai) g. R then R — R U{(aj,ai)} ;
done done c
DUkaz: Zde není dukaz vubec obtíZný. Relace R je zrejme symetrická, nebot (vnitrní) telo cyklu pro vSechny dvojice (ai,aj) € R pridá i (aj,ai). Z druhe
strany vSechny dvojice „přidane" v R \R musí být obsaZeny podle definice
symetricke relace, takZe R je skutecne symetrickým uzíverem podle definice uzíveru relace. □
Petr Hliněný,  FI MU Brno___FI: IB000: Dokazování algoritmů
Algoritmus 8.6. Tranzitivní ůzáver.
Pro danou relaci R na n-prvkové množině A = [a\,a2,..., an} vytvoříme její tranzitivní uzéver R+ takto:
R+  —  R ;
foreach   k — 1,2,...,n-1,n do
foreach   i —1,2,...,n-1,n ; j— 1,2,...,n-1,n do
if (ai,ak) € R+ A (ak, aj) € R+ then
if  (ai,aj) € R+ then R+  —  R+ U{(aj,aj)} ;
fi
done done c
Jak by se dala dokízat sprívnost popsaného algoritmu? Přímí aplikace indukce podle n nevypadí přínosne. .. (Zkuste si sami!)c
Nejkratsí cesta k cíl i vede pouzitím indukce (podle promenne k vnejšího cyklu) na vhodne zesílenem tvrzení. Pro jeho formulaci si definujeme, ze relace S na A je k-Cástečně tranzitivní, pokud pro libovolní i, j a pro l < k platí, ze z
(ai, ai), (ai, aj) € S vyplyví (ai, aj) € S.
Petr Hliněný,  FI MU Brno___FI: IB000: Dokazování algoritmů
Veta. Po kazdych k > 0 iteracích vnejsího cyklu Algoritmu 8.6 aktualn í hodnota relace R+ udava k-castecne tranzitivn í uzaver relace R na A. c
DUkaz: Baze indukce pro k = 0 jasne platí, nebol! veta v tom případe nic neř íka.c
Předpokladejme nyn í, ze tvrzen í platí pro nejake ko > 0 a dokazme jej i pro
k = k0 + 1. Zřejme stac í uvazovat prípad k0 < n. Kazda dvojice (ai, aj) pridana
do R+ uvnitr cyklu musí nalezet do k-castecne tranzitivn ího uzaveru podle definice. Zbyva zduvodnit, proc kazda dvojice (ai,aj) nalezej íc í do k-castecne tranzitivn ího uzaveru, ale ne do k0-castecne tranzitivn ího uzaveru, bude do R+ v k-te iteraci pridana. c
Nen í tezke oveřit, ze (ai,aj) nalez í do k-castecne tranzitivn ího uzaveru, právě
kdyz v relaci R nalezneme takovou cestu „po sipkach" z ai do aj, ktera prechaz í pouze přes prvky ag kde l < k. V nasí situaci vyplyva, ze takova cesta musí
pouz ít i prvek ak (jen jednou!), a proto (ai,ak) i (ak,aj) nalez í do k0-castecne
tranzitivn ího uzaveru R. V k-te iteraci tud íz bude príslusna if podm ínka splnena
a (ai,aj) bude pridana do R+.
□
Petr Hliněný,  FI MU Brno
-1: IB000: Dokazování algoritmů
Dokazování konečnosti algoritmu
Vsimnete si, ze jsme se zatím v dukazech vubec nezamysleli nad tím, zda nas algoritmus vubec skoncí. (To jiste není samozrejme a dukaz konečnosti je nutno v obecnosti podavat!) □
Prozatím jsme vsak ukazovali algoritmy vyuzívající jen foreach cykly, přitom podle nasí konvence obsahuje foreach cyklus predem danou konecnou mnozinu hodnot pro rídící promennou, neboli nas foreach cyklus vzdy musí skoncit. Ale uz v přístím algoritmu vyuzijeme while cyklus, u ktereho vubec není jasne kdy a jestli skoncí, a tudíz bude potrebny i dukaz konecnosti. □
Metoda 8.7. DUkaz konečnosti.
Mame-li za ůkol dokazat, ěe algoritmus skončí, postupujeme nejlepe nasledovne:
• Sledujeme zvoleny celočíselný a zdola ohraničeny parametr algoritmu (těeba pěirozene číslo) a dokaěeme, ěe se jeho hodnota v pruběhu algoritmu neustale ostre zmenšuje. □
• Prípadne pěedčhozí prístup rozěíěíme na zvolenou k-tiči prirozenyčh parametru a dokazeme, ze se jejičh hodnoty v prubehu algoritmu lexiko-grafičky ostěe zmensují
Pozor, naěe „parametry" vubeč nemusejí byt promennymi v programu.
Petr Hliněný.  FI MU Brno__:IB000: Dokazování algorit
mů
Algoritmus 8.8. Cykly permutace.
Pro danou permutaci n na n-prvkove neprazdne množine A = {1, 2,... , n} vypCeme její cykly (viz Oddíl 6.4) takto:
U —  {1,2,...,n}; while   U= 0 do
x — min(U);     (nejmensí prvek množiny)
zacíname vypis cyklu ' {' ;
while   x€U do vytiskneme x;
U — U\{x} ;     x — n (x) ;
done
ukoncíme vypis cyklu ')' ;
done
Jak dokázeme správnost tohoto algoritmu? c
Opet platí, ze přímá aplikace indukce podle n nepřinese nic podstatneho. Dukaz si tentokrát rozdelíme na dve cásti (podle dvou while cyklu). Vsimnete se navíc, ze tentokrát je nezbytnou soucístí dukazu sprívnosti algoritmu i dukaz, ze oba while cykly vzdy skonci.
Petr Hliněný,  FI MU Brno___FI: IB000: Dokazování algoritmů
while   U= 0 do done
Veta. Za předp., ze vnitřní while cýklůs pro jakoůkoliv poc. volbů x skoncí, výp íře cýklůs permůtace n obsahůj ící x a odebere vsechný prvký tohoto cýklů z mnoziný U, Algoritmůs 8.8 vzdý skonc í se spravným výsledkem. c
Důkaz: Postůpůjeme indůkcí podle poctů cýklů v permůtaci n. Jediný cýklůs v n (baze indůkce) je výpsan dle předpokladů vetý a mnozina U zůstane prazdna, tůd íř vnejsí while cýklůs skonc í po prvn í iteraci a výsledek je spravný. c
Podle Vetý 6.5 se kazda permůtace da zapsat jako slozen í disjůnktn ích cýklů. Necht n je tedý slozena z l > 1 cýklů. Po prvn í iteraci while cýklů zbůde v restrikci permůtace n na mnozinů U celkem l — 1 cýklů. Podle indůkcn ího přredpokladů pak týto zbýle cýklý bůdoů spravnře výpsaný a algoritmůs skonřc í.
Vid íte, ze v tomto důkaze indůkc í je indůkcn í krok zcela trivialn í a důlezitý je zde predevsím zaklad indůkce?
□
'etr Hliněný,  FI MU Brno
-1: IB000: Dokazování algoritmů
x  — n (x) ;
done
Veta. Pokud n je permutace, tak vnitřní while cyklus vzdy skoncí a nalezne v n cyklus obsahující libovolny pocatecní prvek x € U. Navíc vsechny prvky nalezeneho cyklu odebere z mnoziny U. c
DUkaz: Zde prímo zopakujeme argument dukazu Vety 6.5: Vezmeme libovolny prvek x = xi € U a iterujeme zobrazen í xi+1 = n(xj) pro i = 1, 2..., az dojde ke zopakovan í prvku xk = xj pro k > j > 1. (To musí nastat, nebot A je konecna.) Jelikoz prvek xj byl jiz odebran z U, v kroku x = dojde k ukoncen í naseho while cyklu. Nadto je n prosta, a proto nemuze nastat xk = xj = n (x j-1) pro j > 1. Takto byl nalezen a odebran z U cyklus
(a\,..., dk-i) a důkaz je hotov.
□
Petr Hliněný,  FI MU Brno
-1:1B000: Dokazování algoritmů
8.4   Zajímavé algoritmy aritmetiky
Například umocnovan i na velmi vysoke exponenty je podkladem RSA sifry: Algoritmus 8.9. Binarní postup umocňovaní.
Pro dana Číslo a, b vypočtěme jejich celočíselnou mocninu (omezenou na zbytkově těídy modulo m kvůli prevenci pěetecení rozsahu celých císel v počítači), tj. c = ab mod m.
c — 1;
while   b > 0 do
if   b mod 2 > 0   then c  —   (c-a)   mod  m ; b  —   |_b/2j ;     a  —   (a-a)   mod m;
done
vysledek c ; c
Zde pouzijeme k dukazu spravnosti algoritmu indukci podle delky l binarn ího zapisu císla b.
Veta.   Algoritmus 8.9 skonci a vzdy spravne vypocte hodnotu mocniny
c = ab mod m.
Petr Hliněný,  FI MU Brno___FI: IB000: Dokazování algoritmů
c—1;
while   b > 0 do
if   b mod 2 > 0   then c  —   (c-a)   mod  m ; b  —   |_b/2j ;     a  —   (a-a)   mod m;
done
vysledek c ;
DUkaz: Baze indukce je pro l = 1, kdy b = 0 nebo b = 1. Přitom pro b = 0 se cyklus vubec nevykona a vysledek je c = 1. Pro b = 1 se vykona jen jedna iterace cyklu a vysledek je c = a mod m. c
Necht tvrzení platí pro lo > 1 a uvazme l = lo + 1. Pak zřejme b > 2 a vykonaj í se alespoř dve iterace cyklu. Po prvn í iteraci bude a' = a2, b' = |_b/2j a c' = (ab mod 2) mod m. Tud íz delka binarn ího zapisu b' bude jen l0 a podle indukřcn iho přredpokladu zbyle iterace algoritmu skonřc i s vysledkem
= c' - a'b'   mod m = (a6  mod 2 - a2L6/2J)   mod m = ab   mod m.
□
Petr Hliněný,  FI MU Brno___IB000: Dokazování algoritn
c
Na záver lekce si ukázeme jeden netradicní krátky algoritmus a jeho analyzu a dukaz ponecháme zde otevřene. Dokázete popsat, na cem je algoritmus zalozen?
Algoritmus 8.10. Celočíselná odmocnina.
Pro dané pěirozené číslo x vypočteme dolní celou část jeho odmocniny r =
Lv^J-
p — x;     r — 0; while   p > 0 do
while   (r + p)2 < x   do r  —  r+p ;
p — Lp/2J ;
done
vyísledek r ;
Petr Hliněný,  FI MU Brno___IB000: Dokazování algoritn