' $'
&
$
%Petr Hliněný, FI MU Brno 1 IB000 "Úv. Inf.": Základní formalismy
1 Základní formalismy: Důkaz a Algoritmus1 Základní formalismy: Důkaz a Algoritmus
Studium informatiky neznamená jen ,,naučit se nějaký programovací jazyk , nýbrž za-
hrnuje celý soubor dalších relevantních předmětů, mezi nimiž najdeme i matematicko­
teoretické (formální) základy moderní informatiky.
Právě odborný nadhled nad celou informatikou včetně nezbytné formální teorie odliší
řadového ,,programátora , kterých jsou dnes mraky i bez VŠ vzdělání, od skutečného
(a mnohem lépe placeného) IT experta.
' $'
&
$
%Petr Hliněný, FI MU Brno 1 IB000 "Úv. Inf.": Základní formalismy
1 Základní formalismy: Důkaz a Algoritmus1 Základní formalismy: Důkaz a Algoritmus
Studium informatiky neznamená jen ,,naučit se nějaký programovací jazyk , nýbrž za-
hrnuje celý soubor dalších relevantních předmětů, mezi nimiž najdeme i matematicko­
teoretické (formální) základy moderní informatiky.
Právě odborný nadhled nad celou informatikou včetně nezbytné formální teorie odliší
řadového ,,programátora , kterých jsou dnes mraky i bez VŠ vzdělání, od skutečného
(a mnohem lépe placeného) IT experta.
Stručný přehled lekce
* Pochopení formálního zápisu a významu matematických tvrzení (vět)
a jejich důkazů.
* Rozbor logické struktury matematických vět,
konstruktivnosti důkazů.
* Správný formální zápis postupu ­ algoritmu, ve světle matematických
formalismů.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Základní formalismy
1.1 Úvod do matematického dokazování1.1 Úvod do matematického dokazování
Matematika (a tudíž i teoretická informatika jako její součást) se vyznačuje
velmi přísnými formálními požadavky na korektnost argumentace.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Základní formalismy
1.1 Úvod do matematického dokazování1.1 Úvod do matematického dokazování
Matematika (a tudíž i teoretická informatika jako její součást) se vyznačuje
velmi přísnými formálními požadavky na korektnost argumentace.
ˇ Uvažme matematickou větu (neboli tvrzení) tvaru
,,Jestliže platí předpoklady, pak platí závěr .
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Základní formalismy
1.1 Úvod do matematického dokazování1.1 Úvod do matematického dokazování
Matematika (a tudíž i teoretická informatika jako její součást) se vyznačuje
velmi přísnými formálními požadavky na korektnost argumentace.
ˇ Uvažme matematickou větu (neboli tvrzení) tvaru
,,Jestliže platí předpoklady, pak platí závěr .
ˇ Důkaz této věty je konečná posloupnost tvrzení, kde
 každé tvrzení je buď
­ předpoklad, nebo
­ obecně přijatá ,,pravda ­ axiom, nebo
­ plyne z předchozích a dříve dokázaných tvrzení podle nějakého ,,ak-
ceptovaného logického principu ­ odvozovacího pravidla;
 poslední tvrzení je závěr.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": Základní formalismy
1.1 Úvod do matematického dokazování1.1 Úvod do matematického dokazování
Matematika (a tudíž i teoretická informatika jako její součást) se vyznačuje
velmi přísnými formálními požadavky na korektnost argumentace.
ˇ Uvažme matematickou větu (neboli tvrzení) tvaru
,,Jestliže platí předpoklady, pak platí závěr .
ˇ Důkaz této věty je konečná posloupnost tvrzení, kde
 každé tvrzení je buď
­ předpoklad, nebo
­ obecně přijatá ,,pravda ­ axiom, nebo
­ plyne z předchozích a dříve dokázaných tvrzení podle nějakého ,,ak-
ceptovaného logického principu ­ odvozovacího pravidla;
 poslední tvrzení je závěr.
O potřebné úrovni formality matematických důkazů a o běžných důkazových technikách
se dozvíme dále v této lekci. . .
' $'
&
$
%Petr Hliněný, FI MU Brno 3 IB000 "Úv. Inf.": Základní formalismy
Poznámka pro připomenutí:
ˇ Sudé číslo je celé číslo dělitelné 2, tj. tvaru 2k.
ˇ Liché číslo je celé číslo nedělitelné 2, tj. tvaru 2k + 1.
Příklad 1.1. Uvažujme následující matematické tvrzení (které jistě už znáte).
Věta. Jestliže x je součtem dvou lichých čísel, pak x je sudé.
' $'
&
$
%Petr Hliněný, FI MU Brno 3 IB000 "Úv. Inf.": Základní formalismy
Poznámka pro připomenutí:
ˇ Sudé číslo je celé číslo dělitelné 2, tj. tvaru 2k.
ˇ Liché číslo je celé číslo nedělitelné 2, tj. tvaru 2k + 1.
Příklad 1.1. Uvažujme následující matematické tvrzení (které jistě už znáte).
Věta. Jestliže x je součtem dvou lichých čísel, pak x je sudé.
Důkaz postupuje v následujících formálních krocích:
tvrzení zdůvodnění
1) a = 2k + 1, k celé předpoklad
2) b = 2l + 1, l celé předpoklad
' $'
&
$
%Petr Hliněný, FI MU Brno 3 IB000 "Úv. Inf.": Základní formalismy
Poznámka pro připomenutí:
ˇ Sudé číslo je celé číslo dělitelné 2, tj. tvaru 2k.
ˇ Liché číslo je celé číslo nedělitelné 2, tj. tvaru 2k + 1.
Příklad 1.1. Uvažujme následující matematické tvrzení (které jistě už znáte).
Věta. Jestliže x je součtem dvou lichých čísel, pak x je sudé.
Důkaz postupuje v následujících formálních krocích:
tvrzení zdůvodnění
1) a = 2k + 1, k celé předpoklad
2) b = 2l + 1, l celé předpoklad
3) x = a + b = 2k + 2l + 1 + 1 1,2) a komutativita sčítání (axiom)
4) x = 2(k + l) + 2  1 3) a distributivnost násobení
5) x = 2(k + l + 1) 4) a opět distributivnost násobení
2
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Základní formalismy
Příklad 1.2. Dokažte:
Věta. Jestliže x a y jsou racionální čísla pro která platí x < y, pak existuje
racionální číslo z pro které platí x < z < y.
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Základní formalismy
Příklad 1.2. Dokažte:
Věta. Jestliže x a y jsou racionální čísla pro která platí x < y, pak existuje
racionální číslo z pro které platí x < z < y.
Důkaz (s již trochu méně formálním zápisem) zní:
ˇ Nechť z = x+y
2 = x + y-x
2 = y - y-x
2 .
ˇ Číslo z je racionální, neboť x a y jsou racionální.
ˇ Platí z > x, neboť y-x
2 > 0.
ˇ Dále platí z < y, opět neboť y-x
2 > 0.
ˇ Celkem x < z < y.
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Základní formalismy
Příklad 1.2. Dokažte:
Věta. Jestliže x a y jsou racionální čísla pro která platí x < y, pak existuje
racionální číslo z pro které platí x < z < y.
Důkaz (s již trochu méně formálním zápisem) zní:
ˇ Nechť z = x+y
2 = x + y-x
2 = y - y-x
2 .
ˇ Číslo z je racionální, neboť x a y jsou racionální.
ˇ Platí z > x, neboť y-x
2 > 0.
ˇ Dále platí z < y, opět neboť y-x
2 > 0.
ˇ Celkem x < z < y.
2
Poznámka. Alternativní formulace Věty z Příkladu 1.2 mohou znít:
ˇ Pro každé x, y  Q, kde x < y, existuje z  Q takové, že x < z < y.
ˇ Množina racionálních čísel je hustá.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Základní formalismy
1.2 Struktura matematických vět a důkazů1.2 Struktura matematických vět a důkazů
ˇ První krok formálního důkazu je uvědomit si, co se má dokázat, tedy co je
předpoklad a co závěr dokazovaného tvrzení.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Základní formalismy
1.2 Struktura matematických vět a důkazů1.2 Struktura matematických vět a důkazů
ˇ První krok formálního důkazu je uvědomit si, co se má dokázat, tedy co je
předpoklad a co závěr dokazovaného tvrzení.
ˇ Příklady:
 Věta. Konečná množina má konečně mnoho podmnožin.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Základní formalismy
