Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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