Updating typos and formating.

thesis/ctufit-thesis.tex

@@ -44,7 +44,7 @@
 \ctufityear{2023} % replace with the year of your defence
 \ctufitdeclarationplace{Praze} % replace with the place where you sign the declaration
 \ctufitdeclarationdate{\today} % replace with the date of signature of the declaration
-\ctufitabstractCZE{Tato práce se zabývá implementaci Dinitzova algoritmu pro hledání maximálního toku v síti a formálnímu důkazu jednotlivých použitích funkcí. Teoretická část seznámí čtenáře s teorií toků v sítích a myšlenkou Dinitzova algoritmu. Představí čtenáři také framework Frama-C pro formální analýzu kódu v programovacím jazyce C a anotační jazyk ACSL, který frameworku pomáhá s verifikací. Praktická část seznámí čtenáře s použitými metodami pro implementaci Dinitzova algoritmu a také objasní použité anotace pro verifikaci algoritmu. }
+\ctufitabstractCZE{Tato práce se zabývá implementaci Dinitzova algoritmu pro hledání maximálního toku v~síti a formálnímu důkazu jednotlivých použitích funkcí. Teoretická část seznámí čtenáře s~teorií toků v~sítích a~myšlenkou Dinitzova algoritmu. Představí čtenáři také framework Frama-C pro formální analýzu kódu v~programovacím jazyce C a~anotační jazyk ACSL, který frameworku pomáhá s~verifikací. Praktická část seznámí čtenáře s~použitými metodami pro implementaci Dinitzova algoritmu a~také objasní použité anotace pro verifikaci algoritmu.}
 \ctufitabstractENG{This thesis deals with the implementation of the Dinitz algorithm for finding maximum flow in the network and the formal proof of individual functions, that it uses. The theoretical part introduces the reader to the theory of flows in networks and the idea of the Dinitz algorithm. It will also introduce the reader to the Frama-C framework for formal code analysis in the C programming language and the ACSL annotation language, which helps the framework with the verification. The practical part introduces the reader to the methods used to implement the Dinitz algorithm and also clarifies the annotations used for the algorithm verification.}
 \ctufitkeywordsCZE{Frama-C, WP, RTE, ACSL, Dinitzův algoritmus, ověřená implementace}
 \ctufitkeywordsENG{Frama-C, WP, RTE, ACSL, Dinitz algorithm, verified implementation}

thesis/text/text.tex

@@ -5,52 +5,52 @@
 \setcounter{page}{1}
 V dnešní době se programy staly nedílnou součástí naší společnosti, řídí naší infrastrukturu počínaje od základních lidských potřeb, například dostupnost pitné vody, zemního plynu až po provoz jaderných elektráren. Stejně tak programy spravují mnoho dalších systémů, které společnost využívá, mezi jinými peněžní systémy jako jsou platby, bankovní účty, daně nebo také dopravní systémy, ať už jsou to semafory na silnicích nebo řízení vlaků, lodí či letadel. 
-Ve zkratce se programy vyskytují všude kolem nás a o to větší je poté problém, když v některém z těchto programů nastane chyba. Tyto chyby mohou zavinit peněžní ztráty od desítek, nebo stovek tisíc korun až po trvalé následky, či dokonce ztráty na životech. A proto se s každým rokem klade větší důraz na prověřování těchto programů, abychom se chybám vyhnuli. 
-Jednou z nejčastěji používaných metod je testování programu. Základní myšlenkou tohoto testování je vytvoření velkého množství vstupů, které jsou náhodné a poté menší část vstupů, které byly vytvořeny programátorem nebo testerem a jsou zaměřené na krajní či zranitelnější části programu. Tento postup nám dává jistotu, že ve většině případů program bude fungovat správně, ale nezaručuje nám bezchybnost daného programu a jak už bylo zmíněno i jedna malá chyba může vést na katastrofální následky.
-Z tohoto důvodu se tato práce bude zabývat statickou a hlavně formální analýzou programu ~\cite{compiler:analysis}. Na rozdíl od testování, statická analýza kontroluje program bez nutnosti spuštění a dokáže verifikovat, zda program je korektní. Kvůli nerozhodnutelnosti některých problémů, ne všechny chyby lze označit za vyřešené, nebo nemožné a tedy malé procento chyb zůstává možnou hrozbou, ale dosahujeme zde dostatečných procent korektnosti a bezchybnosti, abychom mohli daný program využívat v důležitých místech. 
-Formální analýza je rozšířenou statickou analýzou, která využívá matematických operací a tvrzení, aby vyřešila složité problémy v programu. Účelem formální analýzy je tedy dokázat, ať už pomocí vlastních vygenerovaných důkazů, nebo programátorem dodaných, že program je korektní. V této práci budeme využívat formální analýzu k testování korektnosti implementace Dinitzova algoritmu.
-Dinitzův algoritmus je jedním z postupů, jak získat maximální tok v sítích. Maximální tok nám představuje množství média např. vody, elektřiny nebo i lidí, které dokážeme přenést či převést z bodu A do bodu B. Mnoho situací z našeho života lze tedy přeformulovat na problém nalezení maximálního toku, jak už bylo zmíněno doručení média, přeprava lidí nebo řízení leteckého provozu.
+Ve zkratce se programy vyskytují všude kolem nás a~o to větší je poté problém, když v~některém z~těchto programů nastane chyba. Tyto chyby mohou zavinit peněžní ztráty od desítek, nebo stovek tisíc korun až po trvalé následky, či dokonce ztráty na životech. A~proto se s~každým rokem klade větší důraz na prověřování těchto programů, abychom se chybám vyhnuli. 
+Jednou z~nejčastěji používaných metod je testování programu. Základní myšlenkou tohoto testování je vytvoření velkého množství vstupů, které jsou náhodné a~poté menší část vstupů, které byly vytvořeny programátorem nebo testerem a~jsou zaměřené na krajní či zranitelnější části programu. Tento postup nám dává jistotu, že ve většině případů program bude fungovat správně, ale nezaručuje nám bezchybnost daného programu a~jak už bylo zmíněno i jedna malá chyba může vést na katastrofální následky.
+Z tohoto důvodu se tato práce bude zabývat statickou a~hlavně formální analýzou programu~\cite{compiler:analysis}. Na rozdíl od testování, statická analýza kontroluje program bez nutnosti spuštění a~dokáže verifikovat, zda program je korektní. Kvůli nerozhodnutelnosti některých problémů, ne všechny chyby lze označit za vyřešené, nebo nemožné a~tedy malé procento chyb zůstává možnou hrozbou, ale dosahujeme zde dostatečných procent korektnosti a~bezchybnosti, abychom mohli daný program využívat v~důležitých místech. 
+Formální analýza je rozšířenou statickou analýzou, která využívá matematických operací a~tvrzení, aby vyřešila složité problémy v~programu. Účelem formální analýzy je tedy dokázat, ať už pomocí vlastních vygenerovaných důkazů, nebo programátorem dodaných, že program je korektní. V~této práci budeme využívat formální analýzu k testování korektnosti implementace Dinitzova algoritmu.
+Dinitzův algoritmus je jedním z~postupů, jak získat maximální tok v~sítích. Maximální tok nám představuje množství média např. vody, elektřiny nebo i lidí, které dokážeme přenést či převést z~bodu A do bodu B. Mnoho situací z~našeho života lze tedy přeformulovat na problém nalezení maximálního toku, jak už bylo zmíněno doručení média, přeprava lidí nebo řízení leteckého provozu.
 \newpage{}
-Hlavním cílem práce je vytvořit implementaci Dinitzova algoritmu, pro hledání maximálního toku v orientované grafové síti, napsáném v programovacím jazyce C a poté ověření implementace Dinitzova algoritmu pomocí anotačního jazyka ACSL a prostředí Frama-C.
-Záměrem teoretické části práce je seznámení čtenáře se zakládanými pojmy z oblasti toků v orientovaných grafových sítích a dále popsání a vysvětlení Dinitzova algoritmu.
-Účelem praktické části práce je následné popsání a vysvětlení konceptů využitých pro implementaci, ověření Dinitzova algoritmu a diskuze, které části nebo aspekty nebylo možné ověřit.
+Hlavním cílem práce je vytvořit implementaci Dinitzova algoritmu, pro hledání maximálního toku v~orientované grafové síti, napsáném v~programovacím jazyce C a~poté ověření implementace Dinitzova algoritmu pomocí anotačního jazyka ACSL a~prostředí Frama-C.
+Záměrem teoretické části práce je seznámení čtenáře se zakládanými pojmy z~oblasti toků v~orientovaných grafových sítích a~dále popsání a~vysvětlení Dinitzova algoritmu.
+Účelem praktické části práce je následné popsání a~vysvětlení konceptů využitých pro implementaci, ověření Dinitzova algoritmu a~diskuze, které části nebo aspekty nebylo možné ověřit.
 %---------------------------------------------------------------
-\chapter{Toky v sítích}
+\chapter{Toky v~sítích}
 %---------------------------------------------------------------
-V této kapitole uvedeme základní pojmy a definice teorie grafů a toků v sítích, které budou další kapitoly využívat. Poté představíme problém maximálního toku, způsoby řešení a situace z reálného života, které můžeme převést na problém maximálního toku. Hlavním zdrojem informací jsou materiály z předmětu BI-AG2~\cite{predAG2} a kniha \textit{Průvodce labyrintem algoritmů}~\cite{PruvodceLab}
-\section{Teorie a definice}
+V této kapitole uvedeme základní pojmy a~definice teorie grafů a~toků v~sítích, které budou další kapitoly využívat. Poté představíme problém maximálního toku, způsoby řešení a~situace z~reálného života, které můžeme převést na problém maximálního toku. Hlavním zdrojem informací jsou materiály z~předmětu BI-AG2~\cite{predAG2} a~kniha \textit{Průvodce labyrintem algoritmů}~\cite{PruvodceLab}
+\section{Teorie a~definice}
 \begin{definition}[Orientovaný graf~\cite{PruvodceLab}] \label{def:orientGraf}
     \emph{Orientovaný graf} G je uspořádaná dvojice $(V, E)$, kde V je neprázdná konečná
-množina vrcholů a $E \subseteq V \times V$ je množina orientovaných hran. \emph{Orientovaná hrana} $(u, v) \in{} E$ je uspořádaná dvojice různých vrcholů $u, v \in{} V$,
+množina vrcholů a~$E \subseteq V \times V$ je množina orientovaných hran. \emph{Orientovaná hrana} $(u, v) \in{} E$ je uspořádaná dvojice různých vrcholů $u, v \in{} V$,
 někdy ji zkráceně značíme uv. 
 \end{definition}
 \begin{definition} [Síť~\cite{predAG2}] \label{def:Sit}
-    \emph{Sítí} nazveme čtveřici $(G, z, s, c)$, kde $G = (V,E)$ je orientovaný graf, $z$ a $s$ dva různé vrcholy grafu G (říkáme jim $zdroj$ a $stok$) a kapacita $c\colon{}E \rightarrow{} \mathbb{R} _Q^+$  je funkce ohodnocující hrany nezápornými reálnými čísly.
+    \emph{Sítí} nazveme čtveřici $(G, z, s, c)$, kde $G = (V,E)$ je orientovaný graf, $z$ a~$s$ dva různé vrcholy grafu G (říkáme jim $zdroj$ a~$stok$) a~kapacita $c\colon{}E \rightarrow{} \mathbb{R} _Q^+$  je funkce ohodnocující hrany nezápornými reálnými čísly.
 \end{definition}
-\begin{definition} [Tok v síti~ \cite{predAG2}] \label{def:vlastToku}
-    \emph{Tok v síti $(G, z, s, c)$} je každá funkce $f\colon{}E \rightarrow{} \mathbb{R} _0^+$ splňující:
+\begin{definition} [Tok v~síti~ \cite{predAG2}] \label{def:vlastToku}
+    \emph{Tok v~síti $(G, z, s, c)$} je každá funkce $f\colon{}E \rightarrow{} \mathbb{R} _0^+$ splňující:
     \begin{itemize}
-        \item Pro každou hranu e \in{} E platí 0 \le{} f(e) \le{} f(c).
-        \item Pro každý vrchol u \in{} V mimo zdroj a stok platí: 
+        \item Pro každou hranu e \in{} E platí 0 \le{} f(e) \le{} c(e).
+        \item Pro každý vrchol u \in{} V mimo zdroj a~stok platí: 
     \end{itemize}
     \[ \sum_{(x, u)\in{}E} f(x, u) = \sum_{(u, y)\in{}E} f(u,y)  \] 
 \end{definition}
@@ -60,11 +60,11 @@ někdy ji zkráceně značíme uv.
     \[ w(f) = \sum_{(z, x)\in{}E} f(z, x) - \sum_{(x, z)\in{}E} f(x, z)  \]
 \end{definition}
-Pozor na to, že u orientovaných grafů se pojem zdroj používá pro libovolný vrchol, do nějž nevedou žádné hrany. Zdrojem v síti se označuje právě jeden vrchol a hrany do něj dovolujeme. Analogicky pro stok.~\cite{PruvodceLab}
-Síť si lze představovat jako soustavu jednosměrných vodovodních trubek, kde každá má svojí šířku, která určuje kolik vody lze danou trubkou transportovat. Každá trubka tedy může být různě veliká a propouštět různé množství vody, zároveň několik trubek se může setkat v jednom místě, takovému místu budeme říkat vrchol. Vrchol má tedy za úkol pouze trubky spojit tak, aby žádná voda nevytekla a sám žádnou vodu neudržoval, síť tedy ,,těsní"\footnote{Také známe jako Kirchhoffův zákon.}. Dále má dvě vyznačená místa -- zdroj a stok. Ve zdroji pouštíme vodu dovnitř a ve stoku voda vytéká ven. Tok je poté rozvržení, kterými trubkami voda proudí a jakou intenzitou. 
-\begin{definition} [Průtok v síti~\cite{PruvodceLab}] \label{def:prutSit}
+Pozor na to, že u orientovaných grafů se pojem zdroj používá pro libovolný vrchol, do nějž nevedou žádné hrany. Zdrojem v~síti se označuje právě jeden vrchol a~hrany do něj dovolujeme. Analogicky pro stok.~\cite{PruvodceLab}
+Síť si lze představovat jako soustavu jednosměrných vodovodních trubek, kde každá má svojí šířku, která určuje kolik vody lze danou trubkou transportovat. Každá trubka tedy může být různě veliká a~propouštět různé množství vody, zároveň několik trubek se může setkat v~jednom místě, takovému místu budeme říkat vrchol. Vrchol má tedy za úkol pouze trubky spojit tak, aby žádná voda nevytekla a~sám žádnou vodu neudržoval, síť tedy ,,těsní"\footnote{Také známe jako Kirchhoffův zákon.}. Dále má dvě vyznačená místa -- zdroj a~stok. Ve zdroji pouštíme vodu dovnitř a~ve stoku voda vytéká ven. Tok je poté rozvržení, kterými trubkami voda proudí a~jakou intenzitou. 
+\begin{definition} [Průtok v~síti~\cite{PruvodceLab}] \label{def:prutSit}
     Každé hraně uv přiřadíme její \emph{průtok} f*(uv) = f(uv) − f(vu).
 \end{definition}
 \begin{remark} \label{poz:vlastPrut}
@@ -72,22 +72,22 @@ Síť si lze představovat jako soustavu jednosměrných vodovodních trubek, kd
     \begin{enumerate}
         \item f*(uv) = −f*(vu)
         \item f*(uv) \le{} c(uv)
-        \item f*(uv) \geq{} -c(uv)
+        \item f*(uv) \geq{} −c(uv)
         \item pro všechny vrcholy v, kde v \neq{} z,s platí: \[ \sum_{u:uv\in{}E}f^*(uv) = 0 \]
     \end{enumerate}
 \end{remark}
 \begin{definition} [Rezerva hrany~\cite{PruvodceLab}] \label{def:rezHra}
-    \emph{Rezerva hrany} uv k toku f v síti S = $(G, z, s, c)$ je číslo r(uv) := c(uv) − f(uv) + f(vu). Hraně s nulovou rezervou budeme říkat \emph{nasycená}, hraně s kladnou rezervou \emph{nenasycená}. O cestě řekneme, že je nasycená, pokud je nasycená alespoň jedna její hrana; jinak mají všechny hrany kladné rezervy a cesta je nenasycená.
+    \emph{Rezerva hrany} uv k toku f v~síti S = $(G, z, s, c)$ je číslo r(uv) := c(uv) − f(uv) + f(vu). Hraně s~nulovou rezervou budeme říkat \emph{nasycená}, hraně s~kladnou rezervou \emph{nenasycená}. O cestě řekneme, že je nasycená, pokud je nasycená alespoň jedna její hrana; jinak mají všechny hrany kladné rezervy a~cesta je nenasycená.
 \end{definition}
 \begin{definition} [Síť rezerv~\cite{PruvodceLab}] \label{def:sitRezer}
-    \emph{Síť rezerv} k toku f v síti S = (G, z, s, c) je síť R(S, f)~:=~(G,~z,~s,~r), kde r(e) je rezerva hrany e při toku f.
+    \emph{Síť rezerv} k toku f v~síti S = (G, z, s, c) je síť R(S, f)~:=~(G,~z,~s,~r), kde r(e) je rezerva hrany e při toku f.
 \end{definition}
 \section{Problém maximálního toku}
-Problém maximálního toku si tedy můžeme zadefinovat jako nalezení způsobu jak nejlépe směrovat médium ze zdroje do stoku, tak abychom dosáhli maximálního toku v dané síti. Všimněme si, že může existovat několik způsobů jak maximálního toku dosáhnout obrázek~\ref{fig:sitVicToku}. Zároveň maximální tok se může rovnat nule, pokud neexistuje cesta složená z hran o kladné kapacitě ze zdroje do stoku obrázek~\ref{fig:sitTokuNula}.
+Problém maximálního toku si tedy můžeme zadefinovat jako nalezení způsobu jak nejlépe směrovat médium ze zdroje do stoku, tak abychom dosáhli maximálního toku v~dané síti. Všimněme si, že může existovat několik způsobů jak maximálního toku dosáhnout obrázek~\ref{fig:sitVicToku}. Zároveň maximální tok se může rovnat nule, pokud neexistuje cesta složená z~hran o kladné kapacitě ze zdroje do stoku obrázek~\ref{fig:sitTokuNula}.
 \begin{figure}[ht]
     \centering
     \begin{minipage}[c]{0.4\textwidth}
@@ -135,18 +135,18 @@ Problém maximálního toku si tedy můžeme zadefinovat jako nalezení způsobu
 \begin{itemize}
     \item Ford–Fulkersonův algoritmus~\cite{FordFulEx}
     
-    Ford–Fulkersonův algoritmus je založen na jednoduché myšlence, mějme nulový tok a zlepšujme ho, dokud je to možné a tím dostaneme maximální tok. Jinými slovy tento algoritmus vyhledává nenasycenou cestu z-s, přidá minimální tok, který tuto cestu nasytí a poté proces opakuje dokud další cestu z-s nenajde. To ale přímo nezaručuje správnost, může se stát, že zasytí cestu, která v jiném pořadí by zvětšila aktuální tok a je zapotřebí pro nalezení maximálního toku. Algoritmus tento problém řeší pomocí jednoduchého triku, a to možnost zmenšovat aktuální tok při průchodu proti směru hrany. Neboli přidáme do naší sítě rezervy hrany podle definicí~\ref{def:rezHra}~a~\ref{def:sitRezer}. Více si o Ford–Fulkersonův algoritmu a jeho využití si můžete přečíst v této práci 
+    Ford–Fulkersonův algoritmus je založen na jednoduché myšlence, mějme nulový tok a~zlepšujme ho, dokud je to možné a~tím dostaneme maximální tok. Jinými slovy tento algoritmus vyhledává nenasycenou cestu z-s, přidá minimální tok, který tuto cestu nasytí a~poté proces opakuje dokud další cestu z-s nenajde. To ale přímo nezaručuje správnost, může se stát, že zasytí cestu, která v~jiném pořadí by zvětšila aktuální tok a~je zapotřebí pro nalezení maximálního toku. Algoritmus tento problém řeší pomocí jednoduchého triku, a~to možnost zmenšovat aktuální tok při průchodu proti směru hrany. Neboli přidáme do naší sítě rezervy hrany podle definicí~\ref{def:rezHra}~a~\ref{def:sitRezer}.
     \item Edmonds-Karpův algoritmus~\cite{EdKarpEx}
-    Edmonds-Karpův algoritmus je velice podobný Ford–Fulkersonovu algoritmu, začíná stejně s nulovým tokem a hledá zlepšující cesty, jenže tentokrát nevybírá náhodnou cestu, ale cestu nejkratší. 
+    Edmonds-Karpův algoritmus je velice podobný Ford–Fulkersonovu algoritmu, začíná stejně s~nulovým tokem a~hledá zlepšující cesty, jenže tentokrát nevybírá náhodnou cestu, ale cestu nejkratší. 
     \item Dinitzův algoritmus 
     
-    Dinitzovu algoritmu se budeme detailněji zabývat v další kapitole \ref{dinitz}, proto ho zde přeskočíme.
+    Dinitzovu algoritmu se budeme detailněji zabývat v~další kapitole \ref{dinitz}, proto ho zde přeskočíme.
     
     \item Goldbergův algoritmus~\cite{GoldEx}
-    Goldbergův algoritmus na začátku nastaví všem vrcholům ,,výšku" a přebytek, výšku si můžeme představit jako třetí osu pro naší síť, tedy doopravdy si můžeme představit síť jako 3D objekt, výška všech vrcholů se ze začátku rovná počtu vrcholů. Přebytek znázorňuje kolik média aktuálně vrchol~v~sobě drží. Algoritmus běží dokud existuje vrchol s přebytkem. V průběhu algoritmus posouvá přebytek po hranách které nevedou do vrcholů které jsou výš. 
-    \item a mnoho dalších jako jsou například algoritm tří indů (MKM)~\cite{MKMEX}, KRT~\cite{KRTEX} nebo algoritmus Kathuria-Liu-Sidford~\cite{KatEX}
+    Goldbergův algoritmus na začátku nastaví všem vrcholům ,,výšku" a~přebytek, výšku si můžeme představit jako třetí osu pro naší síť, tedy doopravdy si můžeme představit síť jako 3D objekt, výška všech vrcholů se ze začátku rovná počtu vrcholů. Přebytek znázorňuje kolik média aktuálně vrchol~v~sobě drží. Algoritmus běží dokud existuje vrchol s~přebytkem. V~průběhu algoritmus posouvá přebytek po hranách které nevedou do vrcholů které jsou výš. 
+    \item a~mnoho dalších jako jsou například algoritm tří indů (MKM)~\cite{MKMEX}, KRT~\cite{KRTEX} nebo algoritmus Kathuria-Liu-Sidford~\cite{KatEX}.
 \end{itemize}
 \begin{table}[ht!]
@@ -155,7 +155,7 @@ Problém maximálního toku si tedy můžeme zadefinovat jako nalezení způsobu
 \begin{tabular}{@{}lll@{}}
 \toprule
 Název algoritmu & Časová složitost & Paměťová složitost \\ \midrule
-Ford-Fulkerson & $O(E \cdot \mathrm{max\_flow})$ & $O(V + E)$ \\
+Ford-Fulkerson & $O(E \cdot \mathrm{max\_tok})$ & $O(V + E)$ \\
 Edmonds-Karp   & $O(V \cdot E^2)$       & $O(V + E)$ \\
 Dinitz's       & $O(V^2 \cdot E)$       & $O(V^2 + E)$ \\
 Push-relabel   & $O(V^2 \cdot E)$           & $O(V^2)$ \\
@@ -173,7 +173,7 @@ King-Rao-Tarjan & $O(V^{\frac{3}{2}} \cdot \log V)$ & $O(V^2)$ \\
 \caption{Porovnání algoritmů pro řešení problému maximálního toku}
 \label{tab:maxFlowTable}
 \begin{tablenotes}
-\item \textbf{Poznámka:} E značí počet hran v grafu, V značí počet vrcholů v grafu a C značí kapacitu hran v grafu.
+\item \textbf{Poznámka:} E značí počet hran v~grafu, V značí počet vrcholů v grafu a~C značí kapacitu hran v~grafu.
 \end{tablenotes}
 \end{threeparttable}
 \end{table}
@@ -182,16 +182,16 @@ King-Rao-Tarjan & $O(V^{\frac{3}{2}} \cdot \log V)$ & $O(V^2)$ \\
 \chapter{Dinitzův algoritmus} \label{dinitz}
 %---------------------------------------------------------------
-Dinitzův algoritmus, také znám jako Dinicův algoritmus je efektivním způsobem pro řešení problému maximálního toku v síti S = (G, z, s, c). Tento algoritmus byl vyvinut Yefimem Dinitzem v roce 1970 a je založen na myšlence používání blokujících toků a pročištěné sítě.
+Dinitzův algoritmus, také znám jako Dinicův algoritmus je efektivním způsobem pro řešení problému maximálního toku v~síti S = (G, z, s, c). Tento algoritmus byl vyvinut Yefimem Dinitzem v~roce 1970 a~je založen na myšlence používání blokujících toků a~pročištěné sítě.
 \begin{definition} [Blokující tok] \label{def:blokTok}