1.2 Struktura matematických vět a důkazů1.2 Struktura matematických vět a důkazů
ˇ První krok formálního důkazu je uvědomit si, co se má dokázat, tedy co je
předpoklad a co závěr dokazovaného tvrzení.
ˇ Příklady:
 Věta. Konečná množina má konečně mnoho podmnožin.
 Věta. sin2
() + cos2() = 1.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Základní formalismy
1.2 Struktura matematických vět a důkazů1.2 Struktura matematických vět a důkazů
ˇ První krok formálního důkazu je uvědomit si, co se má dokázat, tedy co je
předpoklad a co závěr dokazovaného tvrzení.
ˇ Příklady:
 Věta. Konečná množina má konečně mnoho podmnožin.
 Věta. sin2
() + cos2() = 1.
 Věta. Graf je rovinný jestliže neobsahuje podrozdělení K5 nebo K3,3.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Základní formalismy
1.2 Struktura matematických vět a důkazů1.2 Struktura matematických vět a důkazů
ˇ První krok formálního důkazu je uvědomit si, co se má dokázat, tedy co je
předpoklad a co závěr dokazovaného tvrzení.
ˇ Příklady:
 Věta. Konečná množina má konečně mnoho podmnožin.
 Věta. sin2
() + cos2() = 1.
 Věta. Graf je rovinný jestliže neobsahuje podrozdělení K5 nebo K3,3.
ˇ Často pomůže pouhé rozepsání definic pojmů, které se v dané větě vyskytují.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": Základní formalismy
1.2 Struktura matematických vět a důkazů1.2 Struktura matematických vět a důkazů
ˇ První krok formálního důkazu je uvědomit si, co se má dokázat, tedy co je
předpoklad a co závěr dokazovaného tvrzení.
ˇ Příklady:
 Věta. Konečná množina má konečně mnoho podmnožin.
 Věta. sin2
() + cos2() = 1.
 Věta. Graf je rovinný jestliže neobsahuje podrozdělení K5 nebo K3,3.
ˇ Často pomůže pouhé rozepsání definic pojmů, které se v dané větě vyskytují.
ˇ Jak ,,moc formální mají důkazy vlastně být?
 Záleží na tom, komu je důkaz určen -- ,,konzument musí být schopen
,,snadno ověřit korektnost každého tvrzení v důkazu a plně pochopit,
z čeho vyplývá.
 Je tedy hlavně na vás zvolit tu správnou úroveň formálnosti zápisu vět
