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.10 and 1.11


version 1.10, 2007/08/20 08:42:59
version 1.11, 2007/08/20 09:26:39



Line 10 




Line 10 




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


 %
 %


 
 


 % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.9 2007-05-27 16:38:21 nepto Exp $
 % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.10 2007-08-20 08:42:59 nepto Exp $


 
 


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


 
 




Line 338  správnosť programu~$P$ dokázaná.




Line 338  správnosť programu~$P$ dokázaná.




 
 


 \end{solution} % */
 \end{solution} % */


 
 


 
 \begin{definition}[Jazyk] % /*


 
         Jazykom sú dobre vytvorené formuly $\alpha, \beta$.


 
 \end{definition} % */


 
 


 
 \begin{definition} % /*


 
         Platnosť (pravdivosť) formúl označujeme $\models \alpha$. Znamená


 
         to, že formula $\alpha$ platí v~danej triede modelov.


 
 \end{definition} % */


 
 


 
 \begin{definition}[Dokazovací systém] % /*


 
         Dokázateľnosť (odvoditeľnosť) formúl označujeme $\vdash \alpha$. Formula $\alpha$ sa


 
         dá dokázať (odvodiť) z axióm a inferenčných pravidiel systému:


 
         $$


 
         \frac{\alpha_1 \dots \alpha_n}{\beta}


 
         $$


 
 \end{definition} % */


 
 


 
 \begin{definition}[Zdravý systém] % /*


 
         Zdravý systém je taký, v ktorom dokázateľné sú len pravdivé formuly.


 
         $$


 
         \vdash \alpha ~ \Rightarrow ~ \models \alpha


 
         $$


 
 \end{definition} % */


 
 


 
 \begin{definition}[Úplný systém] % /*


 
         Úplný systém je taký, v ktorom každá pravdivá formula je


 
         dokázateľná.


 
         $$


 
         \models \alpha ~ \Rightarrow ~ \vdash \alpha


 
         $$


 
 \end{definition} % */


 
 


 
 \begin{definition}[Hoareova metóda] % /*


 
 Hoareova metóda používa logický systém pre dokazovanie čiastočnej


 
 správnosti programov založený na jazyku induktívnych formúl


 
 $$


 
 \{p\} P \{q\}


 
 $$


 
 \end{definition} % */


 
 


 
 \begin{definition}[Induktívna formula] % /*


 
         Význam induktívnej (invariantnej) formuly


 
         $$


 
         \models ~ \{p\} P \{q\}


 
         $$


 
         závisí od významu podmienok $p, q$ a významu programu $P$.


 
 


 
         Formula je teda pravdivá práve vtedy, ak vstupné hodnoty programu


 
         $P$ spĺňajú podmienku $p$ a po zastavení programu (príkazu) $P$


 
         výstupné hodnoty $P$ vyhovujú podmienke $q$.


 
 \end{definition} % */


 
 


 
 \begin{definition}[Najslabšia vstupná podmienka] % /*


 
         Označujeme $wp(P, q)$.


 
 


 
         K programu $P$ a výstupnej podmienke $q$:\\


 
         $\forall p$ ak platí $\{wp(P,q)\} P \{q\}, \{p\} P \{q\}$ potom $p


 
         \Rightarrow wp(P, q)$


 
 \end{definition} % */


 
 


 
 \begin{definition}[Najsilnejšia výstupná podmienka] % /*


 
         Označujeme $sp(P, p)$.


 
 


 
         K programu $P$ a vstupnej podmienke $q$:\\


 
         $\forall q$ ak platí $\{p\} P \{sp(P,p)\}, \{p\} P \{q\}$ potom


 
         $sp(P, p) \Rightarrow q$


 
 \end{definition} % */


 
 


 
 \begin{definition}[Inferenčný systém $\mathcal{H}$] % /*


 
         Inferenčný systém pozostáva z troch pravidiel a z jednej axiómy


 
         priradenia:


 
 


 
         \begin{itemize}


 
                 \item \bf{Axiomatická schéma priradenia}


 
                         $$


 
                         \{p(\overline{x}, g(\overline{x}, \overline{y}))\}


 
                         ~ \overline{y} := g(\overline{x}, \overline{y}) ~


 
                         \{p(\overline{x}, \overline{y})\}


 
                         $$


 
                         $$


 
                         \{q[x/s]\} ~ x := s ~ \{q\}


 
                         $$


 
                 \item \bf{Kompozičné pravidlo}


 
                         $$


 
                         \frac{\{p\} S_1 \{q\} ~ ~ ~ \{q\} S_2 \{r\}}{\{p\} S_1; S_2


 
                         \{r\}}


 
                         $$


 
                 \item \bf{Alternatívne pravidlo}


 
                         $$


 
                         \frac{\{p \land b\} S_1 \{q\} ~ ~ ~ \{p \land \lnot b\} S_2


 
                         \{q\}}{\{p\} ~\cmd{if}~ b ~\cmd{then}~ S_1 ~\cmd{else}~ S_2


 
                         ~\cmd{fi}~ \{q\}}


 
                         $$


 
                 \item \bf{Iteratívne pravidlo}


 
                         $$


 
                         \frac{\{p \land b\} S \{p\}}{\{p\} ~\cmd{while}~ b ~\cmd{do}~


 
                         S ~\cmd{od}~ \{p \land \lnot b\}}


 
                         $$


 
         \end{itemize}


 
 \end{definition} % */


 
 


 \begin{example} % /* Hoare I.
 \begin{example} % /* Hoare I.


 
 


 Daný je štruktúrovaný program $P$.
 Daný je štruktúrovaný program $P$.









Legend:


Removed from v.1.10
 


changed lines


 
Added in v.1.11


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / ztp-zbierka
-version 1.10, 2007/08/20 08:42:59
+version 1.11, 2007/08/20 09:26:39
 Line 10
 Line 10
 Line 10
  % 26/02/2003 - created
  %
- % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.9 2007-05-27 16:38:21 nepto Exp $
+ % $Platon: doc/ztp-zbierka/03-spravnost-programov.tex,v 1.10 2007-08-20 08:42:59 nepto Exp $
  \chapter{Správnosť programov}
 Line 338  správnosť programu~$P$ dokázaná.
 Line 338  správnosť programu~$P$ dokázaná.
 Line 338  správnosť programu~$P$ dokázaná.
  \end{solution} % */
