Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:review_of_fixpoints_in_semantics [2008/04/30 11:05]
vkuncak
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 60: Line 60:
 Program points are CFG nodes. ​ Statements are labels on CFG edges. Program points are CFG nodes. ​ Statements are labels on CFG edges.
  
-We look at a particular way of representing and computing sets of reachable, splitting states by program counter (control-flow graph node): **collecting semantics**.+We look at a particular way of representing and computing sets of reachable ​states, splitting states by program counter (control-flow graph node): **collecting semantics**.
  
 $PS$ - the set of values of program variables (not including program counter). $PS$ - the set of values of program variables (not including program counter).
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.
  
 
sav08/review_of_fixpoints_in_semantics.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice