Differences
This shows you the differences between two versions of the page.
sav08:normal_form_of_loop-free_programs [2009/03/04 18:57] vkuncak |
sav08:normal_form_of_loop-free_programs [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | 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 $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) |