Petr Hliněný, FI MU Brno 1 FI: IB000: Dokazování algoritmů 8 Dokazování vlastností algoritmů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ý 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. 2 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. 2 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 FI: IB000: Dokazování algoritmů 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ý ?2 * Co třeba ladění programů? 2 Jelikož počet možných vstupních hodnot je (v principu) neohraničený, nelze otestovat všechna možná vstupní data.2 * 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 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 chování za jiných okolností.)2 * 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.2 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 FI: 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 ... fi , kde else větev lze vynechat (a někdy, na jednom řádku, i fi). * Pevný cyklus uvedeme klíčovými slovy foreach ... do ... done , kde část za foreach 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ý, FI MU Brno 4 FI: IB000: Dokazování algoritmů 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. foreach i 1,2,3,...,n-1,n do foreach j 1,2,3,...,i-1,i do vytiskni 'x'; done done 2 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 1 2 n(n + 1). 2Budeme tedy dokazovat následující tvrzení: Věta. Pro každé přir. n Algoritmus 8.2 vypíše právě 1 2n(n+1) znaků 'x'. Petr Hliněný, FI MU Brno 5 FI: 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 2 Věta. Pro každé přir. n Algoritmus 8.2 vypíše právě 1 2n(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.2 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 2n0(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. 2Celkem 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 FI: 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 1,2,3,...,n-1,n do vytiskni řetězec st; st st+st ; (zřetězení dvou kopií st za sebou) done 2 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 . . .. 2Na 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! 2 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 FI: 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 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'. 2 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 . 2 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 FI: IB000: Dokazování algoritmů 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 ; foreach i 1,2,...,n-1,n do foreach j 1,2,...,n-1,n do if (ai, aj) R (aj, ai) R then R R {(aj, ai)} ; done done 2 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 FI: IB000: Dokazování algoritmů 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 ; 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+ (ak, aj) R+ then if (ai, aj) R+ then R+ R+ {(ai, aj)} ; fi done done 2 Jak by se dala dokázat správnost popsaného algoritmu? Přímá aplikace indukce podle n nevypadá přínosně. . . (Zkuste si sami!)2 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 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á k-částečně tranzitivní uzávěr relace R na A. 2 Důkaz: Báze indukce pro k = 0 jasně platí, neboť věta v tom případě nic neříká.2 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ř cyklů 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. 2 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 FI: IB000: Dokazování algoritmů 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 jistě není samozřejmé a důkaz konečnosti je nutno v obecnosti podávat!) 2 Prozatím jsme však ukazovali algoritmy využívající jen foreach cykly, přitom podle naší konvence obsahuje foreach cyklus předem danou konečnou množinu hodnot pro řídící proměnnou, neboli náš foreach 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. 2 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 algoritmu neustále ostře zmenšuje. 2 * 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ý, FI MU Brno 12 FI: IB000: Dokazování algoritmů 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? 2 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 FI: IB000: Dokazování algoritmů 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. 2 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ý. 2 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 FI: IB000: Dokazování algoritmů 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. 2 Důkaz: Zde přímo zopakujeme argument důkazu Věty 6.5: Vezmeme libovolný prvek x = x1 U a iterujeme zobrazení xi+1 = (xi) 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 = xk dojde k ukončení našeho while cyklu. Nadto je prostá, a proto nemůže nastat xk = xj = (xj-1) pro j > 1. Takto byl nalezen a odebrán z U cyklus a1, . . . , ak-1 a důkaz je hotov. 2 Petr Hliněný, FI MU Brno 15 FI: IB000: Dokazování algoritmů 8.4 Zajímavé algoritmy aritmetiky8.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 (ca) mod m ; b b/2 ; a (aa) mod m ; done výsledek c ; 2 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 FI: IB000: Dokazování algoritmů 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. 2 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 a2b/2 ) mod m = ab mod m . 2 Petr Hliněný, FI MU Brno 17 FI: 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 = 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 ; 2