-    \emph{Blokujícím tokem} (ang. Blocking Flow) nazýváme tok, který na každé cestě uv obsahuje alespoň jednu hranu nasycenou, neboli můžeme blokující tok také brát jako tok o minimální velikosti, který nasytí cesty uv z definice \ref{def:rezHra}.
+    \emph{Blokujícím tokem} (ang. Blocking Flow) nazýváme tok, který na každé cestě uv obsahuje alespoň jednu hranu nasycenou, neboli můžeme blokující tok také brát jako tok o minimální velikosti, který nasytí cesty uv z~definice \ref{def:rezHra}.
 \end{definition}
 \begin{definition} [Pročištěná síť~\cite{PruvodceLab} ] \label{def:cistaSit}
-    \emph{Pročištěnou sítí} (ang. Layered network) budeme nazývat síť T = (H, z, s, c), kde H je podgrafem grafu G sítě S = (G, z, s, c) a podgraf H obsahuje pouze vrcholy a hrany, které leží na nejkratší cestách zs. 
+    \emph{Pročištěnou sítí} (ang. Layered network) budeme nazývat síť T = (H, z, s, c), kde H je podgrafem grafu G sítě S = (G, z, s, c) a~podgraf H obsahuje pouze vrcholy a~hrany, které leží na nejkratší cestách zs. 
 \end{definition}
-Jak tedy Dinitzův algoritmus využívá blokující toky a pročištěné sítě? Pokud bychom chtěli najít blokující tok na celé síti, tak podle definice najdeme tok, který nasytí určité hrany tak, aby neexistovala žádná další nenasycená cesta ze zdroje do stoku, neboli našli bychom maximální tok v síti. Z tohoto důvodu nebudeme hledat blokující tok na celé síti, ale na pročištěné síti, pokud se zase zamyslíme co to znamená, tak zjistíme, že dostaneme tok o velikosti rovném součtu kapacit hran tak, aby všechny nejkratší cesty zs byly nasyceny.
-Pokud znova aplikujeme pročištění sítě s novými hranami, které byly nasyceny, tak dostaneme další pročištěnou síť s novými nenasycenými nejkratšími cestami, na které znova najdeme blokující tok a tento postup opakujeme dokud existuje nenasycená cesta zs v síti. Pomocí těchto blokujících toků poté zlepšujeme maximální tok.\\
+Jak tedy Dinitzův algoritmus využívá blokující toky a~pročištěné sítě? Pokud bychom chtěli najít blokující tok na celé síti, tak podle definice najdeme tok, který nasytí určité hrany tak, aby neexistovala žádná další nenasycená cesta ze zdroje do stoku, neboli našli bychom maximální tok v~síti. Z~tohoto důvodu nebudeme hledat blokující tok na celé síti, ale na pročištěné síti, pokud se zase zamyslíme co to znamená, tak zjistíme, že dostaneme tok o velikosti rovné součtu kapacit hran tak, aby všechny nejkratší cesty zs byly nasyceny.
+Pokud znova aplikujeme pročištění sítě s~novými hranami, které byly nasyceny, tak dostaneme další pročištěnou síť s~novými nenasycenými nejkratšími cestami, na které znova najdeme blokující tok a~tento postup opakujeme dokud existuje nenasycená cesta zs v~síti. Pomocí těchto blokujících toků poté zlepšujeme maximální tok.\\
 Postup Dinitzova algoritmu~\cite{PruvodceLab}: \\
 \textit{Vstup: Síť $S = (G, z, s, c)$}
 \begin{itemize}
@@ -199,86 +199,89 @@ Postup Dinitzova algoritmu~\cite{PruvodceLab}: \\
     \item Opakujeme:
     \begin{enumerate}
         \item Sestrojíme pročištěnou síť H ze sítě S.
-        \item Najdeme nejkratší cesty v síti H.
-        \item Pokud žádná taková cesta neexistuje, zastavíme se a vrátíme tok $f$.
+        \item Najdeme nejkratší cesty v~síti H.
+        \item Pokud žádná taková cesta neexistuje, zastavíme se a~vrátíme tok $f$.
         \item $g \leftarrow$ blokující tok v $R$.
         \item Zlepšíme tok $f$ pomocí $g$.
         \item Upravíme aktuální síť S podle toku $g$.
     \end{enumerate}
 \end{itemize}
-Výstup: Maximální tok $f$.
-Dovysvětlíme ještě čištění sítě, jak už jsme zmínili, jedná se o síť tvořenou podgrafem H z grafu G. Způsob jakým můžeme jednoduše pročištěnou síť vytvořit se zakládá na myšlence rozdělení vrcholů sítě do skupin podle vzdálenosti od zdroje. Mějme tedy rozdělené vrcholy do vhodných vrstev, poté odeberme všechny vrstvy, které mají vzdálenost větší než vzdálenost stoku, poté odeberme všechny hrany které vedly do těchto vrcholů, odeberme také všechny hrany které vedou mezi vrcholy stejné vrstvy a hrany které vedou do vrstev bližších ke zdroji. Na konec odeberme všechny vrcholy, z kterých nevede žádná hrana.\footnote{Nasycené hrany, budeme považovat za smazané.} 
+Výstup: Maximální tok $f$.\\
+Dovysvětlíme ještě čištění sítě, jak už jsme zmínili, jedná se o síť tvořenou podgrafem H z~grafu G. Způsob jakým můžeme jednoduše pročištěnou síť vytvořit, se zakládá na myšlence rozdělení vrcholů sítě do skupin podle vzdálenosti od zdroje. Mějme tedy rozdělené vrcholy do
+vhodných vrstev, poté odeberme všechny vrstvy, které mají vzdálenost větší než vzdálenost stoku.
+Dále odeberme všechny hrany které vedly do těchto vrcholů, odeberme také všechny hrany, které
+vedou mezi vrcholy stejné vrstvy a~hrany které vedou do vrstev bližších ke zdroji. Na konec odeberme všechny vrcholy, z~kterých nevede žádná hrana.\footnote{Nasycené hrany, budeme považovat za smazané.} 
 \section{Implementace}
-Existuje několik způsobů implementace Dinitzova algoritmu a volba konkrétní implementace může záviset na programovacím jazyce, použitých datových strukturách a konkrétních požadavcích problému. 
+Existuje několik způsobů implementace Dinitzova algoritmu a~volba konkrétní implementace může záviset na programovacím jazyce, použitých datových strukturách a~konkrétních požadavcích problému. 
 \begin{enumerate}
-    \item \textit{Výběr datových struktur}: Pro efektivní implementaci Dinicova algoritmu je důležité vybrat vhodné datové struktury pro reprezentaci grafu, kapacit hran a toku. Běžně se používají matice sousednosti, seznamy sousedů nebo seznamy hran.
-    \item \textit{Algoritmus pro hledání nejkratší cesty}: Pro konstrukci vrstevnicového grafu je potřeba najít nejkratší cesty od zdroje k ostatním vrcholům v síti. Můžeme použít algoritmy, jako je BFS~\cite{BFSEx} nebo Dijkstrův algoritmus~\cite{DijkEx}, v závislosti na našich požadavcích a omezeních.
-    \item \textit{Hledání blokujícího toku}: Pro hledání blokujícího toku v pročíštěné síti lze použít DFS~\cite{DFSEx} nebo BFS~\cite{BFSEx}z s vhodnými úpravami. V některých implementacích se používají také augmentační cesty nebo push-relabel metoda.
-    \item \textit{Aktualizace toku a kapacity hran}: Po nalezení blokujícího toku je potřeba aktualizovat tok v síti a kapacity hran. To lze provést pomocí jednoduchých cyklů nebo vektorizovaných operací, v závislosti na použitých datových strukturách a programovacím jazyce.
+    \item \textit{Výběr datových struktur}: Pro efektivní implementaci Dinicova algoritmu je důležité vybrat vhodné datové struktury pro reprezentaci grafu, kapacit hran a~toku. Běžně se používají matice sousednosti, seznamy sousedů nebo seznamy hran.
+    \item \textit{Algoritmus pro hledání nejkratší cesty}: Pro konstrukci vrstevnicového grafu je potřeba najít nejkratší cesty od zdroje k ostatním vrcholům v~síti. Můžeme použít algoritmy, jako je BFS~\cite{BFSEx} nebo Dijkstrův algoritmus~\cite{DijkEx}, v~závislosti na našich požadavcích a~omezeních.
+    \item \textit{Hledání blokujícího toku}: Pro hledání blokujícího toku v~pročištěné síti lze použít DFS~\cite{DFSEx} nebo BFS~\cite{BFSEx} s~vhodnými úpravami. V~některých implementacích se používají také augmentační cesty nebo push-relabel metoda.
+    \item \textit{Aktualizace toku a~kapacity hran}: Po nalezení blokujícího toku je potřeba aktualizovat tok v~síti a~kapacity hran. To lze provést pomocí jednoduchých cyklů nebo vektorizovaných operací, v~závislosti na použitých datových strukturách a~programovacím jazyce.
 \end{enumerate}
 \newpage{}
 \section{Použití}
-Dinitzův algoritmus má širokou škálu praktických aplikací v reálném světě. Následující příklady ilustrují některé z jeho současných použití:
+Dinitzův algoritmus má širokou škálu praktických aplikací v~reálném světě. Následující příklady ilustrují některé z~jeho současných použití:
 \begin{enumerate}
-    \item \textit{Optimalizace dopravních sítí \cite{dinitzRoads}}: Algoritmus můžeme použit k optimalizaci dopravních sítí, například pro řízení dopravy ve velkých městech nebo zajištění efektivního rozdělování zásob. Algoritmus může pomoci najít nejlepší rozložení zdrojů a cest, aby byl zajištěn maximální tok zboží či dopravy s minimálními náklady a zpožděním.
-    \item \textit{Řízení vodních zdrojů}: Algoritmus lze aplikovat na řízení vodních zdrojů, jako jsou řeky, přehrady a zavlažovací systémy. Algoritmus může pomoci určit optimální rozdělení vody mezi různé oblasti, aby byla zajištěna maximální účinnost a minimalizace ztrát.
-    \item \textit{Telekomunikace \cite{dinitzNet}}: V oblasti telekomunikací se algoritmus používá pro optimalizaci přenosu dat v sítích a pro řízení zdrojů, jako je šířka pásma nebo kapacita spojení. Algoritmus může napomoci při navrhování sítí tak, aby bylo zajištěno maximální propustnost a minimální zpoždění.
-    \item \textit{Plánování a analýza sítě \cite{dinitzSit}}: Algoritmus můžeme použít pro plánování a analýzu sítě v různých oborech, jako je například výroba, logistika nebo energetika. Algoritmus může pomoci identifikovat úzká hrdla, optimalizovat zdroje a zlepšit celkovou efektivitu sítě.
-    \item \textit{Optimalizace zpracování informací\cite{dinitzProc}}: V oblasti zpracování informací může být algoritmus použit pro optimalizaci paralelního zpracování úkolů, distribuci zdrojů nebo plánování procesů. Algoritmus může napomoci při navrhování systémů tak, aby bylo dosaženo maximálního výkonu a minimálního času zpracování.
+    \item \textit{Optimalizace dopravních sítí \cite{dinitzRoads}}: Algoritmus můžeme použit k optimalizaci dopravních sítí, například pro řízení dopravy ve velkých městech nebo zajištění efektivního rozdělování zásob. Algoritmus může pomoci najít nejlepší rozložení zdrojů a~cest, aby byl zajištěn maximální tok zboží či dopravy s~minimálními náklady a~zpožděním.
+    \item \textit{Řízení vodních zdrojů}: Algoritmus lze aplikovat na řízení vodních zdrojů, jako jsou řeky, přehrady a~zavlažovací systémy. Algoritmus může pomoci určit optimální rozdělení vody mezi různé oblasti, aby byla zajištěna maximální účinnost a~minimalizace ztrát.
+    \item \textit{Telekomunikace \cite{dinitzNet}}: V~oblasti telekomunikací se algoritmus používá pro optimalizaci přenosu dat v~sítích a~pro řízení zdrojů, jako je šířka pásma nebo kapacita spojení. Algoritmus může napomoci při navrhování sítí tak, aby bylo zajištěno maximální propustnost a~minimální zpoždění.
+    \item \textit{Plánování a~analýza sítě \cite{dinitzSit}}: Algoritmus můžeme použít pro plánování a~analýzu sítě v~různých oborech, jako je například výroba, logistika nebo energetika. Algoritmus může pomoci identifikovat úzká hrdla, optimalizovat zdroje a~zlepšit celkovou efektivitu sítě.
+    \item \textit{Optimalizace zpracování informací\cite{dinitzProc}}: V~oblasti zpracování informací může být algoritmus použit pro optimalizaci paralelního zpracování úkolů, distribuci zdrojů nebo plánování procesů. Algoritmus může napomoci při navrhování systémů tak, aby bylo dosaženo maximálního výkonu a~minimálního času zpracování.
 \end{enumerate}
 %---------------------------------------------------------------
 \chapter{Verifikační prostředí Frama-C}
 %---------------------------------------------------------------
