Differences

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

--- sav08:compositional_vcg [2008/03/04 22:27]
vkuncak
+++ sav08:compositional_vcg [2009/03/04 23:49]
vkuncak
@@ Line 32: / Line 32: @@
     \forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q)
 \]
 ===== Rules for Computing Formulas for Commands =====
@@ Line 61: / Line 62: @@
 Note
 \[
-   \{(x,x') \mid F_1 \} \cup \{(x,x') \mid F_2 \} = \{(x,x') \mid F_1 \lor F_2 \}
+   \{(\vec x,\vec x') \mid F_1 \} \cup \{(\vec x,\vec x') \mid F_2 \} = \{(\vec x,\vec x') \mid F_1 \lor F_2 \}
 \]
 Therefore,
@@ Line 72: / Line 73: @@
 Note that
 \[
-    \{(x,x') \mid F_1 \} \circ \{(x,x') \mid F_2 \} = \{ (x,z) \mid F_1[x':=z] \} \circ \{ (z,x') \mid F_2[x:=z] \} = \{ (x,z) \mid \exists z. F_1[x':=z] \land F_2[x:=z] \}
+    \{(\vec x,\vec x') \mid F_1 \} \circ \{(\vec x,\vec x') \mid F_2 \} = \{ (\vec x,\vec z) \mid F_1[\vec x':=\vec z] \} \circ \{ (\vec z,x') \mid F_2[\vec x:=\vec z] \} = \{ (\vec x,\vec z) \mid \exists \vec z. F_1[\vec x':=\vec z] \land F_2[\vec x:=\vec z] \}
 \]
 Therefore,
 \[
-   F_c(c_1\ ;\ c_2)\ =\ (\exists z. F_c(c_1)[x':=z] \land F_c(c_2)[x:=z])
+   F_c(c_1\ ;\ c_2)\ =\ (\exists \vec z. F_c(c_1)[\vec x':=\vec z] \land F_c(c_2)[\vec x:=\vec z])
 \]
-To avoid re-using variables, introduce always a fresh variable as //z//, denote it $z_i$.
+To avoid re-using variables, introduce always a fresh variable as //\vec z//, denote it $\vec z_i$.
 ===== Using Computed Formulas =====
@@ Line 149: / Line 150: @@
 Using valid formulas we can move the existential quantifiers outside the formula.
+However, we can avoid expanding all paths and instead compute relations by following program structure.
 ===== Size of Generated Formulas =====