Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:normal_form_of_loop-free_programs [2008/03/04 17:31] vkuncak |
sav08:normal_form_of_loop-free_programs [2008/03/05 10:48] vkuncak |
||
|---|---|---|---|
| Line 41: | Line 41: | ||
| \] | \] | ||
| - | ==== 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) | ||