-Frama-C je sofistikovaný analytický nástroj založený na frameworku, který je navržen pro analýzu zdrojového kódu napsaného v jazyce C. Tento nástroj byl nejdříve vyvinut pro zlepšení bezpečnosti a provozu jaderných elektráren společností Inria, francouzským národním institutem pro výzkum v oblasti informatiky a matematického modelování, a jeho hlavním cílem dnes je zlepšit kvalitu, bezpečnost a spolehlivost softwaru. Frama-C poskytuje sadu modulárních a rozšiřitelných pluginů, které umožňují provádět různé druhy analýz, jako je formální analýza, statická analýza, abstraktní interpretace, kontrola běhových chyb nebo generování testovacích dat. My budeme framework Frama-C využívat hlavně pro statickou a formální analýzu programu napsaného v jazyce C, budeme také využívat dva z mnoha možných pluginů -- plugin WP a plugin RTE.
+Frama-C je sofistikovaný analytický nástroj založený na frameworku, který je navržen pro analýzu zdrojového kódu napsaného v~jazyce C. Tento nástroj byl nejdříve vyvinut pro zlepšení bezpečnosti a~provozu jaderných elektráren společností Inria, francouzským národním institutem pro výzkum v~oblasti informatiky a~matematického modelování, a~jeho hlavním cílem dnes je zlepšit kvalitu, bezpečnost a~spolehlivost softwaru. Frama-C poskytuje sadu modulárních a~rozšiřitelných pluginů, které umožňují provádět různé druhy analýz, jako je formální analýza, statická analýza, abstraktní interpretace, kontrola~běhových chyb nebo generování testovacích dat. My budeme framework Frama-C využívat hlavně pro statickou~a~formální analýzu programu napsaného v~jazyce C, budeme také využívat dva z~mnoha možných pluginů -- plugin WP a~plugin RTE.
 \section{Plugin WP}
-Plugin WP (Weakest Precondition)~\cite{WPMan} je součástí Frama-C a slouží k formální verifikaci zdrojového kódu napsaného v jazyce C. WP využívá techniku nejslabších předpokladů (ang. weakest preconditions) pro ověření, zda daný program splňuje formální specifikace zapsané v jazyce ACSL (ANSI/ISO C Specification Language). Tato technika spočívá ve vytváření matematických důkazů, které zachycují chování programu a umožňují ověřit splnění požadavků specifikovaných v ACSL.
-WP podporuje různé druhy nástrojů pro automatické i interaktivní důkazy, jako jsou SMT (Satisfiability Modulo Theories) solvery nebo interaktivní důkazové asistenty, například Coq. Plugin WP je navržen tak, aby byl modulární a rozšiřitelný, což umožňuje snadno přidávat podporu pro další důkazové nástroje nebo techniky.
+Plugin WP (Weakest Precondition)~\cite{WPMan} je součástí Frama-C a~slouží k formální verifikaci zdrojového kódu napsaného v~jazyce C. WP využívá techniku nejslabších předpokladů (ang. weakest preconditions) pro ověření, zda daný program splňuje formální specifikace zapsané v~jazyce ACSL (ANSI/ISO C Specification Language). Tato technika spočívá ve vytváření matematických důkazů, které zachycují chování programu a~umožňují ověřit splnění požadavků specifikovaných v~ACSL.
+WP podporuje různé druhy nástrojů pro automatické i interaktivní důkazy, jako jsou SMT (Satisfiability Modulo Theories) solvery nebo interaktivní důkazové asistenty, například Coq. Plugin WP je navržen tak, aby byl modulární a~rozšiřitelný, což umožňuje snadno přidávat podporu pro další důkazové nástroje nebo techniky.
 \section{Plugin RTE} \label{rte}
-Plugin RTE (Runtime Error) je další komponenta Frama-C, která se zaměřuje na kontrolu běhových chyb v programu napsaném v jazyce C. Tento plugin analyzuje zdrojový kód a automaticky generuje ACSL anotace pro kontrolu běhových chyb, jako jsou přetečení čísel, dělení nulou, neplatné ukazatele nebo přístup mimo rozsah pole.
-RTE~\cite{RTEMan} využívá Frama-C framework pro propagaci těchto anotací v kódu a ověření jejich splnění pomocí dostupných analýz a pluginů, jako je WP~\cite{WPMan} nebo E-ACSL~\cite{ERTEMan}. Plugin RTE umožňuje identifikovat potenciální běhové chyby a nebezpečné chování programu, což přispívá ke zlepšení kvality, bezpečnosti a spolehlivosti softwaru.
+Plugin RTE (Runtime Error) je další komponenta Frama-C, která se zaměřuje na kontrolu běhových chyb v~programu napsaném v~jazyce C. Tento plugin analyzuje zdrojový kód a~automaticky generuje ACSL anotace pro kontrolu běhových chyb, jako jsou přetečení čísel, dělení nulou, neplatné ukazatele nebo přístup mimo rozsah pole.
+RTE~\cite{RTEMan} využívá Frama-C framework pro propagaci těchto anotací v~kódu a~ověření jejich splnění pomocí dostupných analýz a~pluginů, jako je WP~\cite{WPMan} nebo E-ACSL~\cite{ERTEMan}. Plugin RTE umožňuje identifikovat potenciální běhové chyby a~nebezpečné chování programu, což přispívá ke zlepšení kvality, bezpečnosti a~spolehlivosti softwaru.
 \newpage{}
-Ověření programu potřebuje nejen framework Frama-C, zvolené pluginy, ale i takzvané řešiče (ang. solver) založené na teorii splnitelnosti modulo teorie (SMT -- satisfiability modulo theories). Tyto řešiče umožňují automatické dokazování vlastností programu, které vycházejí z anotací ve zdrojovém kódu a matematických teorií. Frama-C podporuje několik SMT řešičů, jako jsou Alt-Ergo, CVC4 a Z3. Každý řešič má své specifické vlastnosti a výhody, což nám umožňuje si vybrat nejvhodnější řešič pro konkrétní úlohu ověřování. My budeme v naší práci používat právě zmíněné tři řešiče Alt-Ergo, CVC4 a Z3.
+Ověření programu potřebuje nejen framework Frama-C, zvolené pluginy, ale i takzvané řešiče (ang. solver) založené na teorii splnitelnosti modulo teorie (SMT -- satisfiability modulo theories). Tyto řešiče umožňují automatické dokazování vlastností programu, které vycházejí z~anotací ve zdrojovém kódu a~matematických teorií. Frama-C podporuje několik SMT řešičů, jako jsou Alt-Ergo, CVC4 a~Z3. Každý řešič má své specifické vlastnosti a~výhody, což nám umožňuje si vybrat nejvhodnější řešič pro konkrétní úlohu ověřování. My budeme v~naší práci používat právě zmíněné tři řešiče Alt-Ergo, CVC4 a~Z3.
 \section{Solver Alt-Ergo}
-\emph{Alt-Ergo}~\cite{altEx} je open-source automatický řešič teorií (SMT solver) vyvinutý ve francouzském výzkumném institutu INRIA. Je založen na Satisfiability Modulo Theories (SMT) a je navržen tak, aby podporoval různé datové typy a struktury, včetně celočíselných a reálných aritmetik, polí a typů výčtů. Řešič je napsán v OCaml a lze jej snadno integrovat do ověřovacích platforem softwaru, jako je Frama-C. Používá se v různých aplikacích, jako je například verifikační software Why3~\cite{why3Ex}, programovací jazyk SPARK~\cite{sparkEx} nebo software pro vývoj programů Atelier-B~\cite{Atelier}.
+\emph{Alt-Ergo}~\cite{altEx} je open-source automatický řešič teorií (SMT solver) vyvinutý ve francouzském výzkumném institutu INRIA. Je založen na Satisfiability Modulo Theories (SMT) a~je navržen tak, aby podporoval různé datové typy a~struktury, včetně celočíselných a~reálných aritmetik, polí a~typů výčtů. Řešič je napsán v~OCaml a~lze jej snadno integrovat do ověřovacích platforem softwaru, jako je Frama-C. Používá se v~různých aplikacích, jako je například verifikační software Why3~\cite{why3Ex}, programovací jazyk SPARK~\cite{sparkEx} nebo software pro vývoj programů Atelier-B~\cite{Atelier}.
 \section{Solver CVC4} 
-CVC4~\cite{cvcEx} je široce používaný open-source SMT řešič vyvinutý týmem výzkumníků ze Stanfordské university a Iowa univerzity. Je čtvrtým v řadě řešitelů Cooperating Validity Checker (CVC). CVC4 byl navržen se zaměřením na výkon, škálovatelnost a robustnost a byl úspěšně aplikován v různých projektech ověřování softwaru a formálních metod, mezi jinými byl použit pro ověřovač programů Dafny vyvinutý společností Microsoft Research~\cite{dafnyEx} nebo pro ověření hardwaru sadou nástrojů SymbiYosys~\cite{symbiEx}.
+CVC4~\cite{cvcEx} je široce používaný open-source SMT řešič vyvinutý týmem výzkumníků ze Stanfordské university a~Iowa univerzity. Je čtvrtým v~řadě řešitelů Cooperating Validity Checker (CVC). CVC4 byl navržen se zaměřením na výkon, škálovatelnost a~robustnost a~byl úspěšně aplikován v~různých projektech ověřování softwaru a~formálních metod, mezi jinými byl použit pro ověřovač programů Dafny vyvinutý společností Microsoft Research~\cite{dafnyEx} nebo pro ověření hardwaru sadou nástrojů SymbiYosys~\cite{symbiEx}.
 \section{Solver Z3}
-Z3~\cite{z3Ex} je vysoce výkonný řešič vyvinutý společností Microsoft Research. Řešič je známý svou efektivitou a snadnou integrací, díky čemuž je oblíbenou volbou pro mnoho ověřovacích úloh. Z3 je široce používán při ověřování softwaru, analýze programů a kontrole modelů a byl integrován do mnoha nástrojů a rámců, např. ověřovací infrastruktura Viper~\cite{viperEx} nebo Metatheory of Algebraic Process Theories (Maude) system~\cite{Aceto_2013}, který se používá ke specifikaci a analýze široké škály formálních modelů.
+Z3~\cite{z3Ex} je vysoce výkonný řešič vyvinutý společností Microsoft Research. Řešič je známý svou efektivitou a~snadnou integrací, díky čemuž je oblíbenou volbou pro mnoho ověřovacích úloh. Z3 je široce používán při ověřování softwaru, analýze programů a~kontrole modelů a~byl integrován do mnoha nástrojů a~rámců, např. ověřovací infrastruktura Viper~\cite{viperEx} nebo Metatheory of Algebraic Process Theories (Maude) system~\cite{Aceto_2013}, který se používá ke specifikaci a~analýze široké škály formálních modelů.
 %---------------------------------------------------------------
 \chapter{Anotační jazyk ACSL}
 %---------------------------------------------------------------
-Jedním z klíčových aspektů Frama-C je jeho schopnost provádět formální analýzu pomocí specifikace ACSL (ANSI/ISO C Specification Language)~\cite{ACSLMan}. ACSL je bohatý a výkonný jazyk pro formální analýzu, který umožňuje popsat chování programu a jeho očekávané vlastnosti na základě matematických konstrukcí a logických výrazů. Frama-C dokáže analyzovat zdrojový kód spolu se specifikací ACSL a ověřit, zda kód splňuje dané požadavky. Tímto způsobem je možné odhalit potenciální chyby, nekonzistence nebo nebezpečné chování, které by mohly vést k selhání softwaru nebo bezpečnostním problémům.
+Jedním z~klíčových aspektů Frama-C je jeho schopnost provádět formální analýzu pomocí specifikace ACSL (ANSI/ISO C Specification Language)~\cite{ACSLMan}. ACSL je bohatý a~výkonný jazyk pro formální analýzu, který umožňuje popsat chování programu a~jeho očekávané vlastnosti na základě matematických konstrukcí a~logických výrazů. Frama-C dokáže analyzovat zdrojový kód spolu se specifikací ACSL a~ověřit, zda kód splňuje dané požadavky. Tímto způsobem je možné odhalit potenciální chyby, nekonzistence nebo nebezpečné chování, které by mohly vést k selhání softwaru nebo bezpečnostním problémům.
 \section{Anotace jazyka ACSL}