+ \begin{definition}[Jazyk] % /*
+         Jazykom sú dobre vytvorené formuly $\alpha, \beta$.
+ \end{definition} % */
+ \begin{definition} % /*
+         Platnosť (pravdivosť) formúl označujeme $\models \alpha$. Znamená
+         to, že formula $\alpha$ platí v~danej triede modelov.
+ \end{definition} % */
+ \begin{definition}[Dokazovací systém] % /*
+         Dokázateľnosť (odvoditeľnosť) formúl označujeme $\vdash \alpha$. Formula $\alpha$ sa
+         dá dokázať (odvodiť) z axióm a inferenčných pravidiel systému:
+         $$
+         \frac{\alpha_1 \dots \alpha_n}{\beta}
+         $$
+ \end{definition} % */
+ \begin{definition}[Zdravý systém] % /*
+         Zdravý systém je taký, v ktorom dokázateľné sú len pravdivé formuly.
+         $$
+         \vdash \alpha ~ \Rightarrow ~ \models \alpha
+         $$
+ \end{definition} % */
+ \begin{definition}[Úplný systém] % /*
+         Úplný systém je taký, v ktorom každá pravdivá formula je
+         dokázateľná.
+         $$
+         \models \alpha ~ \Rightarrow ~ \vdash \alpha
+         $$
+ \end{definition} % */
+ \begin{definition}[Hoareova metóda] % /*
+ Hoareova metóda používa logický systém pre dokazovanie čiastočnej
+ správnosti programov založený na jazyku induktívnych formúl
+ $$
+ \{p\} P \{q\}
+ $$
+ \end{definition} % */
+ \begin{definition}[Induktívna formula] % /*
+         Význam induktívnej (invariantnej) formuly
+         $$
+         \models ~ \{p\} P \{q\}
+         $$
+         závisí od významu podmienok $p, q$ a významu programu $P$.
+         Formula je teda pravdivá práve vtedy, ak vstupné hodnoty programu
+         $P$ spĺňajú podmienku $p$ a po zastavení programu (príkazu) $P$
+         výstupné hodnoty $P$ vyhovujú podmienke $q$.
+ \end{definition} % */
+ \begin{definition}[Najslabšia vstupná podmienka] % /*
+         Označujeme $wp(P, q)$.
+         K programu $P$ a výstupnej podmienke $q$:\\
+         $\forall p$ ak platí $\{wp(P,q)\} P \{q\}, \{p\} P \{q\}$ potom $p
+         \Rightarrow wp(P, q)$
+ \end{definition} % */
+ \begin{definition}[Najsilnejšia výstupná podmienka] % /*
+         Označujeme $sp(P, p)$.
+         K programu $P$ a vstupnej podmienke $q$:\\
+         $\forall q$ ak platí $\{p\} P \{sp(P,p)\}, \{p\} P \{q\}$ potom
+         $sp(P, p) \Rightarrow q$
+ \end{definition} % */
+ \begin{definition}[Inferenčný systém $\mathcal{H}$] % /*
+         Inferenčný systém pozostáva z troch pravidiel a z jednej axiómy
+         priradenia:
+         \begin{itemize}
+                 \item \bf{Axiomatická schéma priradenia}
+                         $$
+                         \{p(\overline{x}, g(\overline{x}, \overline{y}))\}
+                         ~ \overline{y} := g(\overline{x}, \overline{y}) ~
+                         \{p(\overline{x}, \overline{y})\}
+                         $$
+                         $$
+                         \{q[x/s]\} ~ x := s ~ \{q\}
+                         $$
+                 \item \bf{Kompozičné pravidlo}
+                         $$
+                         \frac{\{p\} S_1 \{q\} ~ ~ ~ \{q\} S_2 \{r\}}{\{p\} S_1; S_2
+                         \{r\}}
+                         $$
+                 \item \bf{Alternatívne pravidlo}
+                         $$
+                         \frac{\{p \land b\} S_1 \{q\} ~ ~ ~ \{p \land \lnot b\} S_2
+                         \{q\}}{\{p\} ~\cmd{if}~ b ~\cmd{then}~ S_1 ~\cmd{else}~ S_2
+                         ~\cmd{fi}~ \{q\}}
+                         $$
+                 \item \bf{Iteratívne pravidlo}
+                         $$
+                         \frac{\{p \land b\} S \{p\}}{\{p\} ~\cmd{while}~ b ~\cmd{do}~
+                         S ~\cmd{od}~ \{p \land \lnot b\}}
+                         $$
+         \end{itemize}
+ \end{definition} % */
  \begin{example} % /* Hoare I.
  Daný je štruktúrovaný program $P$.
 Legend:


Removed from v.1.10
 


changed lines


 
Added in v.1.11
 Legend:


Removed from v.1.10
 


changed lines


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


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