8   Dokazování vlastností algoritmů
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ě zapisovat algoritmy. Přitom situace, kdy programátorem zapsaný kód počítá něco trochu jiného, než si programátor představuje, je snad nejčastější programátorskou chybou -o to zákeřnější, že ji žádný „chytrý" překladač nemůže odhalit.
Proto již od počátku seriózního studia informatiky je vhodné klást důraz na správné chápání zápisu algoritmů i na důkazy jejich vlastností a správnosti, 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í algoritmů.
* Několik konkrétních algoritmů a jejich důkazů.
Petr Hliněný, Fl MU Brno, 2011
1/17
Fl: IB000: Dokazování algoritmů
Neformálně o „správnosti" programů
Jak se máme přesvědčit, že je daný program „správný"?c 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.c
• 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 opakované experimenty vedou k různým výsledkům. Nelze je tudíž ani rozumně ladit... c
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žadavkyx
* Pro „malé" algoritmy je možné podat přesný matematický důkaz .
* Narůstající složitosti programových systémů si pak vynucují vývoj jiných „spolehlivých" formálních verifikačních metod.
Petr Hliněný, Fl MU Brno, 2011
2/17
Fl: IB000: Dokazování algoritmů
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 . . . f i , kde else větev lze vynechat (a někdy, na jednom řádku, i f i).
• Pevný cyklus uvedeme klíčovými slovy f oreach ... do ... done , kde část za f oreach 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, foreach, 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ý, Fl MU Brno, 2011
3/17
Fl: IB000: Dokazování algoritmů
8.1   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.
foreach   i<—l,2,3,...,n-l,n do
foreach   j     1,2,3,...,i-l,i do vytiskni   'x' ;
done done c
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.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 výpise právě ^n(n + l) znaků ;x\
Petr Hliněný, Fl MU Brno, 2011
4/17
Fl: IB000: Dokazování algoritmů
Algoritmus 8.2.
foreach   i1,2,3,...,n-l,n do
foreach   j     1,2,3,...,i-l,i do vytiskni   'x' ;
done
done
Věta.  Pro každé při r. n Algoritmus 8.2 výpise právě \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.c
Nechť tedy tvrzení platí pro jakékoliv uq a položme n = uq + 1. Prvních uq iterací vnějšího cyklu podle indukčního předpokladu vypíše (ve vnitřním cyklu) celkem ^no{no + 1) znaků ;x\ Pak již následuje jen jedna poslední iterace vnějšího cyklu s if- n=no+l a v ní se vnitřní cyklus j <— 1,2, . . . , i=n iteruje celkem n = uq + 1 -krát. nCelkem tedy bude vytištěn tento počet znaků ;x;:
^n0(n0 + 1) + n0 + 1 = ^(n0 + 1 + l)(n0 + 1) = ^n{n + 1) Důkaz indukčního kroku je hotov. a
Petr Hliněný, Fl MU Brno, 2011
5/17
Fl: IB000: Dokazování algoritmů
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";
foreach   i<—l,2,3,...,n-l,n do vytiskni řetězec  st;
st  4— 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! c
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ý, Fl MU Brno, 2011
6/17
Fl: IB000: Dokazování algoritmů
Algoritmus 8.4.
st ^"z";
foreach   i1,2,3,...,n-l,n do vytiskni řetězec  st;
st  4— st . st ;     (zřetězení dvou kopií st za sebou)
done
Věta. Pro každé přirozené n Algoritmus 8.4 výpise právě 2n — 1 znaků 'z' a proměnná st bude na konci obsahovat řetězec 2n znaků 'z'. c
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.c
Nechť tedy tvrzení platí pro jakékoliv uq a položme n = n$ + 1. Podle indukčního předpokladu po prvních uq iteracích bude vytištěno 2n° — 1 znaků 'z' a proměnná st bude obsahovat řetězec 2n° znaků 'z'. V poslední iteraci cyklu (pro i 4— n=no+l) vytiskneme dalších 2n° znaků 'z' (z proměnné st) a dále řetězec st „zdvojnásobíme", c
Proto po n iteracích bude vytištěno celkem 2n° - 1 + 2n° = 2n°+1 - 1 = 2n - 1 znaků 'z' a v st bude uloženo 2 • 2n° = 2no+1 = 2n znaků 'z'. n
Petr Hliněný, Fl MU Brno, 2011
7/17
Fl: IB000: Dokazování algoritmů
8.2   Algoritmy pro relace
V dalších pokročilejších ukázkách volíme algoritmy pro relace. Algoritmus 8.5. Symetrický uzávěr.
Pro danou relaci R na n-prvkové množině A = {a±, ci2,..., an} vytvoříme její symetrický uzávěr R takto:
R <- R;
foreach   i     1,2,...,n-l,n do
foreach   j -í— 1,2, . . . ,n-l,n do
if  (di,aj) G i? A (dj,ai) 0 i? then i?  ^—  i? U{(a,', a^)} ;
done done :
Důkaz: Zde není důkaz vůbec obtížný. Relace R D i? je zřejmě symetrická, neboť (vnitřní) tělo cyklu pro všechny dvojice (a,i,aj) G R přidá i (aj,aj).
Z druhé strany všechny dvojice „přidané" v i? \i? musí být obsaženy podle
definice symetrické relace, takže i? je skutečně symetrickým uzávěrem podle definice uzávěru relace. □
Petr Hliněný, Fl MU Brno, 2011
8/17
Fl: IB000: Dokazování algoritmů
Algoritmus 8.6. Tranzitivní uzávěr.
Pro danou relaci R na n-prvkové množině A = {a±, ci2,..., an} vytvoříme její tranzitivní uzávěr R+ takto:
R+  <- R;
foreach   k<— 1,2,...,n-l,n do
foreach   i     l,2,...,n-l,n; j     l,2,...,n-l,n do
if  (aj,cifc) G R+ A (dfc,Oj) G i?+ then
if  (aí,aj)^R+ then i?+   <-  i?+U {(aj, a^)} ;
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
(aí,ae),(ae,cij) G S vyplývá (a^a,) G S.
Petr Hliněný, FI MU Brno, 2011
9/17
FI: IB000: Dokazování algoritmů
Věta. Po každých k > 0 iteracích vnějšího cyklu Algoritmu 8.6 aktuální hodnota relace R+ udává fc-částečně tranzitivní uzávěr relace R na A. c
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é ko > 0 a dokažme jej i pro k = &o + l. Zřejmě stačí uvažovat případ ko < n. Každá dvojice (a,i,aj) přidaná do R+ uvnitř cyklů musí náležet do fc-částečně tranzitivního uzávěru podle definice. Zbývá zdůvodnit, proč každá dvojice (a,i,aj) náležející do fc-částečně tranzitivního uzávěru, ale ne do fco-částečně tranzitivního uzávěru, bude do R+ v k-té iteraci přidána, c
Není těžké ověřit, že (a,i,aj) náleží do fc-částečně tranzitivního uzávěru, právě když v relaci i? nalezneme takovou cestu „po šipkách" z a,i do aj, která přechází pouze přes prvky kde í < k. V naší situaci vyplývá, že taková cesta musí použít i prvek (jen jednou!), a proto (aj,afc) i (a,k,a,j) náleží do fco-částečně tranzitivního uzávěru R. V k-té iteraci tudíž bude příslušná if podmínka splněná a (a,i,aj) bude přidána do R+. □
Petr Hliněný,  Fl MU Brno, 2011
10/17
Fl: IB000: Dokazování algoritmů
8.3   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áš algoritmus vůbec skončí. (To 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 f oreach cykly, přitom podle naší konvence obsahuje f oreach cyklus předem danou konečnou množinu hodnot pro řídící proměnnou, neboli náš f oreach 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, c
Metoda 8.7. Důkaz konečnosti.
Máme-li za úkol dokázat, že algoritmus skončí, vhodný postup je následující:
• 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 algoritmu neustále ostře zmenšuje, c
• Případně předchozí přístup rozšíříme na zvolenou k-tici přirozených parametrů 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ý,  Fl MU Brno, 2011
11/17
Fl: IB000: Dokazování algoritmů
Algoritmus 8.8. Cykly permutace.
Pro danou permutaci tt 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} = A; while        0 do
x -í— min (U);     (nejmenší prvek množiny)
začínáme výpis cyklu ' (' ;
while   xGU do vytiskneme x;
U  <-  U\{x} ;      x  <-  vr (x) ;
done
ukončíme výpis cyklu '}' ;
done
Jak dokážeme správnost tohoto algoritmu? c
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ý,  Fl MU Brno, 2011
12/17
Fl: IB000: Dokazování algoritmů
while        0 do
done
Věta. Za předp., že vnitřní while cyklus pro jakoukoliv poč. volbu x skončí, výpise cyklus permutace tt 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.
c
Důkaz: Postupujeme indukcí podle počtu cyklů v permutaci tt. Jediný cyklus v n (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ý, c
Podle Věty 6.6 se každá permutace dá zapsat jako složení disjunktních cyklů. Nechť tt je tedy složena z í > 1 cyklů. Po první iteraci while cyklu zbude v restrikci permutace tt 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čí.
□
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ý,  Fl MU Brno, 2011
13/17
Fl: IB000: Dokazování algoritmů
while   xGU do vytiskneme x;
U <- U\{x} ;     x <- tt(x) ;
done
Věta. Pokud tt je permutace, tak vnitřní while cyklus vždy skončí a nalezne v tt cyklus obsahující libovolný počáteční prvek x G 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.6: Vezmeme libovolný prvek x = x\ £ U a iterujeme zobrazení Xi+\ = tt(xí) pro i = 1,2..., až dojde ke zopakování prvku Xk = Xj pro k > j > 1. (To musí nastat, neboť A je konečná.) Jelikož prvek Xj byl již odebrán z U, v kroku x = dojde k ukončení našeho while cyklu. Nadto je tt prostá, a proto nemůže nastat xk = xj = Tt(xj-i) pro j > 1. Takto byl nalezen a odebrán z U cyklus (di,..., cifc-i) a důkaz je hotov. □
Petr Hliněný,  Fl MU Brno, 2011
14/17
Fl: IB000: Dokazování algoritmů
8.4   Zajímavé algoritmy aritmetiky
Například umocňování na velmi vysoké exponenty je podkladem RSA šifry: Algoritmus 8.9. Binární postup umocňování.
Pro daná číslo a, b vypočteme jejich celočíselnou mocninu (omezenou na zbytkové 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  -í—   (c-a)  mod  m ; b  i—   \b/2\ ;     a        (a-a)  mod  m ;
done
výsledek c ; i
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 správně vypočte hodnotu c = ab mod m.
Petr Hliněný,  Fl MU Brno, 2011
15/17
Fl: IB000: Dokazování algoritmů
while   b > O do
if   6 mod 2 > 0   then c  -í—   (c-a)  mod  m ; b  i—   \b/2\ ;     a        (a-a)  mod  m ;
done
výsledek c ;
Důkaz: Báze indukce je pro £ = 1, kdy 6 = 0 nebo 6 = 1. Přitom pro 6 = 0 se cyklus vůbec nevykoná a výsledek je c = 1. Pro 6 = 1 se vykoná jen jedna iterace cyklu a výsledek je c = a  mod m. c
Nechť tvrzení platí pro £q > 1 a uvažme £ = £q + 1. Pak zřejmě 6 > 2 a vykonají se alespoň dvě iterace cyklu. Po první iteraci bude a' = a2, b' = [b/2\ a d = (a6 mod 2) mod m. Tudíž délka binárního zápisu b' bude jen £q a podle indukčního předpokladu zbylé iterace algoritmu skončí s výsledkem
c = c' • a'h' mod m = (a6 mod 2 • a2L6/2J)  mod m = ah mod m.
Petr Hliněný,  Fl MU Brno, 2011
16/17
Fl: IB000: Dokazování algoritmů
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é přirozené číslo x vypočteme dolní celou část jeho odmocniny r =
p i— x;      r i— 0; while   p > 0 do
while   (r+p)2 < x   do r  -í— r+p ;
p <- Lp/2J ;
done
výsledek r ;
Petr Hliněný,  Fl MU Brno, 2011
17/17
Fl: IB000: Dokazování algoritmů