Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:normal_form_of_loop-free_programs [2008/03/04 17:32] vkuncak |
sav08:normal_form_of_loop-free_programs [2009/03/04 18:58] vkuncak |
||
---|---|---|---|
Line 40: | Line 40: | ||
\bigwedge_{i=1}^n (\{P\} p_i \{Q\}) | \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 Approaches to Generate Verification Conditions ===== | ||
Line 47: | Line 49: | ||
- compute $sp(P,r)$ as a formula, then check entailment $sp(P,r) \subseteq Q$ (forward symbolic execution) | - 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) | - compute $wp(Q,r)$ as a formula, then check $P \subseteq wp(Q,r)$ (backward symbolic execution) | ||
- |