Rozdiely pre doc/ztp-zbierka/03-spravnost-programov.tex medzi verziami 1.8 a 1.9
| verzia 1.8, 2007/04/29 19:39:13 |
verzia 1.9, 2007/05/27 16:38:21 |
|
|
| % 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} |
| |
|
|
|
| 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\}} |
| $$ |
$$ |
| |
|
Platon Group <platon@platon.sk> http://platon.sk/
|
|
Prihlásiť
Registrácia
English
![[BACK]](http://cvsweb.platon.sk/icons/back.gif){kind=icon}
![[TXT]](http://cvsweb.platon.sk/icons/text.gif){kind=icon}
![[DIR]](http://cvsweb.platon.sk/icons/dir.gif){kind=icon}
Vyššie na