i důkazů podle situace.
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Základní formalismy
Konstruktivní a existenční důkazy
Z hlediska praktické využitelnosti je potřeba rozlišit tyto dvě kategorie důkazů
(třebaže z formálně­matematického pohledu mezi nimi kvalitativní rozdíl není).
ˇ Důkaz Věty 1.2 je konstruktivní. Dokázali jsme nejen, že číslo z existuje,
ale podali jsme také návod, jak ho pro dané x a y sestrojit.
ˇ Existenční důkaz je takový, kde se prokáže existence nějakého objektu bez
toho, aby byl podán návod na jeho konstrukci.
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Základní formalismy
Konstruktivní a existenční důkazy
Z hlediska praktické využitelnosti je potřeba rozlišit tyto dvě kategorie důkazů
(třebaže z formálně­matematického pohledu mezi nimi kvalitativní rozdíl není).
ˇ Důkaz Věty 1.2 je konstruktivní. Dokázali jsme nejen, že číslo z existuje,
ale podali jsme také návod, jak ho pro dané x a y sestrojit.
ˇ Existenční důkaz je takový, kde se prokáže existence nějakého objektu bez
toho, aby byl podán návod na jeho konstrukci.
Příklad 1.3. čistě existenčního důkazu.
Věta. Existuje program, který vypíše na obrazovku čísla tažená v 45. tahu
sportky v roce 2006.
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Základní formalismy
Konstruktivní a existenční důkazy
Z hlediska praktické využitelnosti je potřeba rozlišit tyto dvě kategorie důkazů
(třebaže z formálně­matematického pohledu mezi nimi kvalitativní rozdíl není).
ˇ Důkaz Věty 1.2 je konstruktivní. Dokázali jsme nejen, že číslo z existuje,
ale podali jsme také návod, jak ho pro dané x a y sestrojit.
ˇ Existenční důkaz je takový, kde se prokáže existence nějakého objektu bez
toho, aby byl podán návod na jeho konstrukci.
Příklad 1.3. čistě existenčního důkazu.
Věta. Existuje program, který vypíše na obrazovku čísla tažená v 45. tahu
sportky v roce 2006.
Důkaz: Existuje pouze konečně mnoho možných výsledků losování 45. tahu
sportky v roce 2006. Pro každý možný výsledek existuje program, který tento
daný výsledek vypíše na obrazovku. Mezi těmito programy je tedy jistě ten,
který vypíše právě ten výsledek, který bude v 25. tahu sportky v roce 2006
skutečně vylosován.
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Základní formalismy
Konstruktivní a existenční důkazy
Z hlediska praktické využitelnosti je potřeba rozlišit tyto dvě kategorie důkazů
(třebaže z formálně­matematického pohledu mezi nimi kvalitativní rozdíl není).
ˇ Důkaz Věty 1.2 je konstruktivní. Dokázali jsme nejen, že číslo z existuje,
ale podali jsme také návod, jak ho pro dané x a y sestrojit.
ˇ Existenční důkaz je takový, kde se prokáže existence nějakého objektu bez
toho, aby byl podán návod na jeho konstrukci.
Příklad 1.3. čistě existenčního důkazu.
Věta. Existuje program, který vypíše na obrazovku čísla tažená v 45. tahu
sportky v roce 2006.
Důkaz: Existuje pouze konečně mnoho možných výsledků losování 45. tahu
sportky v roce 2006. Pro každý možný výsledek existuje program, který tento
daný výsledek vypíše na obrazovku. Mezi těmito programy je tedy jistě ten,
který vypíše právě ten výsledek, který bude v 25. tahu sportky v roce 2006
skutečně vylosován. 2
To je ale ,,podvod , že?
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": Základní formalismy
Konstruktivní a existenční důkazy
Z hlediska praktické využitelnosti je potřeba rozlišit tyto dvě kategorie důkazů
(třebaže z formálně­matematického pohledu mezi nimi kvalitativní rozdíl není).
ˇ Důkaz Věty 1.2 je konstruktivní. Dokázali jsme nejen, že číslo z existuje,
ale podali jsme také návod, jak ho pro dané x a y sestrojit.
ˇ Existenční důkaz je takový, kde se prokáže existence nějakého objektu bez
toho, aby byl podán návod na jeho konstrukci.
Příklad 1.3. čistě existenčního důkazu.
Věta. Existuje program, který vypíše na obrazovku čísla tažená v 45. tahu
sportky v roce 2006.
Důkaz: Existuje pouze konečně mnoho možných výsledků losování 45. tahu
sportky v roce 2006. Pro každý možný výsledek existuje program, který tento
daný výsledek vypíše na obrazovku. Mezi těmito programy je tedy jistě ten,
který vypíše právě ten výsledek, který bude v 25. tahu sportky v roce 2006
skutečně vylosován. 2
To je ale ,,podvod , že? A přece není. . .
Formálně správně to je prostě tak a tečka.
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": Základní formalismy
Fakt. Pro informatické i další aplikované disciplíny je důležitá konstruktivnost
důkazů vět, které se zde objevují.
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": Základní formalismy
Fakt. Pro informatické i další aplikované disciplíny je důležitá konstruktivnost
důkazů vět, které se zde objevují.
V matematice ale jsou mnohé příklady užitečných a nenahraditelných existenč-
ních důkazů, třeba tzv. pravděpodobnostní důkazy.
Příklad 1.4. ,,pravděpodobnostního existenčního důkazu.
Věta. Na dané množině bodů je zvoleno libovolně n2 podmnožin, každá
o n prvcích. Dokažte pro dostatečně velká n, že všechny body lze obarvit
dvěma barvami tak, aby žádná množina nebyla jednobarevná.
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": Základní formalismy
Fakt. Pro informatické i další aplikované disciplíny je důležitá konstruktivnost
důkazů vět, které se zde objevují.
V matematice ale jsou mnohé příklady užitečných a nenahraditelných existenč-
ních důkazů, třeba tzv. pravděpodobnostní důkazy.
Příklad 1.4. ,,pravděpodobnostního existenčního důkazu.
Věta. Na dané množině bodů je zvoleno libovolně n2 podmnožin, každá
o n prvcích. Dokažte pro dostatečně velká n, že všechny body lze obarvit
dvěma barvami tak, aby žádná množina nebyla jednobarevná.
Důkaz: U každého bodu si ,,hodíme mincí a podle výsledku zvolíme barvu červeně
nebo modře. (Nezávislé volby s pravděpodobností 1
2 .) Pravděpodobnost, že zvolených
n bodů vyjde jednobarevných, je jen 2
2n = 21-n
.
Pro n2
podmnožin tak je pravděpodobnost, že některá z nich vyjde jednobarevná, shora
ohraničená součtem
21-n
+ . . . + 21-n
n2
=
n2
2n-1
 0 .
