LARA

Differences

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

Link to this comparison view

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 variablesintroduce 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 =====