-Jazyk ACSL umožňuje popsání očekávaného chování programu pomocí kontraktů. Kontrakty se skládají z předpodmínek (ang. preconditions), popisující očekávaný stav před voláním funkce a z následujících podmínek (ang. postconditions), které popisují očekávaný stav po dokončení funkce. Frama-C tak může analyzovat a ověřovat správnost programu, ale i správnost jednotlivých funkcí.
-Jazyk ACSL používá mnoho různých klíčových slov (ang. keywords), kterými kategorizuje tvrzení, která se za nimi nachází. Rychle zde uvedeme a lehce vysvětlíme některá klíčová slova, které budeme používat v našem ověření Dinitzova algoritmu používat.
+Jazyk ACSL umožňuje popsání očekávaného chování programu pomocí kontraktů. Kontrakty se skládají z~předpodmínek (ang. preconditions), popisující očekávaný stav před voláním funkce a~z následujících podmínek (ang. postconditions), které popisují očekávaný stav po dokončení funkce. Frama-C tak může analyzovat a~ověřovat správnost programu, ale i správnost jednotlivých funkcí.
+Jazyk ACSL používá mnoho různých klíčových slov (ang. keywords), kterými kategorizuje tvrzení, která se za nimi nachází. Rychle zde uvedeme a~lehce vysvětlíme některá klíčová slova, které budeme používat v~našem ověření Dinitzova algoritmu používat.
   \begin{itemize} \label{frama:keywords}
   \item \emph{@requires}: Specifikuje předpoklady, které musí být splněny před zavoláním funkce. Tato klauzule se používá k omezení stavů, ve kterých může být funkce bezpečně volána. Předpoklady mohou zahrnovat podmínky na vstupních hodnotách nebo stavech objektů.
   \item \emph{@ensures}: Popisuje podmínky, které musí být splněny po úspěšném ukončení funkce. Tyto podmínky mohou zahrnovat očekávané výsledky nebo změny stavu.
   \item \emph{@assigns}: Udává, jaké proměnné mohou být změněny funkcí. Tato klauzule je důležitá pro omezení účinků funkce na její okolí.
-  \item \emph{@allocates}: Popisuje paměť, kterou funkce alokuje. Tato klauzule je užitečná pro sledování alokace paměti a její správné uvolnění.
+  \item \emph{@allocates}: Popisuje paměť, kterou funkce alokuje. Tato klauzule je užitečná pro sledování alokace paměti a~její správné uvolnění.
   \item \emph{@frees}: Popisuje paměť, kterou funkce uvolňuje. Tato klauzule je důležitá pro zajištění, že všechna alokovaná paměť je správně uvolněna.
-  \item \emph{@loop\_invariant}: Popisuje podmínky, které musí být splněny před a po každé iteraci smyčky. Pokud bychom vzali ukázkový kód \ref{ex:loopC}, tak jako invariant cyklu bychom napsali $0 \leq a  < 10 $, tedy celkem jako /*@ loop invariant 0 <= a <= 10; @*/. Jak tedy vidíme, invarianta musí také obsahovat hodnotu i po skončení cyklu.
-  \item \emph{@loop\_assigns}: Udává, jaké proměnné mohou být změněny smyčkou. Z ukázkového kódu \ref{ex:loopC}, by se jednalo o dvě proměnné: \emph{a} a \emph{i}.
-  \item \emph{@loop\_variant}: Udává funkci, která klesá při každé iteraci smyčky a je nezáporná. Pro náš ukázkový kód \ref{ex:loopC} máme více možností, např.\\ /*@ loop variant 10 - i;@*/ nebo 
+  \item \emph{@loop\_invariant}: Popisuje podmínky, které musí být splněny před a~po každé iteraci smyčky. Pokud bychom vzali ukázkový kód \ref{ex:loopC}, tak jako invariant cyklu bychom napsali $0 \leq a < 10 $, tedy celkem jako /*@ loop invariant 0 <= a <= 10; @*/. Jak tedy vidíme, invarianta musí také obsahovat hodnotu i po skončení cyklu.
+  \item \emph{@loop\_assigns}: Udává, jaké proměnné mohou být změněny smyčkou. Z~ukázkového kódu \ref{ex:loopC}, by se jednalo o dvě proměnné: \emph{a} a~\emph{i}.
+  \item \emph{@loop\_variant}: Udává funkci, která klesá při každé iteraci smyčky a~je nezáporná. Pro náš ukázkový kód \ref{ex:loopC} máme více možností, např.\\ /*@ loop variant 10 - i;@*/ nebo 
   /*@ loop variant 10 - a;@*/
   \item \emph{@axiomatic}: Definuje soubor axiómů, které popisují logické vlastnosti, na kterých lze stavět důkazy. Tato klauzule umožňuje vytvářet složitější logické konstrukty pro dokazování vlastností kódu.
-  \item \emph{@axiom}: Definuje jednotlivý axiom, který je součástí axiomatického bloku a popisuje logickou vlastnost.
+  \item \emph{@axiom}: Definuje jednotlivý axiom, který je součástí axiomatického bloku a~popisuje logickou vlastnost.
   \item \emph{@predicate}: Definuje logickou funkci, která může být použita jako nástroj pro ověřování. Predikáty se používají k popisu vlastností nebo stavů, které jsou buď pravdivé nebo nepravdivé.
-  \item \emph{@assert}: Kontroluje, zda je daná podmínka splněna, a pokud ne, generuje chybu ověřování. Tato klauzule je užitečná pro ověřování, že kód v určitých bodech splňuje očekávané podmínky.
-  \item \emph{@logic}: Definuje logickou funkci, která může být použita v axiomatických bloků, predikátů a dalších logických výrazů. Tyto logické funkce mohou být použity k vytváření komplexnějších logických výrazů pro ověřování vlastností kódu.
+  \item \emph{@assert}: Kontroluje, zda je daná podmínka splněna, a~pokud ne, generuje chybu ověřování. Tato klauzule je užitečná pro ověřování, že kód v~určitých bodech splňuje očekávané podmínky.
+  \item \emph{@logic}: Definuje logickou funkci, která může být použita v~axiomatických bloků, predikátů a~dalších logických výrazů. Tyto logické funkce mohou být použity k vytváření komplexnějších logických výrazů pro ověřování vlastností kódu.
   \item \emph{@reads}: Určuje, které proměnné nebo paměťové oblasti může logická funkce číst.
-  \item \emph{@old}: Klíčové slovo se používá v kontextu klauzule @ensures pro označení hodnoty proměnné před zavoláním funkce. To umožňuje srovnání stavu před a po volání funkce.
-  \item \emph{@Post}: Klíčové slovo Post se používá v klauzuli @ensures pro označení podmínek, které by měly platit po skončení funkce.
-  \item \emph{@at}: Klíčové slovo at se používá k označení hodnoty proměnné v určitém bodě programu. Je to užitečné pro popisování chování programu v čase, například při sledování hodnot proměnných v různých částech smyčky.
+  \item \emph{@old}: Klíčové slovo se používá v~kontextu klauzule @ensures pro označení hodnoty proměnné před zavoláním funkce. To umožňuje srovnání stavu před a~po volání funkce.
+  \item \emph{@Post}: Klíčové slovo Post se používá v~klauzuli @ensures pro označení podmínek, které by měly platit po skončení funkce.
+  \item \emph{@at}: Klíčové slovo at se používá k označení hodnoty proměnné v~určitém bodě programu. Je to užitečné pro popisování chování programu v~čase, například při sledování hodnot proměnných v~různých částech smyčky.
   \end{itemize}
 \begin{lstlisting}[language=C, caption={Ukázkový for cyklus v jazyce C}, backgroundcolor=\color{white}, label={ex:loopC}]
