Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:compositional_vcg [2009/03/04 11:11] vkuncak |
sav08:compositional_vcg [2009/03/04 23:50] vkuncak |
||
---|---|---|---|
Line 32: | Line 32: | ||
\forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q) | \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 ===== | ===== Rules for Computing Formulas for Commands ===== | ||
Line 61: | Line 63: | ||
Note | 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, | Therefore, | ||
Line 72: | Line 74: | ||
Note that | 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, | 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$. | + | Above, $F_c(c_1)[\vec x':=\vec z]$ denotes taking formula $F_c(c_1)$ and replacing in it occurrences of variables $\vec x'$ by variables $\vec z$. |
+ | To avoid re-using variables, introduce always a fresh variable as $\vec z$ and denote it $\vec z_i$. | ||
===== Using Computed Formulas ===== | ===== Using Computed Formulas ===== |