Opensource.Platon.SK CVS: doc/statnica-teoria-prog/04-semantika-programovaich-jazykov.tex - diff

   Up to  [Platon] / doc / statnica-teoria-prog
Diff for doc/statnica-teoria-prog/04-semantika-programovaich-jazykov.tex between version 1.1 and 1.2


version 1.1, 2006/08/17 08:04:27
version 1.2, 2006/08/18 23:29:56



Line 10 




Line 10 




 % 2006-08-17 - created
 % 2006-08-17 - created


 %
 %


 
 


 % $Platon: $
 % $Platon: doc/statnica-teoria-prog/04-semantika-programovaich-jazykov.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $


 
 


 \chapter{Sémantika programovacích jazykov}
 \chapter{Sémantika programovacích jazykov}


 
 


 
 \section{Modálne vlastnosti} % /*


 
 


 
 \begin{defn}[Hennesy-Milner Logic]


 
         $$


 
         \phi = true ~|~ false ~|~ \phi_1 \land \phi_2 ~|~ \phi_1 \lor \phi_2 ~|~ [k]\phi ~|~ \langle k \rangle


 
         \phi, k \in Act


 
         $$


 
 \end{defn}


 
 


 
 \begin{defn} ~


 
         \begin{enumerate}


 
                 \item $P \models true$


 
                 \item $P \models ff$


 
                 \item $P \models \phi \land \psi \iff P \models \phi \land P \models \psi$


 
                 \item $P \models \phi \lor \psi \iff P \models \phi \lor P \models \psi$


 
                 \item $P \models [k]\phi \iff \forall R \in \{P'~|~P\stackrel{x}{\to}P' \land x \in K\}


 
                         ~ R \models \phi$


 
                 \item $P \models \langle k \rangle\phi \iff \exists R \in \{P'~|~P\stackrel{x}{\to}P' \land


 
                         x \in K\} ~ R \models \phi$


 
         \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn} ~


 
         \begin{enumerate}


 
                 \item $-K$ znamená $Act \setminus K$


 
                 \item $-a_1 ... a_n$ znamena $Act \setminus \{a_1 ... a_n\}$


 
                 \item $-$ znamená $Act \setminus \emptyset = Act$


 
         \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn} Výraz $\langle k \rangle tt \land [-k]ff \land [-]\phi$ znamená "len akcia $K$ a bude


 
         platiť $\phi$". Označujeme $(K)\phi$.


 
 \end{defn}


 
 


 
 \begin{defn} ~


 
         \begin{enumerate}


 
                 \item $P \models \lb ~ \rb\phi \iff \forall R \in \{P'~|~P\stackrel{\epsilon}{\to}P'\}


 
                         ~ R \models \phi$


 
                 \item $P \models \lc ~ \rc\phi \iff \exists R \in \{P'~|~P\stackrel{\epsilon}{\to}P'\}


 
                         ~ R \models \phi$


 
         \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn} ~


 
         \begin{enumerate}


 
                 \item $D_0 = \tau . Nil$, $D_{n+1} = \tau D_n$


 
                 \item $D_0^a = a . Nil$, $D_{n+1}^a = \tau D_n^a$


 
         \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn}


 
         Velkosť formuly, tj. počet výskytov $\land, \lor, [k], \langle k \rangle$ budeme označovať


 
         $|\Psi|$.


 
 \end{defn}


 
 


 
 % */


 
 


 
 \section{Image finite} % /*


 
 


 
 \begin{defn}


 
         Proces $P$ voláme {\it bezprostredne image finite}, ak množina $\{P ~|~ P\stackrel{x}{\to}P'$ je


 
         konečná pre všetky $x$.


 
 \end{defn}


 
 


 
 \begin{defn}


 
         Proces $P$ voláme {\it image finite}, ak každý prvok $\{P ~|~ P\stackrel{b}{\to}P', b \in Act^*$ je


 
         bezprostredne image finite.


 
 \end{defn}


 
 


 
 \begin{veta}


 
         Ak procesy $P$ a $R$ sú image finite a platí $P \models \psi$ a tiež $R \models \psi$, potom $P


 
         \sim R$.


 
 \end{veta}


 
 


 
 % */


 
 


 
 \section{Transition closed} % /*


 
 


 
 \begin{defn}


 
         Množina $\epsilon$ je {\it transition closed}, ak


 
         $$


 
         E \in \epsilon \land E \stackrel{x}{\to} F \Rightarrow F \in \epsilon


 
         $$


 
         \begin{enumerate}


 
                 \item $\mathcal{P}$ je neprázdna transition closed množina


 
                 \item $\mathcal{P}(E)$ je najmenšia transition closed množina, ktorá obsahuje $E$


 
         \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn}[Modálny Mu-kalkulus]


 
         $$


 
         \phi = Z ~|~ \phi_1 \land \phi_2 ~|~ \phi_1 \lor \phi_2 ~|~ [k]\phi ~|~ \langle k \rangle \phi


 
         ~|~ \nu Z \phi ~|~ \mu Z \phi


 
         $$


 
         \begin{itemize}


 
                 \item[--] $Z$ je propozičná premenná


 
                 \item[--] $\nu Z, \mu Z$ sú operátory prevných bodov


 
                 \item[--] $\nu Z \phi, \mu Z \phi$ -- $Z$ je viazaná


 
                 \item[--] $tt =^{def} \nu Z.Z$


 
                 \item[--] $ff =^{def} \mu Z.Z$


 
         \end{itemize}


 
 


 
         Nech $P$ je transition closed množina pocesov. $P \models^{?} \phi$ Problém je s def. $P \models


 
         \mu Z \phi$ a $P \models \nu Z \phi$.


 
 \end{defn}


 
 


 
 \begin{veta}


 
         Nech $P \models \phi$, potom $\exists P'$, že $P'$ má konečný počet stavov a $P' \models \phi$.


 
 \end{veta}


 
 


 
 % */


 
 


 
 \section{Verifikácia temporárnych vlastností} % /*


 
 


 
 Problém $E \models \phi$


 
 


 
 Hry a v nich 2 hráči:


 
 \begin{itemize}


 
         \item[--] Hráč 1 sa snaží ukázať $E \not \models \phi$.


 
         \item[--] Hráč 2 sa snaží ukázať opak.


 
 \end{itemize}


 
 


 
 Hra so začiatkom $(E_0, \phi_0)$ je konečná alebo nekonečná postupnosť


 
 $$


 
 (E_0,\phi_0) ... (E_n, \phi_n) ...


 
 $$


 
 


 
 Hráč 1 ťahá keď $\phi$ má tvar $\land, [k], \nu Z.\psi$.\\


 
 Hráč 2 ťahá keď $\phi$ má tvar $\lor, \langle k \rangle, \mu Z.\psi$.


 
 


 
 % */


 
 


 % vim: ts=4 tw=100
 % vim: ts=4 tw=100


 % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
 % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/


 
 