@@ -289,23 +292,23 @@ for(int i = 0; i < 10; ++i) {
 \end{lstlisting}
 %---------------------------------------------------------------
-\chapter{Implementace a ověření algoritmu}
+\chapter{Implementace a~ověření algoritmu}
 %---------------------------------------------------------------
-V této kapitole si popíšeme implementaci a ověření Dinitzova algoritmu pro nalezení maximálního toku v síti, který jsme v minule kapitole\ref{dinitz} popsali z teoretické stránky a nyní ho představíme z praktické. Náš Dinitzův algoritmus jsme implementovali v programovacím jazykem C a to z důvodu pozdější verifikace frameworkem Frama-C, který toto vyžaduje. 
-Naši implementaci jsme rozdělili do tří souborů. Soubor main.c, který obsahuje načítání vstupu od uživatele a uložení dat do správné struktury, s kterou dále náš algoritmus pracuje. Hlavičkový soubor dinitz.h, který obsahuje definice pomocných metod a pomocných struktur a jako poslední máme soubor dinitz.c, ve kterém je kód, který implementuje dříve definované funkce z dinitz.h.
+V této kapitole si popíšeme implementaci a~ověření Dinitzova algoritmu pro nalezení maximálního toku v~síti, který jsme v~minule kapitole~\ref{dinitz} popsali z~teoretické stránky a~nyní ho představíme z~praktické. Náš Dinitzův algoritmus jsme implementovali v~programovacím jazykem C a~to z~důvodu pozdější verifikace frameworkem Frama-C, který toto vyžaduje. 
+Naši implementaci jsme rozdělili do tří souborů. Soubor main.c, který obsahuje načítání vstupu od uživatele a~uložení dat do správné struktury, s~kterou dále náš algoritmus pracuje. Hlavičkový soubor dinitz.h, který obsahuje definice pomocných metod a~pomocných struktur a~jako poslední máme soubor dinitz.c, ve kterém je kód, který implementuje dříve definované funkce z~dinitz.h.
 \section{Implementace}
-Nyní si ukážeme kód implementace a přesněji popíšeme rozhodnutí, které vedly k vybraným technikám, které jsme využili. Začneme od souboru main.c, abychom si uvedli jaké data náš algoritmus přijímá a s jakými podmínkami pracujeme.
+Nyní si ukážeme kód implementace a~přesněji popíšeme rozhodnutí, které vedly k vybraným technikám, které jsme využili. Začneme od souboru main.c, abychom si uvedli jaké data náš algoritmus přijímá a~s jakými podmínkami pracujeme.
 \subsection{Main.c}
-Nejdůležitější části souboru main.c je funkce readInput z výpisu kódu \ref{prac:main.c}, tato funkce čte uživatelem zadané data, a poté je ukládá do pro nás vhodné struktury -- matice sousednosti. Zároveň tato funkce hlídá námi předurčené požadavky, neboli chceme aby graf měl alespoň 2 vrcholy, abychom mohli mít zdroj a stok jako dva různé vrcholy. \footnote{Vždycky považujeme první vrchol jako zdroj a poslední vrchol jako stok.}
-Dále jsme si stanovili, že budeme uvažovat grafy pouze o maximálním počtů vrcholů rovném, nebo menším než 300 000. Tuto velikost grafů jsme si vybrali, aby tento kód měl stále využití v reálném světe, ale zároveň aby doba běhu programu byla stále akceptovatelná. 
-Zároveň nám, ale toto rozhodnutí přináší jiné následky. Znamená to pro nás využití dynamicky alokované paměti, abychom mohli graf takové velikosti uložit. S tím se váže nepříjemná vlastnost frameworku Frama-C a to, že klíčová slova pro ověřování frees a alocates z kapitoly \ref{frama:keywords} nejsou implementovány. A proto, jak ještě uvidíme části kódu spojené, nebo úzce spojené s dynamickou alokací paměti nelze plně ověřit.
-Soubor main.c také obsahuje funkci cleanUp, která uvolní paměť, výpis výsledku našeho algoritmu.
+Nejdůležitější části souboru main.c je funkce readInput z~výpisu kódu \ref{prac:main.c}, tato funkce čte uživatelem zadané data, a~poté je ukládá do pro nás vhodné struktury -- matice sousednosti. Zároveň tato funkce hlídá námi předurčené požadavky, neboli chceme aby graf měl alespoň 2 vrcholy, abychom mohli mít zdroj a~stok jako dva různé vrcholy.\footnote{Vždycky považujeme první vrchol jako zdroj a~poslední vrchol jako stok.}
+Dále jsme si stanovili, že budeme uvažovat grafy pouze o maximálním počtů vrcholů rovném, nebo menším než 300 000. Tuto velikost grafů jsme si vybrali, aby tento kód měl stále využití v~reálném světe, ale zároveň aby doba běhu programu byla stále akceptovatelná. 
+Zároveň nám, ale toto rozhodnutí přináší jiné následky. Znamená to pro nás využití dynamicky alokované paměti, abychom mohli graf takové velikosti uložit. S~tím se váže nepříjemná vlastnost frameworku Frama-C a~to, že klíčová slova pro ověřování frees a~alocates z~kapitoly \ref{frama:keywords} nejsou implementovány. A~proto, jak ještě uvidíme části kódu spojené, nebo úzce spojené s~dynamickou alokací paměti nelze plně ověřit.
+Soubor main.c zajišťuje výpis výsledku našeho algoritmu a dále obsahuje funkci cleanUp, která uvolní paměť.
 \newpage{}
 \begin{lstlisting}[language=C, caption={Soubor main.c}, backgroundcolor=\color{white}, label={prac:main.c}]
 int readInput( double ***graph)
@@ -356,13 +359,13 @@ int readInput( double ***graph)
 \end{lstlisting}
 \newpage{}
 \subsection{Dinitz.h/Dinitz.c}
-Nyní si popíšeme hlavní soubory našeho programu. Začneme od nejdůležitější funkce dinitzMaxFlow  \ref{prac:dinitz} a budeme pomalu představovat další pomocné funkce. Naše hlavní funkce jako první připraví další pole určené pro pamatování si úrovní vrcholů a zavolá BFS \ref{prac:BFS}, kterému toto pole předá. 
-BFS má za úkol prohledat do šířky zadaný graf, nastavit úrovně všech dostupných vrcholů a~tedy~i~zjistit zda existuje cesta zs. BFS také využívá naší pomocnou strukturu Node \ref{prac:Node} a funkce insertHead \ref{prac:insert} a popHead \ref{prac:pop}, které společně simulují frontu pomocí spojového seznamu.
-Po návratu BFS, pokud existuje cesta zs, tak opakovaně voláme funkci DFS \ref{prac:DFS}. Naše prohledávání do hloubky je trochu upravené, dovolujeme DFS cestovat pouze po hranách, které vedou z vrcholu o nižší úrovni do vrcholu s úrovni o jedna vyšší. Zároveň si pamatujeme cestu, kterou jsme přišli, navštívené vrcholy a velikost toku, který se rovná nejmenší kapacitě hrany na cestě zs. DFS poté upravuje aktuální graf a maže hrany, které jsou nasyceny.
-V naší implementaci tedy nevytváříme pročištěnou síť, ale pouze přiřazujeme úrovně a mažeme nasycené hrany. Pro DFS to znamená, že může prohledávat delší dobu, protože nemažeme slepé uličky, ale zvolili jsme tento postup, abychom se vyhnuli dalším alokacím dynamické paměti, které vytváří problémy s ověřovacím frameworkem.
+Nyní si popíšeme hlavní soubory našeho programu. Začneme od nejdůležitější funkce dinitzMaxFlow  \ref{prac:dinitz} a~budeme pomalu představovat další pomocné funkce. Naše hlavní funkce jako první připraví další pole určené pro pamatování si úrovní vrcholů a~zavolá BFS \ref{prac:BFS}, kterému toto pole předá. 
+BFS má za úkol prohledat do šířky zadaný graf, nastavit úrovně všech dostupných vrcholů a~tedy~i~zjistit zda existuje cesta zs. BFS také využívá naší pomocnou strukturu Node \ref{prac:Node} a~funkce insertHead \ref{prac:insert} a~popHead \ref{prac:pop}, které společně simulují frontu pomocí spojového seznamu.
+Po návratu BFS, pokud existuje cesta zs, tak opakovaně voláme funkci DFS \ref{prac:DFS}. Naše prohledávání do hloubky je upravené, dovolujeme DFS cestovat pouze po hranách, které vedou z~vrcholu o nižší úrovni do vrcholu s~úrovni o jedna vyšší. Zároveň si pamatujeme cestu, kterou jsme přišli, navštívené vrcholy a~velikost toku, který se rovná nejmenší kapacitě hrany na cestě zs. DFS poté upravuje aktuální graf a~maže hrany, které jsou nasyceny.
+V naší implementaci tedy nevytváříme pročištěnou síť, ale pouze přiřazujeme úrovně a~mažeme nasycené hrany. Pro DFS to znamená, že může prohledávat delší dobu, protože nemažeme slepé uličky, ale zvolili jsme tento postup, abychom se vyhnuli dalším alokacím dynamické paměti, které vytváří problémy s~ověřovacím frameworkem.
 \begin{lstlisting}[language=C, caption={kód funkce Dinitz Max Flow}, backgroundcolor=\color{white}, label={prac:dinitz}]
@@ -483,9 +486,9 @@ void insertHead(Node** head_ref, int new_data) {
 }
 \end{lstlisting}
 \section{Ověření}
-Nyní už máme naší implementaci kódu a chceme jí ověřit, zavedeme tedy do kódu anotace jazyka ACSL, takové anotace uvádíme pomocí znaků /*@ a @*/. Vlastně se jedná o blokové komentáře programovacího jazyka C doplněné o znak @. Pokud anotace jsou na více řádků tak nemusíme na začátek každého řádku uvádět @, ale my to tak budeme dělat, aby bylo jasné kde máme anotace pro framework Frama-C.
-Nyní už začneme s uváděním funkcí a jejich kontraktů, začneme od menších funkcí, kde kontrakty bývají jednodušší a budeme se posouvat k funkcím složitějším, které často závisí na předešlých funkcích.
+Nyní už máme naší implementaci kódu a~chceme jí ověřit, zavedeme tedy do kódu anotace jazyka ACSL, takové anotace uvádíme pomocí znaků /*@ a~@*/. Jedná se o blokové komentáře programovacího jazyka C doplněné o znak @. Pokud anotace jsou na více řádků tak nemusíme na začátek každého řádku uvádět @, ale my to tak budeme dělat, aby bylo jasné kde máme anotace pro framework Frama-C.
+Nyní už začneme s~uváděním funkcí a~jejich kontraktů, začneme od menších funkcí, kde kontrakty bývají jednodušší a~budeme se posouvat k funkcím složitějším, které často závisí na předešlých funkcích.
 \subsection{Funkce insertHead}
 \begin{lstlisting}[language=C, caption={anotace insertHead}, backgroundcolor=\color{white}, label={ver:insert}]
@@ -501,15 +504,15 @@ void insertHead(Node **head_ref, int new_data){
 }
 \end{lstlisting}
-Popišme anotace funkce insertHead, funkce požaduje, aby ukazatel head\_ref byl validní a zároveň se nerovnal null, to pro nás znamená že chceme, aby paměť, na kterou ukazatel ukazuje byla validní ke čtení a zapisování.
-Dále funkce zajišťuje, že hodnota head\_ref nebude null a zároveň že složka data v Node, na který ukazuje se bude rovnat parametru new\_data, který tato funkce dostala a složka next se bude rovnat staré hodnotě *head\_ref, neboli bude to ukazatel na další prvek v seznamu. 
-Klíčová slova fresh a separated nám pouze říkají, že head\_ref ukazuje na nově alokovaný blok o velikosti Node, a že bloky paměti na které ukazují head\_ref a starý head\_ref se nepřekrývají. 
-Dále máme informaci o tom, že tato funkce alokuje paměť, na kterou ukazuje head\_ref a jako poslední máme klauzuli assigns, která nám říká, že tato funkce manipuluje s pamětí, v tomto případě proměnných *head\_ref, (*head\_ref)->data a (*head\_ref)->next.
-Pokud se pokusíme ověřit pouze tuto část programu tak dostaneme upozornění z obrázku \ref{img:dynMemErr} a část našeho kódu nebude možné z tohoto důvodu ověřit. \ref{img:verIns}
+Popišme anotace funkce insertHead, funkce požaduje, aby ukazatel head\_ref byl validní a~zároveň se nerovnal null, to pro nás znamená, že chceme, aby paměť, na kterou ukazatel ukazuje byla validní ke čtení a~zapisování.
+Dále funkce zajišťuje, že hodnota head\_ref nebude null a~zároveň, že složka data v~Node, na který ukazuje se bude rovnat parametru new\_data, který tato funkce dostala a~složka next se bude rovnat staré hodnotě *head\_ref, neboli bude to ukazatel na další prvek v~seznamu. 
+Klíčová slova fresh a~separated nám pouze říkají, že head\_ref ukazuje na nově alokovaný blok o velikosti Node, a~že bloky paměti na které ukazují head\_ref a~starý head\_ref se nepřekrývají. 
+Dále máme informaci o tom, že tato funkce alokuje paměť, na kterou ukazuje head\_ref a~jako poslední máme klauzuli assigns, která nám říká, že tato funkce manipuluje s~pamětí, v~tomto případě proměnných *head\_ref, (*head\_ref)->data a~(*head\_ref)->next.
+Pokud se pokusíme ověřit pouze tuto část programu tak dostaneme upozornění z~obrázku \ref{img:dynMemErr} a~část našeho kódu nebude možné z~tohoto důvodu ověřit. \ref{img:verIns}
 \begin{figure}[ht!]
     \centering
     \includegraphics[width=14cm]{pictures/frama-c-memory-messages.PNG}
@@ -541,19 +544,19 @@ void popHead(Node** head_ref) {
 }
 \end{lstlisting}
-Nyní si ukažme anotace funkce popHead, na první pohled vidíme část anotací, které se v minulé funkci neobjevily. Jedná se o anotace predicate, jak už jsme zmínili dříve v kapitole \ref{frama:keywords} tato anotace nás informuje o funkci, která může být použitá k ověřování. 
-V~tomto případě se jedná o funkci, která dostane hlavičku naší fronty v podobě spojového seznamu a rekurzivně se volá na další prvky dokud nenarazí na null a v každém kroku kontroluje, zda je možné číst a zapisovat do daného prvku fronty. 
-Dále máme již nám známe anotace ohledně požadování validních vstupních parametrů funkce a použití zmíněné predicate funkce ke kontrole fronty. Anotace nám také říkají, že funkce mění proměnnou *head\_ref, uvolňuje paměť na kterou ukazovala dřívější hodnota *head\_ref.
-V části anotací, kde máme, co funkce zaručuje dostáváme nové klíčové slovo at, které nám říká, že  se koukneme na hodnotu dané proměnné až po daném bodě v kódu, který označíme pomocí štítku, v tomto případě Post. 
-Slovo at, ale už tak doopravdy známe, pokud se podíváme na slovo old(x), tak se vlastně jedná pouze o zkrácenou formu at(x, Old). Slovo old už jsme vysvětlili, že se jedná o hodnotu proměnné před provedením kódu funkce a slovíčko Post je jejím opakem, tedy hodnota po skončení funkce. Celkově tedy zaručujeme, že poté co funkce skončí tak hodnota *head\_ref se rovná ukazateli na další prvek z minulé hlavičky.
-A jako poslední, že paměť, na kterou ukazovala stará hodnota *head\_ref nyní už není validní, neboli nemůžeme jí číst ani do ní psát. V programovacím jazyce C, všechny tyto vlastnosti vyjadřujeme funkcí free.
-Nyní už můžeme ověřit naší funkci popHead obrázek~\ref{img:verPop}, očekáváme podobné výsledky jako s funkcí insertHead, protože nadále pracujeme s dynamickou alokací paměti. Zároveň si ukážeme jak Frama-C transformuje námi dodané anotace a také jak plugin RTE~\ref{rte} přidává vlastní ověřovací anotace obrázek~\ref{img:popFramaCode}.
+Nyní si ukažme anotace funkce popHead, na první pohled vidíme část anotací, které se v~minulé funkci neobjevily. Jedná se o anotace predicate, jak už jsme zmínili dříve v~kapitole \ref{frama:keywords} tato anotace nás informuje o funkci, která může být použitá k ověřování. 
+V~tomto případě se jedná o funkci, která dostane hlavičku naší fronty v~podobě spojového seznamu a~rekurzivně se volá na další prvky dokud nenarazí na null a~v každém kroku kontroluje, zda je možné číst a~zapisovat do daného prvku fronty. 
+Dále máme již nám známe anotace ohledně požadování validních vstupních parametrů funkce a~použití zmíněné predicate funkce ke kontrole fronty. Anotace nám také říkají, že funkce mění proměnnou *head\_ref, uvolňuje paměť na kterou ukazovala dřívější hodnota *head\_ref.
+V části anotací, kde máme, co funkce zaručuje dostáváme nové klíčové slovo at, které nám říká, že  se koukneme na hodnotu dané proměnné až po daném bodě v~kódu, který označíme pomocí štítku, v~tomto případě Post. 
+Slovo at, ale už tak doopravdy známe, pokud se podíváme na slovo old(x), tak se jedná pouze o zkrácenou formu at(x, Old). Slovo old už jsme vysvětlili, že se jedná o hodnotu proměnné před provedením kódu funkce a~slovíčko Post je jejím opakem, tedy hodnota po skončení funkce. Celkově tedy zaručujeme, že poté co funkce skončí tak hodnota *head\_ref se rovná ukazateli na další prvek z~minulé hlavičky.
+A jako poslední, že paměť, na kterou ukazovala stará hodnota *head\_ref nyní už není validní, neboli nemůžeme jí číst ani do ní psát. V~programovacím jazyce C, všechny tyto vlastnosti vyjadřujeme funkcí free.
+Nyní už můžeme ověřit naší funkci popHead obrázek~\ref{img:verPop}, očekáváme podobné výsledky jako s~funkcí insertHead, protože nadále pracujeme s~dynamickou alokací paměti. Zároveň si ukážeme jak Frama-C transformuje námi dodané anotace a~také jak plugin RTE~\ref{rte} přidává vlastní ověřovací anotace obrázek~\ref{img:popFramaCode}.
 \begin{figure}[ht!]
     \centering
@@ -569,7 +572,7 @@ Nyní už můžeme ověřit naší funkci popHead obrázek~\ref{img:verPop}, oč
     \label{img:popFramaCode}
 \end{figure}
-Na obrázku~\ref{img:popFramaCode} je vidět jak předpoklady pro funkci jsou brané jako správné, ale nebyly dokazované, protože aktuálně ověřujeme osamocený kód. V těle funkce bylo dokázáno, že vstupní parametr head\_ref ukazuje na paměť, kterou lze číst a také do ní zapisovat. To nám vychází z předpokladů, ale jen co se dostaneme na ověření uvolnění paměti, tak nám Frama-C oznamuje, že se o ověření pokusilo, ale nedokáže vrátit úspěch ani neúspěch. A tedy ani další notace závisející na správnosti těchto výroků nemohou býti dokázány.
+Na obrázku~\ref{img:popFramaCode} je vidět jak předpoklady pro funkci jsou brané jako správné, ale nebyly dokazované, protože aktuálně ověřujeme osamocený kód. V~těle funkce bylo dokázáno, že vstupní parametr head\_ref ukazuje na paměť, kterou lze číst a~také do ní zapisovat. To nám vychází z~předpokladů, ale jen co se dostaneme na ověření uvolnění paměti, tak nám Frama-C oznamuje, že se o ověření pokusilo, ale nedokáže vrátit úspěch ani neúspěch. A~tedy ani další notace závisející na správnosti těchto výroků nemohou býti dokázány.
 \subsection{Funkce DFS}
 \begin{lstlisting}[language=C, caption={anotace DFS}, backgroundcolor=\color{white}, label={ver:dfs}]
@@ -596,17 +599,17 @@ double DFS (int cur, int end, double **graph, int *levels, int *visited,
 ...
 }
 \end{lstlisting}
-Začínáme se dostávat ke složitějším funkcím, jednou z nich je DFS výpis kódu~\ref{prac:DFS}, která je volaná z naší hlavní funkce dinitzMaxFlow. Začneme klasicky od požadavků funkce, DFS od nás vyžaduje aby index aktuálního vrcholu byl menší, nebo roven indexu stoku, který má být menší než 300 000\footnote{Jakožto pole se čísluje od 0, tak pro nás maximální index se bude rovnat 299 999.}, což byla námi stanovena horní hranice počtu vrcholů v grafu. Funkce také očekává nezáporný tok a validní matici sousednosti, která zobrazuje náš graf, validní pole držící úrovně vrcholů a také validní pole již navštívených vrcholů. 
-Dále říkáme, že funkce DFS pouze mění obsah pole s naším grafem a pole navštívených vrcholů. DFS v našem případě zaručuje, že výsledek bude nezáporný a pokud je větší jak nula, tak pro všechny hrany z aktuálního vrcholů platí, že jejich hodnota bude menší nebo rovná minulé. Neboli pokud toto řekneme více se znalostí našeho algoritmu, tak říkáme, že pokud nalezneme zlepšující tok zs, tak rezervy hran vrcholů, kterými tento tok vede, se může pouze zmenšit.
-Nyní nám už v této funkci zbývají pouze anotace pro cyklus, cykly bývají pro framework frama-C velice těžké na ověření, proto přidáváme anotace, které s tím pomáhají, jednotlivá klíčová slova s příkladem jsme již trochu vysvětlovali na ukázkovém kódu \ref{ex:loopC}, tedy zde budeme psát jejich význam pro ověření.
-Prvně uvádíme proměnné, které se během cyklu mohou měnit nebo musí splňovat jisté podmínky, tyto podmínky budou kontrolovány vždy na začátku a na konci jednoho cyklu. Zde tedy uvádíme proměnnou i, která je řídící proměnnou cyklu a proměnnou flow, od které požadujeme aby byla nezáporná. 
-Dále říkáme jaké proměnné cyklus může měnit a jako poslední uvádíme číselnou hodnotu, která se z každým cyklem bude zmenšovat a je rovná, nebo větší maximálnímu počtu iterací daného cyklu. My jsme si zde vybrali počet vrcholů, protože je to přesný odhad, ale stejně tak bychom mohli říci, že varianta cyklu bude 300 000 - i, protože víme, že naše implementace nebude mít více jak 300 000 vrcholů a tento cyklus prochází všechny hrany daného vrcholu.
-Ověřme tedy naší implementaci funkce DFS obrázek~\ref{img:verDFS} a zjistíme, že většina této funkce bude úspěšně ověřená, stalo se tak, protože ve funkci DFS pracujeme velice minimálně s proměnnými, které jsou dynamicky alokované.
+Začínáme se dostávat ke složitějším funkcím, jednou z~nich je DFS výpis kódu~\ref{prac:DFS}, která je volaná z~naší hlavní funkce dinitzMaxFlow. Začneme od požadavků funkce, DFS od nás vyžaduje aby index aktuálního vrcholu byl menší, nebo roven indexu\footnote{Protože pole se čísluje od 0, tak pro nás maximální index se bude rovnat 299 999.}  stoku, který má být menší než 300 000,což byla námi stanovena horní hranice počtu vrcholů v~grafu. Funkce také očekává nezáporný tok a~validní matici sousednosti, která zobrazuje náš graf, validní pole držící úrovně vrcholů a~také validní pole již navštívených vrcholů. 
+Dále říkáme, že funkce DFS pouze mění obsah pole s~naším grafem a~pole navštívených vrcholů. DFS v~našem případě zaručuje, že výsledek bude nezáporný a~pokud je větší jak nula, tak pro všechny hrany z~aktuálního vrcholů platí, že jejich hodnota bude menší nebo rovná minulé. Což v~kontextu našeho algoritmu znamená, že pokud nalezneme zlepšující tok zs, tak rezervy hran vrcholů, kterými tento tok vede, se může pouze zmenšit.
+Nyní nám už v~této funkci zbývají pouze anotace pro cyklus. Cykly bývají pro framework Frama-C velice těžké na ověření, proto přidáváme anotace, které s~tím pomáhají.
+Prvně uvádíme proměnné, které se během cyklu mohou měnit nebo musí splňovat jisté podmínky, tyto podmínky budou kontrolovány vždy na začátku a~na konci jednoho cyklu. Zde uvádíme proměnnou i, která je řídící proměnnou cyklu a~proměnnou flow, od které požadujeme aby byla nezáporná. 
+Dále říkáme jaké proměnné cyklus může měnit a~na závěr uvádíme číselnou hodnotu, která se s~každým cyklem bude zmenšovat a~je rovná, nebo větší maximálnímu počtu iterací daného cyklu. My jsme si zde vybrali počet vrcholů, protože je to přesný odhad, ale stejně tak bychom mohli říci, že varianta cyklu bude 300 000 - i, protože víme, že naše implementace nebude mít více jak 300 000 vrcholů a~tento cyklus prochází všechny hrany daného vrcholu.
+Ověřme tedy naší implementaci funkce DFS obrázek~\ref{img:verDFS} a~zjistíme, že většina této funkce bude úspěšně ověřená, stalo se tak, protože ve funkci DFS pracujeme velice minimálně s~proměnnými, které jsou dynamicky alokované.
 \begin{figure}[ht!]
     \centering
@@ -668,17 +671,17 @@ int BFS(int start, int end, double **graph, int *levels){
 ...
 }
 \end{lstlisting}
-Funkci BFS už určitě musíme rozebrat po částech, začněme od vrchu, funkce BFS má menší požadavky než funkce DFS, požaduje pouze, aby startovní vrchol neboli zdroj měl menší index než index stoku, a aby stok byl menší než 300 000. Klasicky vyžadujeme validní graf a pole kam můžeme ukládat úrovně vrcholů. 
-Naše BFS pouze upravuje hodnoty pro úrovně vrcholů a poté hlavní funkcionalitou je co vše nám BFS zaručuje. Začneme jednoduše, BFS nám vrací 0 pro nenalezení cesty zs, nebo 1 pokud jsme cestu našli. Druhá vlastnost, kterou nám BFS dává je, že každý vrchol bude mít nastavenou úroveň od -1 až po počet vrcholů - 1. 
-Třetí vlastnost nám říká, že pro každý vrchol, pokud jeho úroveň je -1 po skončení funkce, tak neexistuje hrana mezi vrcholem, který má úroveň vyšší než -1. Neboli BFS nám v teorii grafů zaručuje, že pokud nějaký vrchol nebyl nalezen, tak neexistuje cesta mezi zdrojem a daným vrcholem.
-A poslední vlastnost nám říká, že pokud stok má úroveň vyšší než -1, tak pro každou úroveň existuje vrchol který má hranu, která vede z tohoto vrcholu do vrcholu, který má úroveň o jedna vyšší. Jinými slovy tato vlastnost nám zaručuje, že pokud stok má úroveň vyšší než -1 tak existuje cesta o délce úrovně stoku ze zdroje do stoku. 
-Tedy na rozdíl od předchozího tvrzení, říkáme nejenom, že cesta existuje, ale také tvrdíme, že je dané délky a v tomto případě to také bude délka nejkratší cesty.
-Jakožto ve funkci BFS podle výpisu kódu~\ref{prac:BFS} využíváme také funkce popHead z výpisu kódu~\ref{prac:pop} a insertHead z výpisu kódu~\ref{prac:insert}, tak už nemůžeme prověřit BFS jako osamocený kód, ale musíme ho prověřit společně s těmito funkcemi, tedy většina kódu bude možné verifikovat jak vidíme na obrázku~\ref{img:verBFS}, ale jejich neověřené části se budou propagovat do pozdějších části BFS a znemožňovat další verifikaci.\\
+Funkci BFS už určitě musíme rozebrat po částech, začněme od vrchu, funkce BFS má menší požadavky než funkce DFS, požaduje pouze, aby startovní vrchol, neboli zdroj, měl menší index než index stoku, a~aby stok byl menší než 300 000. Vyžadujeme validní graf a~pole kam můžeme ukládat úrovně vrcholů. 
+Naše BFS pouze upravuje hodnoty pro úrovně vrcholů a~poté hlavní funkcionalitou je, co vše nám BFS zaručuje. Začneme jednoduše, BFS nám vrací 0 pro nenalezení cesty zs, nebo 1 pokud jsme cestu našli. Druhá vlastnost, kterou nám BFS dává je, že každý vrchol bude mít nastavenou úroveň od -1 až po počet vrcholů~-~1. 
+Třetí vlastnost nám říká, že pro každý vrchol, pokud jeho úroveň je -1 po skončení funkce, tak neexistuje hrana mezi vrcholem, který má úroveň vyšší než -1. Neboli BFS nám v~teorii grafů zaručuje, že pokud nějaký vrchol nebyl nalezen, tak neexistuje cesta mezi zdrojem a~daným vrcholem.
+A poslední vlastnost nám říká, že pokud stok má úroveň vyšší než -1, tak pro každou úroveň existuje vrchol který má hranu, která vede z~tohoto vrcholu do vrcholu, který má úroveň o jedna vyšší. Jinými slovy tato vlastnost nám zaručuje, že pokud stok má úroveň vyšší než -1 tak existuje cesta o délce úrovně stoku ze zdroje do stoku. 
+Tedy na rozdíl od předchozího tvrzení, říkáme nejenom, že cesta existuje, ale také tvrdíme, že je dané délky a~v tomto případě to také bude délka nejkratší cesty.
+Protože ve funkci BFS podle výpisu kódu~\ref{prac:BFS} využíváme také funkce popHead z~výpisu kódu~\ref{prac:pop} a~insertHead z~výpisu kódu~\ref{prac:insert}, tak už nemůžeme prověřit BFS jako osamocený kód, ale musíme ho prověřit společně s~těmito funkcemi. Většinu kódu bude možné verifikovat jak vidíme na obrázku~\ref{img:verBFS}, ale jejich neověřené části se budou propagovat do pozdějších části BFS a~znemožňovat další verifikaci.\\
 \begin{figure}[ht!]
     \centering
     \includegraphics[scale=0.95]{pictures/frama-c-BFS.PNG}
@@ -695,7 +698,7 @@ Jakožto ve funkci BFS podle výpisu kódu~\ref{prac:BFS} využíváme také fun
 \end{figure}
-Jak již jsme viděli na obrázku~\ref{img:popFramaCode}, tak i zde Frama-C byla schopná ověřit vše, až do bodu, kdy se střetne s alokací dynamické paměti obrázek~\ref{img:genBFS} a poté nemá možnost ověřit naše tvrzení a přiřazování, protože si není jistá, zda paměť lze číst a modifikovat.
+Jak jsme již viděli na obrázku~\ref{img:popFramaCode}, tak i zde Frama-C byla schopná ověřit vše, až do bodu, kdy se střetne s~alokací dynamické paměti obrázek~\ref{img:genBFS} a~poté nemá možnost ověřit naše tvrzení a~přiřazování, protože si není jistá, zda paměť lze číst a~modifikovat.
 \newpage{}
 \subsection{Funkce dinitzMaxFlow}
@@ -754,25 +757,25 @@ double dinitzMaxFlow(int nodes, double **graph)
     ...
 }
 \end{lstlisting}
