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
Next revision Both sides next revision
sav08:collecting_semantics [2008/05/07 08:08]
vkuncak 		sav08:collecting_semantics [2008/05/08 12:36]
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} C(p_2) = C(p_2) \bigcup_{(p_1,​p_2) \in E} \sp(C(p_1),​r(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)$. 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) \}$