Legend:


Removed from v.1.1
 


changed lines


 
Added in v.1.2


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / statnica-teoria-prog
-version 1.1, 2006/08/17 08:04:27
+version 1.2, 2006/08/18 23:29:56
 Line 10
 Line 10
 Line 10
  % 2006-08-17 - created
  %
- % $Platon: $
+ % $Platon: doc/statnica-teoria-prog/04-semantika-programovaich-jazykov.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $
  \chapter{Sémantika programovacích jazykov}
+ \section{Modálne vlastnosti} % /*
+ \begin{defn}[Hennesy-Milner Logic]
+         $$
+         \phi = true ~|~ false ~|~ \phi_1 \land \phi_2 ~|~ \phi_1 \lor \phi_2 ~|~ [k]\phi ~|~ \langle k \rangle
+         \phi, k \in Act
+         $$
+ \end{defn}
+ \begin{defn} ~
+         \begin{enumerate}
+                 \item $P \models true$
+                 \item $P \models ff$
+                 \item $P \models \phi \land \psi \iff P \models \phi \land P \models \psi$
+                 \item $P \models \phi \lor \psi \iff P \models \phi \lor P \models \psi$
+                 \item $P \models [k]\phi \iff \forall R \in \{P'~|~P\stackrel{x}{\to}P' \land x \in K\}
+                         ~ R \models \phi$
+                 \item $P \models \langle k \rangle\phi \iff \exists R \in \{P'~|~P\stackrel{x}{\to}P' \land
+                         x \in K\} ~ R \models \phi$
+         \end{enumerate}
+ \end{defn}
+ \begin{defn} ~
+         \begin{enumerate}
+                 \item $-K$ znamená $Act \setminus K$
+                 \item $-a_1 ... a_n$ znamena $Act \setminus \{a_1 ... a_n\}$
+                 \item $-$ znamená $Act \setminus \emptyset = Act$
+         \end{enumerate}
+ \end{defn}
+ \begin{defn} Výraz $\langle k \rangle tt \land [-k]ff \land [-]\phi$ znamená "len akcia $K$ a bude
+         platiť $\phi$". Označujeme $(K)\phi$.
+ \end{defn}
+ \begin{defn} ~
+         \begin{enumerate}
+                 \item $P \models \lb ~ \rb\phi \iff \forall R \in \{P'~|~P\stackrel{\epsilon}{\to}P'\}
+                         ~ R \models \phi$
+                 \item $P \models \lc ~ \rc\phi \iff \exists R \in \{P'~|~P\stackrel{\epsilon}{\to}P'\}
+                         ~ R \models \phi$
+         \end{enumerate}
+ \end{defn}
+ \begin{defn} ~
+         \begin{enumerate}
+                 \item $D_0 = \tau . Nil$, $D_{n+1} = \tau D_n$
+                 \item $D_0^a = a . Nil$, $D_{n+1}^a = \tau D_n^a$
+         \end{enumerate}
+ \end{defn}
+ \begin{defn}
+         Velkosť formuly, tj. počet výskytov $\land, \lor, [k], \langle k \rangle$ budeme označovať
+         $|\Psi|$.
+ \end{defn}
+ % */
+ \section{Image finite} % /*
+ \begin{defn}
+         Proces $P$ voláme {\it bezprostredne image finite}, ak množina $\{P ~|~ P\stackrel{x}{\to}P'$ je
+         konečná pre všetky $x$.
+ \end{defn}
+ \begin{defn}
+         Proces $P$ voláme {\it image finite}, ak každý prvok $\{P ~|~ P\stackrel{b}{\to}P', b \in Act^*$ je
+         bezprostredne image finite.
+ \end{defn}
+ \begin{veta}
+         Ak procesy $P$ a $R$ sú image finite a platí $P \models \psi$ a tiež $R \models \psi$, potom $P
+         \sim R$.
+ \end{veta}
+ % */
+ \section{Transition closed} % /*
+ \begin{defn}
+         Množina $\epsilon$ je {\it transition closed}, ak
+         $$
+         E \in \epsilon \land E \stackrel{x}{\to} F \Rightarrow F \in \epsilon
+         $$
+         \begin{enumerate}
+                 \item $\mathcal{P}$ je neprázdna transition closed množina
+                 \item $\mathcal{P}(E)$ je najmenšia transition closed množina, ktorá obsahuje $E$
+         \end{enumerate}
+ \end{defn}
+ \begin{defn}[Modálny Mu-kalkulus]
+         $$
+         \phi = Z ~|~ \phi_1 \land \phi_2 ~|~ \phi_1 \lor \phi_2 ~|~ [k]\phi ~|~ \langle k \rangle \phi
+         ~|~ \nu Z \phi ~|~ \mu Z \phi
+         $$
+         \begin{itemize}
+                 \item[--] $Z$ je propozičná premenná
+                 \item[--] $\nu Z, \mu Z$ sú operátory prevných bodov
+                 \item[--] $\nu Z \phi, \mu Z \phi$ -- $Z$ je viazaná
+                 \item[--] $tt =^{def} \nu Z.Z$
+                 \item[--] $ff =^{def} \mu Z.Z$
+         \end{itemize}
+         Nech $P$ je transition closed množina pocesov. $P \models^{?} \phi$ Problém je s def. $P \models
+         \mu Z \phi$ a $P \models \nu Z \phi$.
+ \end{defn}
+ \begin{veta}
+         Nech $P \models \phi$, potom $\exists P'$, že $P'$ má konečný počet stavov a $P' \models \phi$.
+ \end{veta}
+ % */
+ \section{Verifikácia temporárnych vlastností} % /*
+ Problém $E \models \phi$
+ Hry a v nich 2 hráči:
+ \begin{itemize}
+         \item[--] Hráč 1 sa snaží ukázať $E \not \models \phi$.
+         \item[--] Hráč 2 sa snaží ukázať opak.
+ \end{itemize}
+ Hra so začiatkom $(E_0, \phi_0)$ je konečná alebo nekonečná postupnosť
+ $$
+ (E_0,\phi_0) ... (E_n, \phi_n) ...
+ $$
+ Hráč 1 ťahá keď $\phi$ má tvar $\land, [k], \nu Z.\psi$.\\
+ Hráč 2 ťahá keď $\phi$ má tvar $\lor, \langle k \rangle, \mu Z.\psi$.
+ % */
  % vim: ts=4 tw=100
  % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
 Legend:


Removed from v.1.1
 


changed lines


 
Added in v.1.2
 Legend:


Removed from v.1.1
 


changed lines


 
Added in v.1.2
-Removed from v.1.1
+Added in v.1.2


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