Rozdiely pre doc/ztp-zbierka/03-spravnost-programov.tex medzi verziami 1.2 a 1.3
| verzia 1.2, 2003/10/10 13:40:35 |
verzia 1.3, 2004/03/15 10:24:47 |
|
|
| % 26/02/2003 - created |
% 26/02/2003 - created |
| % |
% |
| |
|
| % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.1 2003/07/18 17:07:11 nepto Exp $ |
% $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.2 2003/10/10 13:40:35 nepto Exp $ |
| |
|
| \chapter{Správnosť programov} |
\chapter{Správnosť programov} |
| |
|
| Riadok 440 vychádzať z~poslednej implikácie a odvod |
|
| Riadok 440 vychádzať z~poslednej implikácie a odvod |
|
| od~výstupnej podmienky~$q$. |
od~výstupnej podmienky~$q$. |
| |
|
| V~našom prípade je podmienka~$r$ rovnaká, ako prislúchajúci invariant |
V~našom prípade je podmienka~$r$ rovnaká, ako prislúchajúci invariant |
| v~ekvivalentnom štandartnom programe dokazovanom Floydovou metódou. |
v~ekvivalentnom štandardnom programe dokazovanom Floydovou metódou. |
| |
|
| $$ |
$$ |
| r ~\equiv~ y_1^2 = y_2 ~\land~ (y_1 - 1)^2 < x |
r ~\equiv~ y_1^2 = y_2 ~\land~ (y_1 - 1)^2 < x |
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