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:collecting_semantics [2008/05/07 08:08]
vkuncak 		sav08:collecting_semantics [2008/05/08 12:37]
vkuncak
Line 9: Line 9:
 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$ - states describing values of program variables (not including program counter). $PS$ - states describing values of program variables (not including program counter).
Line 27: Line 27:
 \] \]
 over variables $C(p)$ for all of finitely many program points $p$. over variables $C(p)$ for all of finitely many program points $p$.
 +
 +The last condition is equivalent to
 +\[
 +  \bigwedge_{p_2 \in V}\ \left( C(p_2) = C(p_2) \cup \bigcup_{(p_1,​p_2) \in E} sp(C(p_1),​r(p_1,​p_2))) \right)
 +\]
  
 Here $r(p_1,​p_2)$ is the relation giving semantics for the command associated with edge $(p_1,​p_2)$. Here $r(p_1,​p_2)$ is the relation giving semantics for the command associated with edge $(p_1,​p_2)$.
  
 Set of recursive inequations in the lattice of products of sets.  Note $e_1 \subseteq e_2$ is equivalent to $e_2 = e_1 \cup e_2$, so we have equations in lattice. Set of recursive inequations in the lattice of products of sets.  Note $e_1 \subseteq e_2$ is equivalent to $e_2 = e_1 \cup e_2$, so we have equations in lattice.
 +
 +They specify function $G$ from pairs of sets of states to pairs of sets of states which is $\cup$-morphism (and therefore monotonic).
 +
 +Least fixpoint of $G$ is $\bigcup_{i \ge 0} G^i(\emptyset)$.
  
 **Example** **Example**
Line 49: Line 58:
 } }
 </​code>​ </​code>​
 +After the assignment of $x$ to 2, the set of reachable states $C$ is $C = \{ (x,2), (i,20), (y,t) \}$