Opensource.Platon.SK CVS: doc/ztp-zbierka/03-spravnost-programov.tex - diff

   Up to  [Platon] / doc / ztp-zbierka
Diff for doc/ztp-zbierka/03-spravnost-programov.tex between version 1.9 and 1.10


version 1.9, 2007/05/27 16:38:21
version 1.10, 2007/08/20 08:42:59



Line 10 




Line 10 




 % 26/02/2003 - created
 % 26/02/2003 - created


 %
 %


 
 


 % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.8 2007-04-29 19:39:13 nepto Exp $
 % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.9 2007-05-27 16:38:21 nepto Exp $


 
 


 \chapter{Správnosť programov}
 \chapter{Správnosť programov}


 
 


 \section{Metódy dokazovania správnosti}
 \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.
 \begin{example} % /* Floyd I.


 
 


 Uvažujme nasledujúci štandardný program~$P$, ktorý počíta
 Uvažujme nasledujúci štandardný program~$P$, ktorý počíta









Legend:


Removed from v.1.9
 


changed lines


 
Added in v.1.10


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / ztp-zbierka
-version 1.9, 2007/05/27 16:38:21
+version 1.10, 2007/08/20 08:42:59
 Line 10
 Line 10
 Line 10
  % 26/02/2003 - created
  %
- % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.8 2007-04-29 19:39:13 nepto Exp $
+ % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.9 2007-05-27 16:38:21 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
 Legend:


Removed from v.1.9
 


changed lines


 
Added in v.1.10
 Legend:


Removed from v.1.9
 


changed lines


 
Added in v.1.10
-Removed from v.1.9
+Added in v.1.10


Copyright © 2002-2006 Platon Group Site powered by Metafox CMS	Go to Top