% % 03-spravnost-programov.tex % % Developed by Ondrej Jombik % 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 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=/*,*/