10   Formalizace a důkazy pro algoritmy
Je faktem, že situace, kdy programátorem zapsaný kód ve skutečnosti počítá něco trochu jiného, než si autor 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ž na počátku studia informatiky je žádoucí klást důraz na správné chápání zápisu algoritmů i na přesné důkazy jejich vlastností a správnosti.
Stručný přehled lekce
c
* Jednoduchá formalizace pojmu algoritmus.
* Jak dokazovat vlastnosti a správnost algoritmů.
* Indukce při dokazování algoritmů. Rekurzivní algoritmy.
Petr Hliněný, Fl MU Brno, 2012
1/14
Fl: IB000: Důkazy pro algoritmy
10.1   Formální popis algoritmu
Před samotným závěrem kurzu si položme otázku, co je vlastně algoritmus?
Poznámka: Za definici algoritmu je obecně přijímána tzv. Church-Turingova teze tvrdící, že všechny algoritmy lze „simulovat" na Turingově stroji. Jedná se sice o přesnou, ale značně nepraktickou definici.
Mimo Turingova stroje existují i jiné matematické modely výpočtů, jako třeba stroj RAM, který je abstrakcí skutečného strojového kódu, nebo neprocedurální modely, c
Konvence 10.1. Zjednodušeně zde algoritmem rozumíme konečnou posloupnost elementárních výpočetních kroků, ve které každý další krok vhodně využívá (neboli závisí na) vstupní údaje či hodnoty vypočtené v předchozích krocích. Tuto závislost přitom pojímáme zcela obecně nejen na operandy, ale i na vykonávané instrukce v krocích.
Pro zápis algoritmu a jeho zpřehlednění a zkrácení využíváme řídící konstrukce - podmíněná větvení a cykly, c
Vidíte, jak blízké si jsou konstruktivní matematické důkazy a algoritmy v našem pojetí? Jedná se nakonec o jeden ze záměrů našeho přístupu.. .
Petr Hliněný, Fl MU Brno, 2012
2/14
Fl: IB000: Důkazy pro algoritmy
Ukázka algoritmického zápisu
Příklad 10.2. Zápis algoritmu pro výpočet průměru daného pole a[] s n prvky.
• Inicializujeme sum    0 ;
• postupně pro i=0,l,2, . . . ,n-l provedeme
* sum    sum+a[i] ;
• vypíšeme podíl (sum/n) . c
□
Ve „vyšší úrovni" formálnosti se totéž dá zapsat jako:
Algoritmus 10.3. Průměr z daného pole a[] s n prvky.
input pole a [] délky n; sum    0;
foreach   i     0,1,2,...,n-l do sum     sum+a[i];
done
res sum/n; output res;
Petr Hliněný, Fl MU Brno, 2012
3/14
Fl: IB000: Důkazy pro algoritmy
Symbolický zápis algoritmů
Značení. Pro potřeby symbolického formálního zápisu algoritmu v predmetu Fl: IB000 si zavedeme následující pravidla:
• Proměnné nebudeme deklarovat ani typovat, pole odlišíme závorkami p [].
• Prirazení hodnoty zapisujeme a-í—b, prípadne 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, c
• 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 f i).
• Pevný cyklus uvedeme klíčovými slovy foreach ... do ... done, kde část za foreach musí obsahovat předem danou 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, 2012
4/14
Fl: IB000: Důkazy pro algoritmy
Co počítá následující algoritmus?
Příklad 10.4. Je dán následující symbolicky zapsaný algoritmus. Co je jeho výstupem v závislosti na vstupech a,b?
Algoritmus 10.5. input a, b; res 7;
foreach   i     1,2,...,b-l,b do res  ^— res + a+2-b + 8;
done
output res; i
Vypočítáme hodnoty výsledku res v počátečních iteracích cyklu:
0:    res = 7,
1:    res = 7 + a + 2b + 8,
2:    res = 7 + (a + 2b + 8) + (a + 2b + 8), ... c
Co dále? Výčet hodnot naznačuje pravidelnost a závěr, že obecný výsledek po b iteracích cyklu bude mít hodnotu
res = 7 + b(a + 26 + 8) = ab + 2b2 + 86 + 7. □
Petr Hliněný, Fl MU Brno, 2012
5/14
Fl: IB000: Důkazy pro algoritmy
10.2   O „správnosti" a dokazování programů
Jak se máme přesvědčit, že je daný program počítá „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.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, c
Mimochodem, co to vlastně znamená „počítat správně"?
Petr Hliněný, Fl MU Brno, 2012
6/14
Fl: IB000: Důkazy pro algoritmy
Ukázka formálního důkazu algoritmu
Příklad 10.6. Je dán následující symbolicky zapsaný algoritmus. Dokažte, že jeho výsledkem je „výměna" vstupních hodnot a,b.
Algoritmus 10.7. input a, b; a ^—  a+b; b  ^— a-b; a a-b; output a, b; i
Pro správný formální důkaz si musíme nejprve uvědomit, že je třeba symbolicky odlišit od sebe proměnné a,b od jejich daných vstupních hodnot, třeba ha, hifz Nyní v krocích algoritmu počítáme hodnoty proměnných:
* a = ha, b = hf,,
* a <— a + b = ha + hf,,   b = hf,, c
* a = ha + hb,   b-^a — b = ha + hb — hb = ha, c
* a <— a — b = ha + hf, — ha = hf,,   b = ha,
Tímto jsme s důkazem hotovi. □
Petr Hliněný, Fl MU Brno, 2012
7/14
Fl: IB000: Důkazy pro algoritmy
10*3   Jednoduché indukční dokazování
Pro dokazování algoritmů se jeví nejvhodněji matematická indukce, která je „jako stvořená" pro formální uchopení opakovaných sekvencí v algoritmech.
Příklad 10.8. Dokažte, že násl. algoritmus navrátí výsledek ab + 2b2 + 86 + 7.
Algoritmus 10.9. input a, b; res 7;
foreach   i     1,2,...,b-l,b do res  ^— res + a+2-b + 8;
done
output res; i
V prvé řadě si z důvodu formální přesnosti přeznačíme mez cyklu v algoritmu na foreach i <— 1,2,... ,c do .. (kde c = b). Poté postupujeme přirozeně indukcí podle počtu c iterací (už nezávisle na vstupní hodnotě b); dokazujeme, že výsledek výpočtu algoritmu bude res = ac + 2bc + 8c + 7.
Petr Hliněný, Fl MU Brno, 2012
8/14
Fl: IB000: Důkazy pro algoritmy
Algoritmus .
input a, b;
res i—7;
foreach   i     1,2,...,b-l,b do res  ^— res + a+2-b + 8;
done
output res; i Pro c = 0 je výsledek správně res = 0 + 7.
Pokud dále předpokládáme platnost vztahu res = ac + 26c + 8c + 7 po nějakých c iteracích cyklu foreach, tak následující iterace pro i 4—c + l (jejíž průběh na samotné hodnotě i nezáleží) změní hodnotu na
res <- res + a + 2b + 8 = ac + a + 26c + 2b + 8c + 8 + 7 = = a(c + 1) + 26(c + 1) + 8(c + 1) + 7.
Důkaz indukcí je tím hotov. □
Petr Hliněný, Fl MU Brno, 2012
9/14
Fl: IB000: Důkazy pro algoritmy
Příklad 10.10. Zjistěte, kolik znaků 'x' v závislosti na celočíselné hodnotě vstupního parametru n vypíše následující algoritmus.
Algoritmus 10.11.
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.8), že je celkem \n{n + l).c Budeme tedy dokazovat následující tvrzení:
Věta.   Pro každé n Algoritmus 10.11 výpise právě ^n(n + l) znaků ;x\
Petr Hliněný,  Fl MU Brno, 2012
10/14
Fl: IB000: Důkazy pro algoritmy
Algoritmus .
foreach   i<—l,2,3,...,n-l,n do
foreach   j     1,2,3,...,i-l,i do vytiskni   'x' ;
done done c
Věta.  Pro každé n Algoritmus 10.11 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ž je správně.
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, 2012
11/14
Fl: IB000: Důkazy pro algoritmy
10.4   Rekurzivní algoritmy
* Rekurentní vztahy posloupností, stručně uvedené v Oddíle 3.4, mají svou přirozenou obdobu v rekurzivně zapsaných algoritmech, c
* Zjednodušeně řečeno to jsou algoritmy, které se v průběhu výpočtu odvolávají na výsledky sebe sama pro jiné (menší) vstupní hodnoty, c
* U takových algoritmů je zvláště důležité kontrolovat jejich správnost a také proveditelnost.
Příklad 10.12. Symbolický zápis jednoduchého rekurzivního algoritmu.
Algoritmus. Rekurzivní funkce factorial(x) if x < 1 then   t 1; else   t <— x • factorial(x-1); return t
Co je výsledkem výpočtu?
Jednoduše řečeno, výsledkem je faktoriál vstupní přirozené hodnoty x, tj. hodnota xl = x ■ (x — 1).....2-1. □
Petr Hliněný,  Fl MU Brno, 2012
12/14
Fl: IB000: Důkazy pro algoritmy
Fibonacciho čísla
Pro další příklad rekurze se vrátíme k Oddílu 3.4, kde byla zmíněna známá Fibonacciho posloupnost 1,1, 2, 3, 5, 8,13, 21, 34, 55, 89,144,.... c
Algoritmus 10.13. Rekurzivní výpočet funkce f ibonacci (x) Pro dané přirozené x vypočítáme x-té Fibonacciho číslo následovně: if x < 2 then   t <— x;
else   t i—   fibonacci(x-l)+fibonacci(x-2); return t
c
Správnost Algoritmu 10.13 je víceméně zřejmá z jeho přímé podoby s rekurentním vzorcem v definici Fibonacciho čísel. Zamyslete se však, jak je to s praktickou „proveditelností" takového algoritmu...
Petr Hliněný,  Fl MU Brno, 2012
13/14
Fl: IB000: Důkazy pro algoritmy
Příklad 10.14. Nerekurzivní algoritmus pro Fibonacciho čísla.
Dokažte, že následující algoritmus pro každé přirozené n počítá tutéž hodnotu jako f ibonacci(n) v Algoritmu 10.13.
Algoritmus . input n;
b[0] <- 0;    b[l] <- 1; foreach   i     2,3,...,n do b [i]   <-  b[i-l]+b[i-2] ;
done
output b[n] i
Indukcí budeme dokazovat, že po i-té iteraci cyklu algoritmu bude vždy platit b[i] = fibonacci{i). Co se týče báze indukce, toto vyplývá z úvodního přiřazení.
Pro i > 2 pak předpokládáme platnost indukčního předpokladu b[j] = fibonacci(j) pro j = i — 1, i — 2.
V i-té iteraci cyklu nastane b[i] <—b[i — 1] + b[i — 2] = fibonacci(i — 1) + fibonacci{i — 2) = fibonacci{i). □
Petr Hliněný,  Fl MU Brno, 2012
14/14
Fl: IB000: Důkazy pro algoritmy