-Poslední funkcí, kterou musíme popsat je naše hlavní funkce dinitzMaxFlow, začneme nejdřív axiomem, který později využíváme dál. Axiomatic SumCapacity nám definuje nový axiomatický blok s názvem SumCapacity, poté definujeme logickou funkci sum\_capacity, která bere tři argumenty: dvojrozměrné pole, které udržuje náš graf, číslo nodes, které nám říká počet vrcholů a jako poslední index. Tato logická funkce čte hodnoty z našeho grafu od indexu 0 až po nodes - 1. 
-Nyní již definujeme axiom sum\_capacity\_base, který nám dává základní krok pro funkci sum\_capacity, samotný axiom říká, že pokud nodes je větší nebo rovno nule, tak sum\_capacity pro index 0 je rovno 0. Druhý axiom sum\_capacity\_step, nám definuje rekurzivní krok pro funkci sum\_capacity, kde tvrdíme, že pro každý index, který je mezi 0 a nodes - 1, tak sum\_capacity pro index + 1 je rovná sum\_capacity pro index + hodnota hrany v grafu z vrcholu o indexu 0 do vrcholu o indexu index.
-Pokud tento axiom spojíme s naší reprezentací grafu pomocí matice sousednosti a také toho, že pro nás vrchol o indexu 0 je vždy zdroj, tak tento axiom nám dá součet kapacit všech hran vycházejících ze zdroje. Axiomy můžeme také ověřit jak je vidět na obrázku~\ref{img:verAxiom}.
-Dále tento součet používáme v námi definovaném predikátu valid\_flow, kde říkáme, že výsledek se musí nacházet mezi -1 a součtem kapacit hran včetně z obou stran. Tento predikát poté používáme jako vlastnost kterou dinicMaxFlow funkce splňuje.
-Zbylé anotace už jsou oproti minulé triviální, pouze požadujeme, aby počet vrcholů byl větší než 0 a menší než 300 000 a také požadujeme aby graf byl validní. Nakonec říkáme, že tato funkce může změnit obsah matice udržované v proměnné graph.
-Teď nám už zbývají pouze anotace u cyklů, začneme anotacemi vnitřního cyklu. Nejdříve uvádíme podmínku na proměnnou total, jedná se o náš výsledek, který by měl být vždycky nezáporný. Poté říkáme, že tento cyklus může měnit hodnoty proměnných flow a total, prvky pole visited a prvky matice graph. 
-Jako poslední chceme určit hodnotu varianty grafu, tedy jak omezit shora iterace cyklu, v tomto případě jsme se rozhodli o odečítání aktuálního celkového toku od maximální hodnoty typu double zvětšená o 1000. Dovolili jsme totiž hrany, které nemusí být celá čísla a proto chceme zachytávat i tyto malé změny. Zároveň si myslíme, že tato hodnota bude s každým cyklem klesat, protože DFS najde pokaždé hodnotu o kterou zvětší náš tok, nebo vrátí nulu, která cyklus ukončí.
-Od vnějšího cyklu vyžadujeme, aby proměnná flow byla před a po každé iteraci větší, nebo rovno nule a menší, nebo rovno sumě kapacit hran vycházejících ze zdroje. Tento cyklus také může měnit proměnnou total a prvky polí vertexLevel, graph a visited\footnote{Pole visited zde ještě není alokované, takže nemůžeme určit rozměry stejně jako u ostatních polí.}. 
-Teď už nám zbývá pouze variant vnějšího cyklu, který tentokrát bude celkový počet vrcholů - 1 - úroveň stoku. Pokud se trochu nad tímto zamyslíme, tak v nejhorším případě naše nejkratší cesty se budou s každou iterací prodlužovat o jeden vrchol a to až do doby kdy všechny vrcholy budou potřeba k nalezení nejkratší cesty zs. V této iteraci naše DFS nasytí i tyto cesty a nezbudou již žádné cesty zs a algoritmus skončí. Tedy variant se z každou iterací zmenší alespoň o jedna a bude vždy vetší nebo roven 0.
-Zbývá nám poslední verifikace a to celého kódu obrázek~\ref{img:verDinitz}, jakožto dinitzMaxFlow využívá všech ostatních funkcí.
+Poslední funkcí, kterou musíme popsat je naše hlavní funkce dinitzMaxFlow, začneme nejdřív axiomem, který později využíváme dál. Axiomatic SumCapacity nám definuje nový axiomatický blok s~názvem SumCapacity, poté definujeme logickou funkci sum\_capacity, která bere tři argumenty: dvojrozměrné pole, které udržuje náš graf, číslo nodes, které nám říká počet vrcholů a~jako poslední index. Tato logická funkce čte hodnoty z~našeho grafu od indexu 0 až po nodes~-~1. 
+Nyní již definujeme axiom sum\_capacity\_base, který nám dává základní krok pro funkci sum\_capacity, samotný axiom říká, že pokud nodes je větší nebo rovno nule, tak sum\_capacity pro index 0 je rovno 0. Druhý axiom sum\_capacity\_step, nám definuje rekurzivní krok pro funkci sum\_capacity, kde tvrdíme, že pro každý index, který je mezi 0 a~nodes~-~1, tak sum\_capacity pro index + 1 je rovná sum\_capacity pro index + hodnota hrany v~grafu z~vrcholu o indexu \emph{0} do vrcholu o indexu \emph{index}.
+Pokud tento axiom spojíme s~naší reprezentací grafu pomocí matice sousednosti a~také toho, že pro nás vrchol o indexu 0 je vždy zdroj, tak tento axiom nám dá součet kapacit všech hran vycházejících ze zdroje. Axiomy můžeme také ověřit jak je vidět na obrázku~\ref{img:verAxiom}.
+Dále tento součet používáme v~námi definovaném predikátu valid\_flow, kde říkáme, že výsledek se musí nacházet mezi -1 a~součtem kapacit hran včetně z~obou stran. Tento predikát poté používáme jako vlastnost kterou dinicMaxFlow funkce splňuje.
+Zbylé anotace už jsou oproti minulé triviální, pouze požadujeme, aby počet vrcholů byl větší než 0 a~menší než 300 000 a~také požadujeme aby graf byl validní. Nakonec říkáme, že tato funkce může změnit obsah matice udržované v~proměnné graph.
+Teď nám už zbývají pouze anotace u cyklů, začneme anotacemi vnitřního cyklu. Nejdříve uvádíme podmínku na proměnnou total, jedná se o náš výsledek, který by měl být vždycky nezáporný. Poté říkáme, že tento cyklus může měnit hodnoty proměnných flow a~total, prvky pole visited a~prvky matice graph. 
+Jako poslední chceme určit hodnotu varianty grafu, tedy jak omezit shora iterace cyklu, v~tomto případě jsme se rozhodli o odečítání aktuálního celkového toku od maximální hodnoty typu double zvětšená o 1000. Dovolili jsme totiž hrany, které nemusí být celá čísla a~proto chceme zachytávat i tyto malé změny. Zároveň si myslíme, že tato hodnota bude s~každým cyklem klesat, protože DFS najde pokaždé hodnotu o kterou zvětší náš tok, nebo vrátí nulu, která cyklus ukončí.
+Od vnějšího cyklu vyžadujeme, aby proměnná flow byla před a~po každé iteraci větší, nebo rovno nule a~menší, nebo rovno sumě kapacit hran vycházejících ze zdroje. Tento cyklus také může měnit proměnnou total a~prvky polí vertexLevel, graph a~visited\footnote{Pole visited zde ještě není alokované, takže nemůžeme určit rozměry stejně jako u ostatních polí.}. 
+Teď už nám zbývá pouze variant vnějšího cyklu, který tentokrát bude celkový počet vrcholů - 1 - úroveň stoku. Pokud se nad tímto zamyslíme, tak v~nejhorším případě naše nejkratší cesty se budou s~každou iterací prodlužovat o jeden vrchol a~to až do doby kdy všechny vrcholy budou potřeba k nalezení nejkratší cesty zs. V~této iteraci naše DFS nasytí i tyto cesty a~nezbudou již žádné cesty zs a~algoritmus skončí. Tedy variant se s~každou iterací zmenší alespoň o jedna a~bude vždy vetší nebo roven 0.
+Zbývá nám poslední verifikace a~to celého kódu obrázek~\ref{img:verDinitz}, protože dinitzMaxFlow využívá všech ostatních funkcí.
 \begin{figure}[ht!]
     \centering
     \includegraphics[scale=0.8]{pictures/frama-c-ver-axiom.PNG}
