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.8 and 1.9

version 1.8, 2007/04/29 19:39:13 version 1.9, 2007/05/27 16:38:21
Line 10 
Line 10 
 % 26/02/2003 - created  % 26/02/2003 - created
 %  %
   
 % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.7 2005-11-23 19:33:59 nepto Exp $  % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.8 2007-04-29 19:39:13 nepto Exp $
   
 \chapter{Správnosť programov}  \chapter{Správnosť programov}
   
Line 906  $$
Line 906  $$
 Inferenčné pravidlo pre programovú konštrukciu $P_K$ vyzerá nasledovne.  Inferenčné pravidlo pre programovú konštrukciu $P_K$ vyzerá nasledovne.
 Podrobné odvodenie je prenechané ako cvičenie pre~čitateľa.  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~\{s\}~~(p \land\lnot c \Rightarrow s)~~(r \land\lnot c  
 %\Rightarrow s)~~(s \land\lnot b \Rightarrow q)}{\{p\}~P_K~\{q\}}  
 %$$  
   
 $$  $$
 \frac{\{p \land c\}~S~\{p\}~~\{s \land b\}~S~\{r\}~~\{r \land  \frac{\{p \land c\}~S~\{p\}~~\{s \land b\}~S~\{r\}~~\{r \land
 c\}~S~\{s\}~~(p \land\lnot c \Rightarrow s)~~(r \land\lnot c  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\}}  \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\}}
 $$  $$
   
Legend:
Removed from v.1.8  
changed lines
  Added in v.1.9
Platon Group <platon@platon.org> http://platon.org/
Copyright © 2002-2006 Platon Group
Site powered by Metafox CMS 		Go to Top