Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:relational_semantics_of_procedures [2009/05/26 22:52] vkuncak |
sav08:relational_semantics_of_procedures [2009/05/26 23:06] vkuncak |
||
|---|---|---|---|
| Line 150: | Line 150: | ||
| === Example === | === Example === | ||
| - | In the example above, we have | + | In the example above, we can prove that |
| + | \[ | ||
| + | r_{even} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land | ||
| + | (wasEven' \leftrightarrow ((x \mod 2) = 0)) | ||
| + | \] | ||
| + | \[ | ||
| + | r_{odd} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land | ||
| + | (wasEven' \leftrightarrow ((x \mod 2) \ne 0)) | ||
| + | \] | ||
| === Remark === | === Remark === | ||