Differences

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

--- sav08:normal_form_of_loop-free_programs [2008/03/04 17:31]
vkuncak
+++ sav08:normal_form_of_loop-free_programs [2009/03/04 18:57]
vkuncak
@@ Line 1: / Line 1: @@
-====== Normal form for loop-free programs ======
-Example:
-<code>
-(if (x < 0) x=x+1 else x=x);
-(if (y < 0) y=y+x else y=y);
-</code>
-Without loops, after expressing conditionals using [] we obtain
-  c ::=  x=T | assume(F) |  c [] c  |  c ; c
-Laws:
-\[
-     (r_1 \cup r_2) \circ r_3 = (r_1 \circ r_3) \cup (r_2 \circ r_3)
-\]
-\[
-     r_3 \circ (r_1 \cup r_2) = (r_3 \circ r_1) \cup (r_3 \circ r_2)
-\]
-Normal form:
-\[
-   \bigcup_{i=1}^n p_i
-\]
-Each $p_i$ is of form $b_1 \circ \ldots \circ b_k$ for some $k$, where each $b_i$ is assignment or assume.  Each $p_i$ corresponds to one of the finitely paths from beginning to end of the acyclic control-flow graph for loop-free program.
-Length of normal form with sequences of if-then-else.
 We want to show:
@@ Line 41: / Line 16: @@
 \]
-==== Three Approaches ====
+Note: the rule also applies to infinite union of paths (e.g. generated by loops).
-Three equivalent formulations of Hoare triple give us three approaches:
+===== Three Approaches to Generate Verification Conditions =====
-  - compute meaning of $c$, then check Hoare triple (compositional approach for verification-condition generation)
-  - compute $sp(P,r)$ then check entailment $sp(P,r) \subseteq Q$ (forward symbolic execution)
-  - compute $wp(Q,r)$, then check $P \subseteq wp(Q,r)$ (backward symbolic execution)
+Three equivalent formulations of Hoare triple give us three approaches:
+  - compute meaning of $c$ as a formula, then check Hoare triple (compositional approach for verification-condition generation)
+  - compute $sp(P,r)$ as a formula, then check entailment $sp(P,r) \subseteq Q$ (forward symbolic execution)
+  - compute $wp(Q,r)$ as a formula, then check $P \subseteq wp(Q,r)$ (backward symbolic execution)