This is an old revision of the document!
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)