Differences

This shows you the differences between two versions of the page.

--- sav08:relational_semantics_of_procedures [2009/05/26 20:35]
vkuncak
+++ sav08:relational_semantics_of_procedures [2009/05/26 23:02]
vkuncak
@@ Line 62: / Line 62: @@
 In fact, $F^n(\emptyset)$ represents the result of inlining the recursive procedure $n$ times. Therefore, if $s_0$ is the initial state such
 that the computation in the procedure terminates within $n$ steps, then $(s_0,s) \in F^n(\emptyset)$ iff $(s_0,s) \in r_{move}$.
+In this example, we have
+\[
+   r_{move} = \{((x,y),(x',y').\ (x > 0 \land x'=0 \land y'=x+y) \lor (x \le 0 \land x'=x \land y'=y) \}
+\]
 ===== Multiple Mutually Recursive Procedures =====
@@ Line 143: / Line 148: @@
 The meaning of all procedures is then the tuple $p_* \in {\cal R}^n$ given by $\bigsqcup\limits_{n \ge 0} G^n(\emptyset,\ldots,\emptyset)$.
-**Remark:** $p_*$ is the least fixpoint of $G$, so by [[sav08:Tarski's Fixpoint Theorem]], it is also the least $p$ such that $G(p) \sqsubseteq p$. Thus, $G(p) \sqsubseteq p$ implies $p_* \sqsubseteq p$.
+=== Example ===
+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 ===
+$p_*$ is the least fixpoint of $G$, so by [[sav08:Tarski's Fixpoint Theorem]], it is also the least $p$ such that $G(p) \sqsubseteq p$. Thus, $G(p) \sqsubseteq p$ implies $p_* \sqsubseteq p$.