Jelikož je toto číslo (pravděpodobnost) pro n  7 menší než 1, bude existovat obarvení
bez jednobarevných zvolených podmnožin. 2
' $'
&
$
%Petr Hliněný, FI MU Brno 8 IB000 "Úv. Inf.": Základní formalismy
1.3 Formální popis algoritmu1.3 Formální popis algoritmu
Položme si otázku, co je vlastně algoritmus?
Poznámka: Za definici algoritmu je obecně přijímána tzv. Church­Turingova teze tvr-
dí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.
' $'
&
$
%Petr Hliněný, FI MU Brno 8 IB000 "Úv. Inf.": Základní formalismy
1.3 Formální popis algoritmu1.3 Formální popis algoritmu
Položme si otázku, co je vlastně algoritmus?
Poznámka: Za definici algoritmu je obecně přijímána tzv. Church­Turingova teze tvr-
dí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.
Konvence 1.5. Zjednodušeně zde algoritmem rozumíme konečnou posloup-
nost elementárních (výpočetních) kroků, ve které každý další krok využívá
vstupní údaje či hodnoty vypočtené v předchozích krocích.
Pro zpřehlednění a zkrácení zápisu algoritmu využíváme řídící konstrukce ­
podmíněná větvení a cykly.
' $'
&
$
%Petr Hliněný, FI MU Brno 8 IB000 "Úv. Inf.": Základní formalismy
1.3 Formální popis algoritmu1.3 Formální popis algoritmu
Položme si otázku, co je vlastně algoritmus?
Poznámka: Za definici algoritmu je obecně přijímána tzv. Church­Turingova teze tvr-
dí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.
Konvence 1.5. Zjednodušeně zde algoritmem rozumíme konečnou posloup-
nost elementárních (výpočetních) kroků, ve které každý další krok využívá
vstupní údaje či hodnoty vypočtené v předchozích krocích.
Pro zpřehlednění a zkrácení zápisu algoritmu využíváme řídící konstrukce ­
podmíněná větvení a cykly.
Vidíte, jak blízké si jsou konstruktivní matematické důkazy a formální zápisy algoritmů?
' $'
&
$
%Petr Hliněný, FI MU Brno 9 IB000 "Úv. Inf.": Základní formalismy
Příklad 1.6. Zápis algoritmu pro výpočet průměru z daného pole a[] s n prvky.
ˇ Inicializujeme sum  0 ;
ˇ postupně pro i=0,1,2,...,n-1 provedeme
 sum  sum+a[i] ;
