LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:review_of_fixpoints_in_semantics [2008/05/07 22:58]
giuliano
sav08:review_of_fixpoints_in_semantics [2015/04/21 17:30] (current)
Line 4: Line 4:
  
 Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation
-\[+\begin{equation*}
     r^* = \bigcup_{n \ge 0} r^n     r^* = \bigcup_{n \ge 0} r^n
-\]+\end{equation*}
 where $r^0 = \Delta_D$. where $r^0 = \Delta_D$.
  
Line 23: Line 23:
  
 This can be written as  This can be written as 
-\[+\begin{equation*}
    p = F(p)    p = F(p)
-\]+\end{equation*}
 where  where 
   F(p) = if (c) then (s;p) else skip   F(p) = if (c) then (s;p) else skip
Line 35: Line 35:
  
 If $r_s$ is meaning of $s$ and $\Delta_c$ is meaning of //assume( c )//, the meaning is the fixpoint of function If $r_s$ is meaning of $s$ and $\Delta_c$ is meaning of //assume( c )//, the meaning is the fixpoint of function
-\[+\begin{equation*}
     f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c}     f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c}
-\]+\end{equation*}
  
 Any program can be reduced to a loop: Any program can be reduced to a loop:
Line 71: Line 71:
  
 The set of reachable states is defined as the least solution of constraints:​ The set of reachable states is defined as the least solution of constraints:​
-\[+\begin{equation*}
   I \subseteq C(p_0)   I \subseteq C(p_0)
-\] +\end{equation*} 
-\[+\begin{equation*}
   \bigwedge_{(p_1,​p_2) \in E} sp(C(p),​r(c(p_1,​p_2)))) \subseteq C(p_2)   \bigwedge_{(p_1,​p_2) \in E} sp(C(p),​r(c(p_1,​p_2)))) \subseteq C(p_2)
-\]+\end{equation*}
 where $c(p_1,​p_2)$ is command associated with edge $(p_1,​p_2)$,​ and $r(c(p_1,​p_2))$ is the relation giving semantics for this command. where $c(p_1,​p_2)$ is command associated with edge $(p_1,​p_2)$,​ and $r(c(p_1,​p_2))$ is the relation giving semantics for this command.