This is an old revision of the document!
Normal form for loop-free programs
Example:
(if (x < 0) x=x+1 else x=x); (if (y < 0) y=y+x else y=y);
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 is of form for some , where each is assignment or assume. Each 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: \[
\{ P \} r \{ Q \}
\]
Verifying Each Path Separately
By normal form this is \[
\{ P \} \bigcup_{i=1}^n p_i \{ Q \}
\] which is equivalent to \[
\bigwedge_{i=1}^n (\{P\} p_i \{Q\})
\]
Note: the rule also applies to infinite union of paths (e.g. generated by loops).
Three Approaches to Generate Verification Conditions
Three equivalent formulations of Hoare triple give us three approaches:
- compute meaning of as a formula, then check Hoare triple (compositional approach for verification-condition generation)
- compute as a formula, then check entailment (forward symbolic execution)
- compute as a formula, then check (backward symbolic execution)