@@ -793,12 +796,12 @@ Zbývá nám poslední verifikace a to celého kódu obrázek~\ref{img:verDinitz
 \markboth{Závěr}{Závěr}
 %---------------------------------------------------------------
-V této práci jsme se věnovali problematice formálního ověření a implementace Dinitzova algoritmu s dynamicky alokovanou pamětí, pro hledání maximálního toku v orientované grafové síti. Podařilo se nám plně implementovat Dinitzův algoritmus v programovacím jazyce C s ACSL anotacemi a také ověřit část kódu, která nepotřebuje prozatím neimplementované výrazy frameworku Frama-C týkajících se dynamické alokace paměti. 
-V prvních dvou kapitolách jsme také čtenáře seznámili s oblastí toků v orientovaných grafech, představili jsme jim mnoho základních pojmů a definic a také plně popsali myšlenku Dinitzova algoritmus pro hledání maximálního toku. Poskytli jsme mu také další zdroje a práce, pokud by se chtěl v tomto tématu dále vzdělávat. 
-Později jsme také uvedli některé možnosti, z mnoha dalších, frameworku Frama-C a doprovázejícímu mu anotačnímu jazyku ACSL, který jsme zde lehce popsali. Zavedli jsme si nástroje, které jsme používali v naší práci, mimo frameworku Frama-C také pluginy WP, RTE a také řešiče Alt-Ergo, CVC4 a Z3. Ke každému z nich jsme dodali lehký popisek a také projekty v kterých byli využiti.
-V praktické části jsme se již plně zaměřili na popsání naší implementace Dinitzova algoritmu a objasnění naších rozhodnutí ohledně výběrů prostředků pro funkčnost našeho algoritmu. Poté jsme se vrhli na vysvětlení a zařazení anotací jazyka ACSL do tématu a problému nalezení maximálního toku v sítích. Řekli jsme si zde také problémy svázané s použitím dynamicky alokované paměti a pozdější verifikací pomocí frameworku Frama-C. 
-Rozšířením této práce by mohlo být porovnání rychlostí ověřeného Dinitzova algoritmu pro hledání maximálního toku a neověřeného Dinitzova algoritmu s využitím programovacích taktik, sloužícím ke zrychlení algoritmu. Takové taktiky často nemůžeme při verifikaci používat, protože je velice obtížné, nebo i nemožné je poté ověřit.
+V této práci jsme se věnovali problematice formálního ověření a~implementace Dinitzova algoritmu s~dynamicky alokovanou pamětí, pro hledání maximálního toku v~orientované grafové síti. Podařilo se nám plně implementovat Dinitzův algoritmus v~programovacím jazyce C s~ACSL anotacemi a~také ověřit část kódu, která nepotřebuje prozatím neimplementované výrazy frameworku Frama-C týkajících se dynamické alokace paměti. 
+V prvních dvou kapitolách jsme také čtenáře seznámili s~oblastí toků v~orientovaných grafech, představili jsme jim mnoho základních pojmů a~definic a~také plně popsali myšlenku Dinitzova algoritmus pro hledání maximálního toku. Poskytli jsme jim také další zdroje a~práce, pokud by se chtěli v~tomto tématu dále vzdělávat. 
+Později jsme také uvedli některé možnosti, z~mnoha dalších, frameworku Frama-C a~doprovázejícímu mu anotačnímu jazyku ACSL, který jsme zde představili. Zavedli jsme si nástroje, které jsme používali v~naší práci, mimo frameworku Frama-C, také pluginy WP, RTE a~také řešiče Alt-Ergo, CVC4 a~Z3. Ke každému z~nich jsme dodali krátký popisek a~také projekty v~kterých byly využity.
+V praktické části jsme se již plně zaměřili na popsání naší implementace Dinitzova algoritmu a~objasnění naších rozhodnutí ohledně výběrů prostředků pro funkčnost našeho algoritmu. Poté jsme pokračovali vysvětlením a~zařazením anotací jazyka ACSL do tématu a~problématiky nalezení maximálního toku v~sítích. Řekli jsme si zde také problémy svázané s~použitím dynamicky alokované paměti a~pozdější verifikací pomocí frameworku Frama-C. 
+Rozšířením této práce by mohlo být porovnání rychlostí ověřeného Dinitzova algoritmu pro hledání maximálního toku a~neověřeného Dinitzova algoritmu s~využitím programovacích taktik, sloužícím ke zrychlení algoritmu. Takové taktiky často nemůžeme při verifikaci používat, protože je velice obtížné, nebo i nemožné je poté ověřit.
\ No newline at end of file