LARA

Differences

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

Link to this comparison view

Next revision 		Previous revision
Next revision Both sides next revision
sav08:collecting_semantics [2008/05/07 00:57]
vkuncak created 		sav08:collecting_semantics [2008/05/07 01:24]
vkuncak
Line 11: Line 11:
 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, splitting states by program counter (control-flow graph node): **collecting semantics**.
  
-$PS$ - the set of values of program variables (not including program counter).+$PS$ - states describing ​values of program variables (not including program counter).
  
 For each program point $p$, we have the set of reachable states $C(p) \subseteq PS$. For each program point $p$, we have the set of reachable states $C(p) \subseteq PS$.
Line 24: Line 24:
 \] \]
 \[ \[
-  \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_1),​r(c(p_1,​p_2)))) \subseteq C(p_2)
 \] \]
 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.
 +
 +Set of recursive inequations in the lattice of products of sets.  Note $e_1 \subseteq e_2$ is equivalent to $e_1 \cap e_2 = e_1$, so we have equations in lattice.
 +
 +**Example**
 +
 +Sets of states at selected points:
 +
 +<​code>​
 +i = 20;
 +x = 2;
 +while (i > 0) {
 +  x = x + 4;
 +  i = i - 1;
 +}
 +if (x==0) {
 +  error;
 +} else {
 +  y = 1000/x;
 +}
 +</​code>​