ˇ vypíšeme podíl (sum/n) .
' $'
&
$
%Petr Hliněný, FI MU Brno 9 IB000 "Úv. Inf.": Základní formalismy
Příklad 1.6. Zápis algoritmu pro výpočet průměru z daného pole a[] s n prvky.
ˇ Inicializujeme sum  0 ;
ˇ postupně pro i=0,1,2,...,n-1 provedeme
 sum  sum+a[i] ;
ˇ vypíšeme podíl (sum/n) .
2
Ve ,,vyšší úrovni formálnosti (s jasnějším vyznačením řídících struktur algo-
ritmu) se totéž dá zapsat jako:
Algoritmus 1.7. Průměr
z daného pole a[] s n prvky.
sum  0;
for i  0,1,2,...,n-1 do
sum  sum+a[i];
done
res  sum/n;
output res;
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": Základní formalismy
Značení. Pro potřeby formálního popisu algoritmů v předmětu IB000 si zave-
deme následovnou konvenci:
ˇ 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": Základní formalismy
Značení. Pro potřeby formálního popisu algoritmů v předmětu IB000 si zave-
deme následovnou konvenci:
ˇ 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 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": Základní formalismy
Značení. Pro potřeby formálního popisu algoritmů v předmětu IB000 si zave-
deme následovnou konvenci:
ˇ 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 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 11 IB000 "Úv. Inf.": Základní formalismy
Malé srovnání závěrem
Jak to tedy je s vhodnou a únosnou mírou formalizace u matematických důkazů
i u zápisu algoritmů?
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Základní formalismy
Malé srovnání závěrem
Jak to tedy je s vhodnou a únosnou mírou formalizace u matematických důkazů
i u zápisu algoritmů?
zcela formální běžná úroveň
matematika formální rozepsání všech
elem. kroků (Příklad 1.1)
strukturovaný a matem.
přesný text v běžném jazyce
algoritmy rozepsání všech elem. kroků
ve výpočetním modelu
strukturovaný rozpis kroků
(Algoritmus 1.7), i s využi-
tím běžného jazyka
programování asembler / strojový kód
(kde se s ním dnes běžně se-
tkáte?)
,,vyšší (strukturované)
programovací jazyky,
například Java
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Základní formalismy
Malé srovnání závěrem
Jak to tedy je s vhodnou a únosnou mírou formalizace u matematických důkazů
i u zápisu algoritmů?
zcela formální běžná úroveň
matematika formální rozepsání všech
elem. kroků (Příklad 1.1)
strukturovaný a matem.
přesný text v běžném jazyce
algoritmy rozepsání všech elem. kroků
ve výpočetním modelu
strukturovaný rozpis kroků
(Algoritmus 1.7), i s využi-
tím běžného jazyka
programování asembler / strojový kód
(kde se s ním dnes běžně se-
tkáte?)
,,vyšší (strukturované)
programovací jazyky,
například Java
Pochopitelně se ve všech třech bodech obvykle držíme druhého přístupu, tedy běžné
úrovně formality, pokud si specifické podmínky výslovně nevyžadují přístup nejvyšší
formality. . .