%
% 03-spravnost-programov.tex
%
% Developed by Ondrej Jombik <nepto@platon.sk>
% Copyright (c) 2003-2005 Platon Group, http://platon.sk/
% Licensed under terms of GNU General Public License.
% All rights reserved.
%
% Changelog:
% 26/02/2003 - created
%
% $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.10 2007-08-20 08:42:59 nepto Exp $
\chapter{Správnosť programov}
\section{Metódy dokazovania správnosti}
\begin{definition}[Floydova metóda] % /*
Floydová metóda robí redukciu dôkazu čiastočnej správnosti programu na
dokazovanie predikátových formúl:
\begin{itemize}
\item program rozdelíme deliacimi bodmi na konečné cesty
(počiatočný, koncový, resp. vnútorné body),
\item pre každý vnútorný deliaci bod sformulujeme invariant
$I_A(\overline{x}, \overline{y})$ -- podmienku, ktorá platí pri
každom prechode deliacim bodom; počiatočnému deliacemu bodu
zodpovedá vstupná podmienka, koncovému zase
výstupná podmienka,
\item ku každej konečnej ceste AB odvodíme a dokážeme verifikačnú
podmienku: ak pri prechode deliacim bodom A je splnená podmienka
$I_A$ potom po prechode cestou AB bude v deliacom bode B
splnená podmienka $I_B$:
$$
\forall \overline{x}, \overline{y}: I_A(\overline{x}, \overline{y})
\land R_{AB} (\overline{x}, \overline{y}) \Leftarrow I_B
(\overline{x}, r_{AB} (\overline{x}, \overline{y}))
$$
Sémantické vlastnosti cesty:
\begin{itemize}
\item $R_{AB} (\overline{x}, \overline{y})$ -- podmienka pre prechod cesty AB,
\item $r_{AB} (\overline{x}, \overline{y})$ -- modifikácia
pracovných premenných pri prechode AB.
\end{itemize}
\end{itemize}
\end{definition} % */
\begin{veta} % /*
Ak pre všetky cesty v programe $P$ (definované deliacimi bodmi)
platia zodpovedajúce verifikačné podmienky, potom je program $P$
čiastočne správny.
\end{veta} % */
\begin{example} % /* Floyd I.
Uvažujme nasledujúci štandardný program~$P$, ktorý počíta
$\lceil\sqrt{x}\rceil$ (hornú celú časť odmocniny~$x$).
$$
\begin{array}{lrl}
P: & \cmd{begin} & [y_1, y_2] := [1, 1] \\
& 1: & \cmd{if}~ y_2 \ge x ~\cmd{then}~\cmd{goto}~\cmd{end} \\
& 2: & [y_1, y_2] := [y_1 + 1, (y_1 + 1)^2] \\
& 3: & \cmd{goto}~1 \\
& \cmd{end} & [z] := [y_1] \\
\end{array}
$$
Definujte vstupnú podmienku, výstupnú podmienku a invarianty. Floydovou
metódou dokážte čiastočnú správnosť programu vzhľadom na vstupnú a
výstupnú podmienku.
\end{example} % */
\begin{solution} % /*
Vstupná podmienka presne vymedzuje vstupné hodnoty pre ktoré dáva
program žiadaný výsledok. V našom prípade ide o všetky kladné hodnoty.
Program by sa dal modifikovať aj tak, aby dával zmysluplné výsledky pre
všetky nezáporné hodnoty, ale prinieslo by nám to isté množstvo ďalších
komplikácií. Takže vstupná podmienka $p$ vyzerá nasledovne.
$$
p(x):~ x > 0
$$
Výstupná podmienka $q$ popisuje $z~=~\lceil\sqrt{x}\rceil$.
$$
\begin{array}{llcccl}
q(x, z): & & &\lceil\sqrt{x}\rceil & = & z \\
& (z - 1) & < & \sqrt{x} & \le & z \\
& (z - 1)^2 & < & x & \le & z^2 \\
\end{array}
$$
Invariantu v~príkaze $\cmd{begin}$ zodpovedá vstupná podmienka a
invariantu v~príkaze $\cmd{end}$ zodpovedá výstupná podmienka.
$$
\begin{array}{lcr}
I_B & = & p \\
I_E & = & q \\
\end{array}
$$
Program obsahuje jeden cyklus. Ideálne miesto pre jeho deliaci bod je
tam, kde sa z cyklu vychádza. V programe~$P$ je to rovnaké miesto ako
to, kde sa do cyklu vchádza. Ako deliaci bod teda zvolíme riadok~$1$.
Invariant~$I_1$ v~tomto bode vyzerá nasledovne.
$$
I_1:~ (y_1 - 1)^2 < x ~\land~ y_2 = y_1^2
$$
Prvá časť invariantu $I_1$ reprezentuje riadiacu podmienku cyklu.
V~druhej časti sa definuje závislosť medzi premennými $y_1$ a $y_2$.
Program~$P$ obsahuje tri deliace body medzi ktorými sú tri konečné
cesty.
\begin{center}
\begin{tabular}{lrcl}
-- ~ cesta B1: & $\cmd{begin}$ & $\rightarrow$ & riadok $1$ \\
-- ~ cesta 11: & riadok $1$ & $\rightarrow$ & riadok $1$ \\
-- ~ cesta 1E: & riadok $1$ & $\rightarrow$ & $\cmd{end}$ \\
\end{tabular}
\end{center}
Z definície vieme, že pre~každú cestu musíme dokázať verifikačnú
podmienku odvodenú z nasledujúceho všeobecného tvaru.
$$
\forall \overline{x}, \overline{y}
~ ~ I_A(\overline{x}, \overline{y})
~ \land
~ R_{AB}(\overline{x}, \overline{y})
~ \Longrightarrow
~ I_B(\overline{x}, r_{AB}(\overline{x}, \overline{y}))
$$
\underline{cesta B1:} Použitím spätnej substitúcie odvodíme podmienku
prechodu a modifikáciu pracovných premenných na~ceste~B1 a dosadíme do
príslušnej verifikačnej podmienky.
$$
\begin{array}{rcl}
R_{B1}(y_1,~y_2) & = & true \\
r_{B1}(y_1,~y_2) & = & (1,~1) \\
\end{array}
$$
$$
\begin{array}{rcl}
I_B ~ \land ~ true & \Rightarrow & I_1(1, 1) \\
x > 0 ~ \land ~ true & \Rightarrow & (1 - 1)^2 < x ~ \land ~ 1^2 = 1 \\
x > 0 ~ \land ~ true & \Rightarrow & 0 < x ~ \land ~ 1 = 1 \\
x > 0 ~ \land ~ true & \Rightarrow & x > 0 \\
\end{array}
$$
\underline{cesta 11:} Podobne ako v predchádzajúcom prípade odvodíme
$R_{11}$~a~$r_{11}$ a dosadíme do verifikačnej podmienky pre~cestu~11.
$$
\begin{array}{rcl}
R_{11}(y_1,~y_2) & = & true ~ \land ~ \lnot (y_2 \ge x) ~ = ~ y_2 < x \\
r_{11}(y_1,~y_2) & = & (y_1 + 1, (y_1 + 1)^2) \\
\end{array}
$$
$$
\begin{array}{rcl}
I_1(y_1, y_2) ~ \land ~ y_2 < x & \Rightarrow & I_1(y_1 + 1, (y_1 + 1)^2) \\
(y_1 - 1)^2 < x ~ \land ~ y_1^2 = y_2 ~ \land ~ y_2 < x & \Rightarrow
& (y_1 + 1 - 1)^2 < x ~ \land ~ (y_1 + 1)^2 = (y_1 + 1)^2 \\
y_1^2 = y_2 ~ \land ~ y_2 < x & \Rightarrow & y_1^2 < x ~ \land ~ true \\
y_1^2 < x & \Rightarrow & y_1^2 < x \\
\end{array}
$$
\underline{cesta 1E:} A do tretice aj pre poslednú cestu odvodíme
spätnou substitúciou $R_{1E}$~a~$r_{1E}$ a dosadíme do prislúchajúcej
verifikačnej podmienky.
$$
\begin{array}{rcl}
R_{1E}(y_1,~y_2) & = & true ~ \land ~ y_2 \ge x \\
r_{1E}(z) & = & y_1 \\
\end{array}
$$
$$
\begin{array}{rcl}
I_1(y_1, y_2) ~ \land ~ y_2 \ge x
& \Rightarrow & I_E \\
(y_1 - 1)^2 < x ~ \land ~ y_2 = y_1^2 ~ \land ~ y_2 \ge x
& \Rightarrow & (y_1 - 1)^2 < x \le y_1^2 \\
(y_1 - 1)^2 < x ~ \land ~ y_1^2 \ge x
& \Rightarrow & (y_1 - 1)^2 < x ~ \land ~ y_1^2 \ge x \\
\end{array}
$$
Pre všetky cesty v~programe~$P$ sme overili platnosť príslušných
odvodených verifikačných podmienok a tým sme dokázali aj čiastočnú
správnosť programu~$P$ vzhľadom na vstupnú podmienku~$p$ a výstupnú
podmienku~$q$.
\end{solution} % */
\begin{example} % /* Floyd II.
Daný je štandardný program $P$.
$$
\begin{array}{lrl}
P: & \cmd{begin} & [y_1, y_2] := [0, x_1] \\
& 1: & \cmd{if}~ y_2 < x_2 ~\cmd{then}~\cmd{goto}~\cmd{end} \\
& 2: & [y_1, y_2] := [y_1 + 1, y_2 - x_2] \\
& 3: & \cmd{goto}~1 \\
& \cmd{end} & [z_1, z_2] := [y_1, y_2] \\
\end{array}
$$
Floydovou metódou formálne dokážte čiastočnú správnosť programu~$P$
vzhľadom na nasledujúce podmienky:
\begin{itemize}
\item vstupná podmienka -- $p(x_1, x_2):~ x_1 \ge 0 ~ \land ~ x_2 > 0$
\item výstupná podmienka -- $q(x_1, x_2, z_1, z_2):~ z_1x_2 + z_2 = x_1 ~ \land ~ 0 \le z_2 < x_2$
\end{itemize}
Určte deliace body, nájdite k~nim prislúchajúce invarianty, zostrojte
verifikačné podmienky a ukážte, že platia\HWwarn{5}.
\end{example} % */
\begin{solution} % /*
Po krátkej analýze zistíme, že program delí hodnotu vstupnej premennej
$x_1$ hodnotou $x_2$. Deliteľ je uložený do výstupnej premennej $z_1$ a
zvyšok po delení do premennej $z_2$. Výsledok je tak tvaru
$x_1=z_1x_2+z_2$, kde~$z_2<x_2$ (zvyšok je menší ako hodnota, ktorou
delíme).
Máme dva implicitné deliace body v~návestiach $\cmd{begin}$ a
$\cmd{end}$. Invariantom v~týchto bodoch zodpovedajú vstupná
podmienka~$p$ a výstupná podmienka~$q$. Takže platí $I_B=p$ a $I_E=q$.
Keďže program opäť obsahuje jeden cyklus, ako jeho deliaci bod zvolíme
riadok~$1$. Je to miesto kde sa do cyklu vchádza i vychádza. Konštrukcia
invariantu k~tomuto deliacemu bodu programu je nerozhodnuteľným
problémom. Preto sa snažíme vyčítať z~vlastností programu i cyklu čo
najviac užitočných informácií a vložiť ich do podmienok
invariantu~$I_1$.
$$
I_1:~ x_1 = y_1x_2 + y_2 ~ \land ~ x_2 > 0 ~ \land ~ y_1 \ge 0 ~ \land ~ y_2 \ge 0
$$
Pre každú z~troch ciest odvodíme a dokážeme verifikačnú podmienku.
\underline{cesta B1:} $$
\begin{array}{rcl}
R_{B1}(y_1,~y_2) & = & true \\
r_{B1}(y_1,~y_2) & = & (0,~x_1) \\
\end{array}
$$
$$
\begin{array}{rcl}
I_B ~ \land ~ true & \Rightarrow & I_1(0, x_1) \\
x_1 \ge 0 ~ \land ~ x_2 > 0 & \Rightarrow & x_1 = 0x_2 + x_1 ~ \land ~ x_2 > 0 ~ \land ~ 0 \ge 0 ~ \land ~ x_1 \ge 0 \\
x_1 \ge 0 ~ \land ~ x_2 > 0 & \Rightarrow & x_1 = x_1 ~ \land ~ x_2 > 0 ~ \land ~ x_1 \ge 0 \\
x_1 \ge 0 ~ \land ~ x_2 > 0 & \Rightarrow & x_1 \ge 0 ~ \land ~ x_2 > 0 \\
\end{array}
$$
\underline{cesta 11:} $$
\begin{array}{rcl}
R_{11}(y_1,~y_2) & = & true ~ \land ~ \lnot (y_2 < x_2) ~ = ~ y_2 \ge x_2 \\
r_{11}(y_1,~y_2) & = & (y_1 + 1, y_2 - x_2) \\
\end{array}
$$
$$
\begin{array}{rcl}
I_1(y_1, y_2) ~ \land ~ y_2 \ge x_2 & \Rightarrow & I_1(y_1 + 1, y_2 - x_2) \\
%%%
%x_1 = y_1x_2 + y_2 ~ \land ~ x_2 > 0 ~ \land ~ ~ & & \\
%\land ~ y_1 \ge 0 ~ \land ~ y_2 \ge 0 & \Rightarrow
%& x_1 = (y_1 + 1)x_2 + (y_2 - x_2) ~ \land ~ x_2 > 0 ~ \land \\
%& & ~ ~ \land ~ y_1 + 1 \ge 0 ~ \land ~ y_2 - x_2 \ge 0 \\
%%%
%x_1 = y_1x_2 + y_2 ~ \land ~ ~ & & \\
%\land ~ y_1 \ge 0 ~ \land ~ y_2 - x_2 \ge 0 & \Rightarrow
%& x_1 = y_1x_2 + y_2 ~ \land \\
%& & ~ ~ \land ~ y_1 + 1 \ge 0 ~ \land ~ y_2 - x_2 \ge 0 \\
\end{array}
$$
$$
\begin{array}{c}
%I_1(y_1, y_2) ~ \land ~ y_2 \ge x_2 ~ \Rightarrow ~ I_1(y_1 + 1, y_2 - x_2) \\
%%%
x_1 = y_1x_2 + y_2 ~ \land ~ x_2 > 0 ~ \land ~ y_1 \ge 0 ~ \land ~ y_2 \ge 0 ~ \land ~ y_2 \ge x_2 ~ \Rightarrow ~ \hfill \\
\hfill ~ \Rightarrow ~ x_1 = (y_1 + 1)x_2 + (y_2 - x_2) ~ \land ~ x_2 > 0 ~ \land ~ y_1 + 1 \ge 0 ~ \land ~ y_2 - x_2 \ge 0 \\
\hfill \textrm{{\small (zrejme $y_2 \ge 0 \land x_2 > 0 \land y_2 \ge x_2 \Rightarrow y_2 - x_2 \ge 0$)}} \\
%\end{array}
%--$-$
%%%
%--$-$
%\begin{array}{c}
x_1 = y_1x_2 + y_2 ~ \land ~ y_1 \ge 0 ~ \land ~ y_2 - x_2 \ge 0 ~ \Rightarrow ~ \hfill \\
\hfill ~ \Rightarrow ~ x_1 = y_1x_2 + y_2 ~ \land ~ y_1 + 1 \ge 0 ~ \land ~ y_2 - x_2 \ge 0 \\
\hfill \textrm{{\small (zrejme platí $y_1 \ge 0 \Rightarrow y_1 + 1 \ge 0$)}} \\
\end{array}
$$
\underline{cesta 1E:}
$$
\begin{array}{rcl}
R_{1E}(y_1,~y_2) & = & true ~ \land ~ y_2 < x_2 \\
r_{1E}(z_1, z_2) & = & (y_1, y_2) \\
\end{array}
$$
$$
\begin{array}{rcl}
I_1(y_1, y_2) ~ \land ~ y_2 < x_2 & \Rightarrow & I_E \\
\end{array}
$$
$$
\begin{array}{c}
x_1 = y_1x_2 + y_2 ~ \land ~ x_2 > 0 ~ \land ~ y_1 \ge 0 ~ \land ~ y_2 \ge 0 ~ \land ~ y_2 < x_2 ~ \Rightarrow ~ \hfill \\
\hfill ~ \Rightarrow ~ x_1 = y_1x_2 + y_2 ~ \land ~ 0 \le y_2 < x_2 \\
x_1 = y_1x_2 + y_2 ~ \land ~ y_2 \ge 0 ~ \land ~ y_2 < x_2 ~ \Rightarrow ~ \hfill \\
\hfill ~ \Rightarrow ~ x_1 = y_1x_2 + y_2 ~ \land ~ y_2 \ge 0 ~ \land y_2 < x_2 \\
\end{array}
$$
Po overení verifikačných podmienok pre všetky cesty je čiastočná
správnosť programu~$P$ dokázaná.
\end{solution} % */
\begin{definition}[Jazyk] % /*
Jazykom sú dobre vytvorené formuly $\alpha, \beta$.
\end{definition} % */
\begin{definition} % /*
Platnosť (pravdivosť) formúl označujeme $\models \alpha$. Znamená
to, že formula $\alpha$ platí v~danej triede modelov.
\end{definition} % */
\begin{definition}[Dokazovací systém] % /*
Dokázateľnosť (odvoditeľnosť) formúl označujeme $\vdash \alpha$. Formula $\alpha$ sa
dá dokázať (odvodiť) z axióm a inferenčných pravidiel systému:
$$
\frac{\alpha_1 \dots \alpha_n}{\beta}
$$
\end{definition} % */
\begin{definition}[Zdravý systém] % /*
Zdravý systém je taký, v ktorom dokázateľné sú len pravdivé formuly.
$$
\vdash \alpha ~ \Rightarrow ~ \models \alpha
$$
\end{definition} % */
\begin{definition}[Úplný systém] % /*
Úplný systém je taký, v ktorom každá pravdivá formula je
dokázateľná.
$$
\models \alpha ~ \Rightarrow ~ \vdash \alpha
$$
\end{definition} % */
\begin{definition}[Hoareova metóda] % /*
Hoareova metóda používa logický systém pre dokazovanie čiastočnej
správnosti programov založený na jazyku induktívnych formúl
$$
\{p\} P \{q\}
$$
\end{definition} % */
\begin{definition}[Induktívna formula] % /*
Význam induktívnej (invariantnej) formuly
$$
\models ~ \{p\} P \{q\}
$$
závisí od významu podmienok $p, q$ a významu programu $P$.
Formula je teda pravdivá práve vtedy, ak vstupné hodnoty programu
$P$ spĺňajú podmienku $p$ a po zastavení programu (príkazu) $P$
výstupné hodnoty $P$ vyhovujú podmienke $q$.
\end{definition} % */
\begin{definition}[Najslabšia vstupná podmienka] % /*
Označujeme $wp(P, q)$.
K programu $P$ a výstupnej podmienke $q$:\\
$\forall p$ ak platí $\{wp(P,q)\} P \{q\}, \{p\} P \{q\}$ potom $p
\Rightarrow wp(P, q)$
\end{definition} % */
\begin{definition}[Najsilnejšia výstupná podmienka] % /*
Označujeme $sp(P, p)$.
K programu $P$ a vstupnej podmienke $q$:\\
$\forall q$ ak platí $\{p\} P \{sp(P,p)\}, \{p\} P \{q\}$ potom
$sp(P, p) \Rightarrow q$
\end{definition} % */
\begin{definition}[Inferenčný systém $\mathcal{H}$] % /*
Inferenčný systém pozostáva z troch pravidiel a z jednej axiómy
priradenia:
\begin{itemize}
\item \bf{Axiomatická schéma priradenia}
$$
\{p(\overline{x}, g(\overline{x}, \overline{y}))\}
~ \overline{y} := g(\overline{x}, \overline{y}) ~
\{p(\overline{x}, \overline{y})\}
$$
$$
\{q[x/s]\} ~ x := s ~ \{q\}
$$
\item \bf{Kompozičné pravidlo}
$$
\frac{\{p\} S_1 \{q\} ~ ~ ~ \{q\} S_2 \{r\}}{\{p\} S_1; S_2
\{r\}}
$$
\item \bf{Alternatívne pravidlo}
$$
\frac{\{p \land b\} S_1 \{q\} ~ ~ ~ \{p \land \lnot b\} S_2
\{q\}}{\{p\} ~\cmd{if}~ b ~\cmd{then}~ S_1 ~\cmd{else}~ S_2
~\cmd{fi}~ \{q\}}
$$
\item \bf{Iteratívne pravidlo}
$$
\frac{\{p \land b\} S \{p\}}{\{p\} ~\cmd{while}~ b ~\cmd{do}~
S ~\cmd{od}~ \{p \land \lnot b\}}
$$
\end{itemize}
\end{definition} % */
\begin{example} % /* Hoare I.
Daný je štruktúrovaný program $P$.
$$
\begin{array}{lrl}
P: & \cmd{begin} & [y_1, y_2] := [1, 1] \\
& & \cmd{while}~ y_2 < x ~\cmd{do} \\
& & ~~~~[y_1, y_2] := [y_1 + 1, (y_1 + 1)^2] \\
& & \cmd{od} \\
& \cmd{end} & [z] := [y_1] \\
\end{array}
$$
Hoareovou metódou formálne dokážte čiastočnú správnosť programu~$P$
vzhľadom na~nasledujúce podmienky:
\begin{itemize}
\item vstupná podmienka -- $p(x):~ x > 0$
\item výstupná podmienka -- $q(x, y):~ (z - 1)^2 < x \le z^2$
\end{itemize}
\end{example} % */
\begin{solution} % /*
Hoareova metóda dokazovania čiastočnej správnosti štruktúrovaných
programov sa opiera o~logický systém založený na~jazyku induktívnych
formúl $\{p\}~P~\{q\}$. Pri dokazovaní sa používajú všetky platné
formuly špecifikačného jazyka, axióma priradenia a inferenčné
resp.~odvodzovacie pravidlá Hoareovského kalkulu.
Pre dôkaz čiastočnej správnosti programu~$P$ musíme dokázať platnosť
nasledujúcej induktívnej formuly.
$$
\{p\}~P~\{q\}
$$
Krátkou analýzou zistíme, že program~$P$ sa skladá z~troch častí.
Z~dostupných inferenčných pravidiel teda aplikujeme \textit{pravidlo
kompozície} a vyriešime induktívne formuly zodpovedajúce jednotlivým
častiam programu~$P$.
$$
\{p\}~P_1~\{r\} ~~~ \{r\}~P_2~\{s\} ~~~ \{s\}~P_3~\{q\}
$$
Ešte pred samotným riešením jednotlivých induktívnych formúl sa pokúsime
prispôsobiť si podmienky $r$ a $s$. Časť $P_2$ je $\cmd{while}$ cyklus
s~podmienkou $b$, preto uhádneme, ako by mohla vyzerať podmienka $s$,
ktorá platí po jeho ukončení.
$$
s ~\equiv~ r \land \lnot b
$$
Je nutné podotknúť, že~v~našom prípade tento postup povedie k~úspechu.
Rozhodne však neplatí vo~všeobecnosti na~všetky štruktúrované programy.
\begin{itemize}
\item \underline{Induktívna formula $\{p\}~P_1~\{r\}$:} Časť~$P_1$
programu~$P$ obsahuje jediné priradenie v~návestí $\cmd{begin}$.
Použitím \textit{axiómy priradenia} nahradíme v~podmienke $r$ obe
premenné $y_1$ a $y_2$ hodnotou~$1$. Určite platí
$$
\{r[y_1/1, y_2/1]\}~P_1~\{r\}
$$
Ak sa podarí dokázať nasledujúcu implikáciu, bude možné použiť
\textit{pravidlo následku} a tým bude induktívna formula
$\{p\}~P_1~\{r\}$ dokázaná.
$$
p ~\Rightarrow~ r[y_1/1, y_2/1]
$$
\item \underline{Induktívna formula $\{r\}~P_2~\{r \land \lnot b\}$:}
Časť~$P_2$ programu~$P$ je reprezentovaná cyklusom $\cmd{while}$.
Preto použijeme \textit{pravidlo iterácie}.
$$
\{r \land b\}~P_{21}~\{r\}
$$
Pre priradenie nachádzajúce~sa v~cykle $\cmd{while}$ použijeme
\textit{axiómu priradenia}. Určite teda platí
$$
\{r[y_1/y_1+1, y_2/(y_1+1)^2]\}~P_{21}~\{r\}
$$
Dokázaním nasledujúcej implikácie dokážeme platnosť celej induktívnej
formuly $\{r\}~P_2~\{r \land \lnot b\}$.
$$
r \land b ~\Rightarrow~ r[y_1/y_1+1, y_2/(y_1+1)^2]
$$
\item \underline{Induktívna formula $\{r \land \lnot b\}~P_3~\{q\}$:}
Podobne ako časť~$P_1$ aj časť~$P_3$ programu~$P$ obsahuje len jedno
priradenie, tentokrát v~návestí~$\cmd{end}$. Aplikujeme
\textit{axiómu priradenia}. Potom určite platí
$$
\{q[z/y_1]\}~P_3~\{q\}
$$
Ak sa podarí dokázať nasledujúcu implikáciu, bude možné použiť
\textit{pravidlo následku} a tým bude induktívna formula
$\{r \land \lnot b\}~P_3~\{q\}$ dokázaná.
$$
r \land \lnot b ~\Rightarrow~ q[z/y_1]
$$
\end{itemize}
Z~troch hlavných častí programu teda dostávame tri implikácie, ktorých
platnosť je nutné dokázať.
$$
\begin{array}{rcl}
p(x) ~\land~ true & \Rightarrow & r[y_1/1, y_2/1] \\
r ~\land~ b & \Rightarrow & r[y_1/y_1+1, y_2/(y_1+1)^2] \\
r ~\land~ \lnot b & \Rightarrow & q[z/y_1] \\
\end{array}
$$
Musíme sformulovať podmienku~$r$. Podobne ako hľadanie invariantu
vo~Floydovej metóde, je nájdenie tejto podmienky netriviálny a
nedeterministický proces. Je vhodné a vo~väčšine prípadov aj úspešné
vychádzať z~poslednej implikácie a odvodiť hľadanú podmienku~$r$
od~výstupnej podmienky~$q$.
V~našom prípade je podmienka~$r$ rovnaká, ako prislúchajúci invariant
v~ekvivalentnom štandardnom programe dokazovanom Floydovou metódou.
$$
r ~\equiv~ y_1^2 = y_2 ~\land~ (y_1 - 1)^2 < x
$$
Poznáme podmienku~$b$ cyklu~$\cmd{while}$ v~časti~$P_2$.
$$
b ~\equiv~ y_2 < x
$$
Výsledné implikácie teda vyzerajú nasledovne.
$$
\begin{array}{rcl}
x > 0 ~\land~ true & \Rightarrow & 1^2 = 1 ~\land~ (1 - 1)^2 < x \\
y_1^2 = y_2 ~\land~ (y_1 - 1)^2 < x ~\land~ y_2 < x & \Rightarrow & (y_1 + 1)^2 = (y_1+1)^2 ~\land~ (y_1 + 1 - 1)^2 < x \\
y_1^2 = y_2 ~\land~ (y_1 - 1)^2 < x ~\land~ y_2 \ge x & \Rightarrow & (y_1 - 1)^2 < x \le y_1^2 \\
\end{array}
$$
Samotné dôkazy implikácií sú priamočiare a jednoduché.
\end{solution} % */
\begin{example} % /* Hoare II.
Daný je štruktúrovaný program $P$.
$$
\begin{array}{lrl}
P: & \cmd{begin} & [y_1, y_2] := [0, x_1] \\
& & \cmd{while}~ y_2 \ge x_2 ~\cmd{do} \\
& & ~~~~[y_1, y_2] := [y_1 + 1, y_2 - x_2] \\
& & \cmd{od} \\
& \cmd{end} & [z_1, z_2] := [y_1, y_2] \\
\end{array}
$$
Hoareovou metódou formálne dokážte čiastočnú správnosť programu~$P$
vzhľadom na~nasledujúce podmienky:
\begin{itemize}
\item vstupná podmienka -- $p(x_1, x_2):~ x_1 \ge 0 ~ \land ~ x_2 > 0$
\item výstupná podmienka -- $q(x_1, x_2, z_1, z_2):~ z_1x_2 + z_2 = x_1 ~ \land ~ 0 \le z_2 < x_2$
\HWwarn{6}
\end{itemize}
\end{example} % */
\begin{solution} % /*
V predchádzajúcom príklade na~dokazovanie čiastočnej správnosti
programu~$P$ Hoareovou metódou sme použili tzv. postup \textit{zhora
dole}. Vychádzali sme z~induktívnej formuly~$\{p\}P\{q\}$, na ktorú sme
postupne aplikovali inferenčné odvodzovacie pravidlá a axiómu
priradenia. Týmto spôsobom sme dospeli k~niekoľkým implikáciam, ktoré
sme dokázali.
Akosi implicitne sme predpokladali, ze dokázaním týchto implikácií sa
dokáže aj induktívna formula~$\{p\}P\{q\}$ a teda aj čiastočná správnosť
programu~$P$. To je samozrejme pravda, no v skutočnosti má táto
induktívna formula stáť na konci celého procesu odvodzovania a
dokazovania a nie na jeho začiatku. Preto existuje aj spôsob, ako
zapísať Hoareovu metódu formálnejšie.
Je nutné zdôrazniť, že oba zápisy sú dobré. Prvý je názornejší, keďže
nezačíname ničnehovoriacim tvrdením, ale známou všeobecnou induktívnou
formulou. Druhý zápis je zase formálnejší. Nasledujúci dôkaz čiastočnej
správnosti Hoareovou metódou zapíšeme formálnejším spôsobom. Tento
spôsob je používaný taktiež v~skriptách.
Zvolíme si invariant. \hfill $R(x_1, x_2, y_1, y_2):~ y_1x_2 + y_2 = x_1 \land 0 \le y_2 < x_2$
\begin{enumerate}
\item $x_1 \ge 0 ~\land~ x_2 > 0 ~\Rightarrow~ R(x_1, x_2, 0, x_1) \\
0x_2 + x_1 = x_1 ~\land~ x_1 \ge 0$
\item $\{R(x_1, x_2, 0, x_1)\} \\
\mathrm{~~~~}[y_1, y_2] := [0, x_1] \\
\{R(x_1, x_2, y_1, y_2)\} \\
\textrm{\textit{axióma priradenia}}$
\item $\{x_1 \ge 0 ~\land~ x_2 > 0\} \\
\mathrm{~~~~}[y_1, y_2] := [0, x_1] \\
\{R(x_1, x_2, y_1, y_2)\} \\
\textrm{\textit{pravidlo následku} pre 1. a 2.}$
\item $R(x_1, x_2, y_1, y_2) ~\land~ y_2 \ge x_2 ~\Rightarrow~ R(x_1, x_2, y_1 + 1, y_2 - x_2) \\
y_1x_2 + y_2 = x_1 ~\land~ y_2 \ge 0 ~\land~ y_2 \ge x_2 ~\Rightarrow \hfill \\
\mathrm{~~~~}\Rightarrow~ (y_1 + 1)x_2 + y_2 - x_2 = x_1 ~\land~ y_2 - x_2\ge 0 \\
y_1x_2 + y_2 = x_1 ~\land~ y_2 \ge 0 ~\land~ y_2 \ge x_2 ~\Rightarrow~ y_1x_2 + y_2 = x_1 ~\land~ y_2 \ge x_2$
\item $\{R(x_1, x_2, y_1 + 1, y_2 - x_2)\} \\
\mathrm{~~~~}[y_1, y_2] := [y_1 + 1, y_2 - x_2] \\
\{R(x_1, x_2, y_1, y_2)\} \\
\textrm{\textit{axióma priradenia}}$
\item $\{R(x_1, x_2, y_1, y_2) ~\land~ y_2 \ge x_2\} \\
\mathrm{~~~~}[y_1, y_2] := [y_1 + 1, y_2 - x_2] \\
\{R(x_1, x_2, y_1, y_2)\} \\
\textrm{\textit{pravidlo následku} pre 4. a 5.}$
\item $\{R(x_1, x_2, y_1, y_2)\} \\
\mathrm{~~~~}\cmd{while}~ y_2 \ge x_2 ~\cmd{do} \\
\mathrm{~~~~~~~~}[y_1, y_2] := [y_1 + 1, y_2 - x_2] \\
\mathrm{~~~~}\cmd{od} \\
\{R(x_1, x_2, y_1, y_2) ~\land~ y_2 < x_2\} \\
\textrm{\textit{pravidlo iterácie} pre 6.}$
\item $\{x_1 \ge 0 ~\land~ x_2 > 0\} \\
\mathrm{~~~~}[y_1, y_2] := [0, x_1] \\
\mathrm{~~~~}\cmd{while}~ y_2 \ge x_2 ~\cmd{do} \\
\mathrm{~~~~~~~~}[y_1, y_2] := [y_1 + 1, y_2 - x_2] \\
\mathrm{~~~~}\cmd{od} \\
\{R(x_1, x_2, y_1, y_2) ~\land~ y_2 < x_2\} \\
\textrm{\textit{pravidlo kompozície} pre 3. a 7.}$
\item $R(x_1, x_2, y_1, y_2) ~\land~ y_2 < x_2 ~\Rightarrow~ y_1x_2 + y_2 = x_1 ~\land~ 0 \le y_2 < x_2 \\
y_1x_2 + y_2 = x_1 ~\land~ y_2 \ge 0 ~\land~ y_2 < x_2 ~\Rightarrow~ y_1x_2 + y_2 = x_1 ~\land~ 0 \le y_2 < x_2$
\item $\{y_1x_2 + y_2 = x_1 ~\land~ 0 \le y_2 < x_2\} \\
\mathrm{~~~~}[z_1, z_2] := [y_1, y_2] \\
\{z_1x_2 + z_2 = x_1 ~\land~ 0 \le z_2 < x_2\} \\
\textrm{\textit{axióma priradenia}}$
\item $\{R(x_1, x_2, y_1, y_2) ~\land~ y_2 < x_2\} \\
\mathrm{~~~~}[z_1, z_2] := [y_1, y_2] \\
\{z_1x_2 + z_2 = x_1 ~\land~ 0 \le z_2 < x_2\} \\
\textrm{\textit{pravidlo následku} pre 9. a 10.}$
\item $\{x_1 \ge 0 ~\land~ x_2 > 0\} \\
\mathrm{~~~~}[y_1, y_2] := [0, x_1] \\
\mathrm{~~~~}\cmd{while}~ y_2 \ge x_2 ~\cmd{do} \\
\mathrm{~~~~~~~~}[y_1, y_2] := [y_1 + 1, y_2 - x_2] \\
\mathrm{~~~~}\cmd{od} \\
\mathrm{~~~~}[z_1, z_2] := [y_1, y_2] \\
\{z_1x_2 + z_2 = x_1 ~\land~ 0 \le z_2 < x_2\} \\
\textrm{\textit{pravidlo kompozície} pre 8. a 11.}$
\end{enumerate}
\end{solution} % */
\begin{example} % /* Hoare III.
Uvažujme nasledujúci štruktúrovaný program $P$.
$$
\begin{array}{lrl}
P: & \cmd{begin} & [y_1, y_2, y_3] := [1, 0, 0] \\
& & \cmd{while}~ y_1 \le n ~\cmd{do} \\
& & ~~~~[y_3] := [a[y_1]]; \\
& & ~~~~\cmd{if}~ y_3 < 0 ~\cmd{then} \\
& & ~~~~~~~~[y_3] := [-y_3] \\
& & ~~~~\cmd{fi}; \\
& & ~~~~[y_1, y_2] := [y_1 + 1, y_2 + y_3] \\
& & \cmd{od} \\
& \cmd{end} & [z] := [y_2] \\
\end{array}
$$
Hoareovou metódou formálne dokážte čiastočnú správnosť programu~$P$
vzhľadom na~vstupnú a výstupnú podmienku:
\begin{itemize}
\item vstupná podmienka -- $p(a, n):~ n \ge 0$
\item výstupná podmienka -- $q(a, n, z):~ z = \sum_{i=1}^{n}|a[i]|$
\end{itemize}
\end{example} % */
\begin{solution} % /*
Začíname použitím \textit{pravidla kompozície}.
$$
\frac{\{p\}~P_1~\{r\}~~~\{r\}~P_2~\{s\}~~~\{s\}~P_3~\{q\}}{\{p\}~P~\{q\}}
$$
Postupne dokážeme všetky tri induktívne formuly. Prvú, tretiu a nakoniec
druhú, ktorá je najobsiahlejšia.
\begin{itemize}
\item \underline{Induktívna formula $\{p\}~P_1~\{r\}$:} Vieme, že podľa
\textit{axiómy priradenia} platí tvrdenie $\{r[y_1/1, y_2/0,
y_3/0]\}P_1\{r\}$. Musíme teda dokázať nasledujúcu implikáciu.
$$
p ~\Rightarrow~ r[y_1/1, y_2/0, y_3/0]
$$
\item \underline{Induktívna formula $\{s\}~P_3~\{q\}$:} Určite platí
$\{q[z/y_2]\}P_3\{q\}$ a tak dokazujeme nasledujúcu implikáciu.
$$
s ~\Rightarrow~ q[z/y_2]
$$
\item \underline{Induktívna formula $\{r\}~P_2~\{s\}$:} Časť~$P_2$
programu~$P$ obsahuje cyklus $\cmd{while}$, pre~ktorý je možné
použiť \textit{pravidlo iterácie}. Ešte pred tým si však musíme
upraviť induktívnu formulu \textit{pravidlom následku}.
$$
\frac
{\{r\}~\cmd{while}~ b ~\cmd{do}~ P_2^{'} ~\cmd{od}~\{r \land \lnot b\}~~~(r \land \lnot b \Rightarrow s)}
{\{r\}~\cmd{while}~ b ~\cmd{do}~ P_2^{'} ~\cmd{od}~\{s\}}
$$
$$
\frac
{\{r \land b\}~ P_2^{'} ~\{r\}}
{\{r\}~\cmd{while}~ b ~\cmd{do}~ P_2^{'} ~\cmd{od}~\{r \land \lnot b\}}
$$
Pre vnútorný príkaz~$P_2^{'}$ cyklusu~$\cmd{while}$ použijeme
\textit{pravidlo kompozície}, pretože sa skladá z~troch osobitných
častí.
$$
\frac
{\{r \land b\}~ P_{21} ~\{f\}~~~\{f\}~ P_{22} ~\{g\}~~~\{g\}~ P_{23} ~\{r\}}
{\{r \land b\}~ P_2^{'} ~\{r\}}
$$
Časti~$P_{21}$~a~$P_{23}$ sú reprezentované priradeniami. Určite platia
tvrdenia $\{f[y_3/a[y_1]]\}P_{21}\{f\}$ a $\{r[y_1/y_1+1,
y_2/y_2+y_3]\}P_{23}\{r\}$, preto musíme dokázať nasledujúce implikácie.
$$
\begin{array}{rcl}
r \land b & \Rightarrow & f[y_3/a[y_1]] \\
g & \Rightarrow & r[y_1/y_1+1, y_2/y_2+y_3] \\
\end{array}
$$
Zostávajúcu časť~$P_{22}$ tvorí riadiaca štruktúra~$\cmd{if}$
neobsahujúca vetvu~$\cmd{else}$. Pre~tento účel sa používa upravené
\textit{pravidlo alternatívy}, tzv. \textit{pravidlo pol~alternatívy}.
$$
\frac
{\{f \land c\}~P_{221}~\{g\}~~~(f \land \lnot c \Rightarrow g)}
{\{f\}~\cmd{if}~ c ~\cmd{then}~ P_{221} ~\cmd{fi}~\{g\}}
$$
Nakoniec \textit{axiómou priradenia} aplikovanou na časť~$P_{221}$
dostávame poslednú implikáciu.
$$
f \land c ~\Rightarrow~ g[y_3/-y_3]
$$
\end{itemize}
Pre dokázanie čiastočnej správnosti programu~$P$ je teda nutné
sformulovať podmienky~$r$, $s$, $f$ a $g$ v~nasledujúcich implikáciach a
tieto implikácie dokázať.
$$
\begin{array}{rcl}
p & \Rightarrow & r[y_1/1, y_2/0, y_3/0] \\
s & \Rightarrow & q[z/y_2] \\
r \land \lnot b & \Rightarrow & s \\
r \land b & \Rightarrow & f[y_3/a[y_1]] \\
g & \Rightarrow & r[y_1/y_1+1, y_2/y_2+y_3] \\
f \land \lnot c & \Rightarrow & g \\
f \land c & \Rightarrow & g[y_3/-y_3] \\
\end{array}
$$
%%% TODO\footnote{nechce sa mi to doťahovať, asi to prenechám na čitateľa}
Po sformulovaní podmienok~$r$, $s$, $f$ a $g$ a následnom dokázaní
všetkých uvedených implikácií je čiastočná správnosť programu~$P$
vzhľadom na~vstupnú podmienku~$p$ a výstupnú podmienku~$q$ dokázaná.
Kompletný dôkaz je prenechaný ako cvičenie pre~čitateľa.
\end{solution} % */
\section{Rozširovanie Hoareovských kalkulov}
\begin{example} % /*
Sformulujte inferenčné pravidlo Hoareovského kalkulu pre riadiacu
štruktúru~$\cmd{repeat}$ definovanú nasledujúcim vzťahom.
$$
(\cmd{repeat}~ S ~\cmd{until}~ b) ~\equiv~ (S; ~\cmd{while}~ \neg b ~\cmd{do}~ S ~\cmd{od})
$$
Dokážte, že navrhnuté inferenčné pravidlo je zdravé.
\end{example} % */
\begin{solution} % /*
Riadiaca štruktúra~$\cmd{repeat}$, dobre známa napríklad
z~programovacieho jazyka Pascal, sa dá jednoducho prepísať pomocou
riadiacej štruktúry~$\cmd{while}$ tak, ako je to zobrazené v~zadaní
úlohy.
\begin{center}
$
\begin{array}{@{} c @{}}
\{p\}~S; ~\cmd{while}~ \neg b ~\cmd{do}~ S ~\cmd{od}~\{q\} \\
\hline
\{p\}~\cmd{repeat}~ S ~\cmd{until}~ b~\{q\} \\
\end{array}
$
~~~
$
\begin{array}{c}
(1) \\
(2) \\
\end{array}
$
\end{center}
Ak dokážeme tvrdenie~$(1)$, budeme mať dokázané aj~tvrdenie~$(2)$.
Obdobný postup budeme aplikovať aj~v~ďalších odvodzovaniach rozširovaní
Hoareovských kalkulov za~pomoci štyroch inferenčných pravidiel.
Tvrdenie~$(1)$ sa skladá z~dvoch častí. Použijeme \textit{pravidlo
kompozície}.
$$
\frac
{\{p\}~S~\{r\}~~~\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S ~\cmd{od}~\{q\}}
{\{p\}~S; ~\cmd{while}~ \neg b ~\cmd{do}~ S ~\cmd{od}~\{q\}}
$$
Pre cyklus $\cmd{while}$ existuje \textit{pravidlo iterácie}. Pravidlo
však vyžaduje výstupnú podmienku v~konkrétnom tvare. Na~dosiahnutie
žiadaného tvaru použijeme \textit{pravidlo následku}.
$$
\frac
{\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S ~\cmd{od}~\{r \land b\}~~~(r \land b \Rightarrow q)}
{\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S ~\cmd{od}~\{q\}}
$$
Teraz je už možné použiť zmieňované \textit{pravidlo iterácie}
pre~cyklus~$\cmd{while}$.
$$
\frac
{\{r \land \lnot b\}~S~\{r\}}
{\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S ~\cmd{od}~\{r \land b\}}
$$
Nakoniec sformulujeme inferenčné pravidlo pre~riadiacu
štruktúru~$\cmd{repeat}$.
$$
\frac
{\{p\}~S~\{r\}~~~\{r \land \lnot b\}~S~\{r\}~~~(r \land b \Rightarrow q)}
{\{p\}~\cmd{repeat}~ S ~\cmd{until}~ b~\{q\}}
$$
Výsledné inferenčné pravidlo je zdravé, pretože pri~jeho odvodzovaní sme
používali už~existujúce inferenčné pravidlá Hoareovského dokazovacieho
systému, ktoré sú zdravé.
\end{solution} % */
\begin{example} % /*
Navrhnite inferenčné pravidlo Hoareovho dokazovacieho systému
pre~riadiacu štruktúru reprezentujúcu tzv.~jeden~a~pol cyklus.
$$
\begin{array}{l}
\cmd{do} \\
~~~~S_1; \\
~~~~\cmd{exit}~\cmd{when}~b; \\
~~~~S_2 \\
\cmd{od} \\
\end{array}
$$
resp.
$$
(\cmd{loop}~ S_1; ~\cmd{when}~ b ~\cmd{exit};~ S_2 ~\cmd{pool})
~\equiv~ (S_1; ~\cmd{while}~ \lnot b ~\cmd{do}~ S_2;~S_1 ~\cmd{od})
$$
\end{example} % */
\begin{solution} % /*
Podobne ako v~predchádzajúcom príklade budeme používať už existujúce
inferenčné pravidlá Hoareovského kalkulu pre~dokázanie žiadaného
tvrdenia.
$$
\frac
{\{p\}~S_1; ~\cmd{while}~ \lnot b ~\cmd{do}~ S_2;~S_1 ~\cmd{od}~\{q\}}
{\{p\}~\cmd{loop}~ S_1; ~\cmd{when}~ b ~\cmd{exit};~ S_2 ~\cmd{pool}~\{q\}}
$$
\begin{itemize}
\item \textit{pravidlo kompozície}
$$
\frac
{\{p\}~S_1~\{r\}~~~\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S_2;~S_1 ~\cmd{od}~\{q\}}
{\{p\}~S_1; ~\cmd{while}~ \lnot b ~\cmd{do}~ S_2;~S_1 ~\cmd{od}~\{q\}}
$$
\item \textit{pravidlo následku}
$$
\frac
{\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S_2;~S_1 ~\cmd{od}~\{r \land b\}~~~(r \land b \Rightarrow q)}
{\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S_2;~S_1 ~\cmd{od}~\{q\}}
$$
\item \textit{pravidlo iterácie}
$$
\frac
{\{r \land \lnot b\}~ S_2;~S_1 ~\{r\}}
{\{r\}~\cmd{while}~ \lnot b ~\cmd{do}~ S_2;~S_1 ~\cmd{od}~\{r \land b\}}
$$
\item \textit{pravidlo kompozície}
$$
\frac
{\{r \land \lnot b\}~ S_2 ~\{s\}~~~\{s\}~ S_1 ~\{r\}}
{\{r \land \lnot b\}~ S_2;~S_1 ~\{r\}}
$$
\end{itemize}
Na~záver sformulujeme výsledné inferenčné pravidlo.
$$
\frac
{\{p\}~S_1~\{r\}~~~\{r \land \lnot b\}~ S_2 ~\{s\}~~~\{s\}~ S_1 ~\{r\}~~~(r \land b \Rightarrow q)}
{\{p\}~\cmd{loop}~ S_1; ~\cmd{when}~ b ~\cmd{exit};~ S_2 ~\cmd{pool}~\{q\}}
$$
\end{solution} % */
\begin{example} % /* 3x while (P_K)
Sformulujte inferenčné pravidlo Hoareovského kalkulu pre~programovú
konštrukciu~$P_K$.
$$
\begin{array}{ll}
P_K: & \cmd{while}~ c ~\cmd{do}~ S ~\cmd{od}; \\
& \cmd{while}~ b ~\cmd{do} \\
& ~~~~~~S; \\
& ~~~~~~\cmd{while}~ c ~\cmd{do}~ S ~\cmd{od}; \\
& \cmd{od} \\
\end{array}
$$
\end{example} % */
\begin{solution} % /*
Inferenčné pravidlo pre programovú konštrukciu $P_K$ vyzerá nasledovne.
Podrobné odvodenie je prenechané ako cvičenie pre~čitateľa.
$$
\frac{\{p \land c\}~S~\{p\}~~\{s \land b\}~S~\{r\}~~\{r \land
c\}~S~\{r\}~~(p \land\lnot c \Rightarrow s)~~(r \land\lnot c
\Rightarrow s)~~(s \land\lnot b \Rightarrow q)}{\{p\}~\cmd{while}~ c ~\cmd{do}~ S ~\cmd{od}; ~\cmd{while}~ b ~\cmd{do}~ S; ~\cmd{while}~ c ~\cmd{do}~ S ~\cmd{od}; ~\cmd{od}~\{q\}}
$$
\end{solution} % */
\begin{example} % /* 3x while (P_K) part II.
Predpokladajme, že platí nasledujúca formula.
$$
\{p ~\land~ (b ~\lor~ c)\}~S~\{p\}
$$
Dokážte Hoareovou metódou čiastočnú správnosť programovej
konštrukcie~$P_K$ z~predchádzajúceho príkladu vzhľadom na~vstupnú
podmienku~$\{p\}$ a výstupnú podmienku~$\{p \land (\lnot b \land \lnot
c)\}$.
\end{example} % */
\begin{solution} % /*
Pre vyriešenie úlohy stačí dokázať nasledujúci
vzťah.\footnote{V~skutočnosti je to však dosť zložité. Komplexné
riešenie úlohy je vítané a bude zaradené do~\textit{Zbierky riešených
úloh zo~ZTP}.}
$$
\frac
{\{p ~\land~ (b ~\lor~ c)\}~ S ~\{p\}}
{\{p\}~ P_K ~\{p ~\land~ \lnot b ~\land~ \lnot c\}}
$$
%%% TODO\footnote{Tu je problém, že to neviem doriešiť. Na cvikách sme to
%%% skúšali, ale nie veľmi úspešne. Ak by to niekto náhodou vyriešil, budem
%%% vďačný ak mi pošle riešenie\dots}
\end{solution} % */
% vim: ts=4 isk+=-
% vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
Platon Group <platon@platon.org> http://platon.org/
|