Differences

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

--- sav08:collecting_semantics [2008/05/07 07:56]
vkuncak
+++ sav08:collecting_semantics [2008/05/07 08:08]
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.
@@ Line 24: / Line 24: @@
 \]
 \[
-  \bigwedge_{(p_1,p_2) \in E} sp(C(p_1),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$.
+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.