Platon Technologies
not logged in Login Registration
EnglishSlovak
open source software development celebrating 10 years of open source development! Friday, October 16, 2026
[BACK] [TXT][DIR] Up to [Platon] / doc / ztp-zbierka

Diff for doc/ztp-zbierka/03-spravnost-programov.tex between version 1.1 and 1.2

version 1.1, 2003/07/18 17:07:11 version 1.2, 2003/10/10 13:40:35
Line 10 
Line 10 
 % 26/02/2003 - created  % 26/02/2003 - created
 %  %
   
 % $Platon$  % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.1 2003/07/18 17:07:11 nepto Exp $
   
 \chapter{Správnosť programov}  \chapter{Správnosť programov}
   
Line 714  f \land c        & \Rightarrow    & g[y_3/-y_3]
Line 714  f \land c        & \Rightarrow    & g[y_3/-y_3]
 \end{array}  \end{array}
 $$  $$
   
 TODO\footnote{nechce sa mi to doťahovať, asi to prenechám na čitateľa}  %%% 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} % */  \end{solution} % */
   
Line 951  c)\}$.
Line 956  c)\}$.
   
 \begin{solution} % /*  \begin{solution} % /*
   
 Pre vyriešenie úlohy stačí dokázať nasledujúci vzťah.  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  \frac
Line 959  $$
Line 967  $$
 {\{p\}~ P_K ~\{p ~\land~ \lnot b ~\land~ \lnot c\}}  {\{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  %%% 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  %%% 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}  %%% vďačný ak mi pošle riešenie\dots}
   
 \end{solution} % */  \end{solution} % */
   
Legend:
Removed from v.1.1  
changed lines
  Added in v.1.2
Platon Group <platon@platon.org> http://platon.org/
Copyright © 2002-2006 Platon Group
Site powered by Metafox CMS 		Go to Top