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:relational_semantics_of_procedures [2009/05/26 22:52] vkuncak |
sav08:relational_semantics_of_procedures [2009/05/26 23:02] 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 \pmod 2 = 0)) | ||
+ | \] | ||
+ | \[ | ||
+ | r_{odd} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land | ||
+ | (wasEven' \leftrightarrow (x \pmod 2 \ne 0)) | ||
+ | \] | ||
=== Remark === | === Remark === |