Differences

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

--- sav08:collecting_semantics [2008/05/07 00:57]
vkuncak created
+++ sav08:collecting_semantics [2008/05/08 12:36]
vkuncak
@@ Line 5: / Line 5: @@
 We can represent programs by control-flow graphs (CFG).
-**Definition:** Control flow-graph is a graph with nodes $V$, edges $E \subseteq V\times V$ and for each edge $e \in E$ a command $c(e)$, with initial $init$ and final node $final$
+**Definition:** Control flow-graph is a graph with nodes $V$, edges $E \subseteq V\times V$ and for each edge $e \in E$ a command given by relation $r(e)$, with initial $init$ and final node $final$
 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$ - 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$.
@@ 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(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.
+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) \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)$.
+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**
+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>
+After the assignment of $x$ to 2, the set of reachable states $C$ is $C = \{ (x,2), (i,20), (y,t) \}$