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 17:48] vkuncak |
sav08:relational_semantics_of_procedures [2009/05/26 23:06] vkuncak |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| How can we define semantics for program with recursive procedures? | How can we define semantics for program with recursive procedures? | ||
| + | |||
| + | We consider first the case of procedures without parameters; adding parameters is straightforward. | ||
| ===== One Recursive Procedure ===== | ===== One Recursive Procedure ===== | ||
| Line 60: | 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 | 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}$. | 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 ===== | ===== Multiple Mutually Recursive Procedures ===== | ||
| Line 115: | Line 122: | ||
| We define lattice structure on ${\cal R}^2$ by | We define lattice structure on ${\cal R}^2$ by | ||
| \[ | \[ | ||
| - | (r_1,r_2) \sqsubseteq (r'_1,r'_2) \ \mbox{iff} (r_1 \subseteq r'_1) \land (r_2 \subseteq r'_2) | + | (r_1,r_2) \sqsubseteq (r'_1,r'_2) \ \mbox{ iff } \ (r_1 \subseteq r'_1) \land (r_2 \subseteq r'_2) |
| \] | \] | ||
| \[ | \[ | ||
| (r_1,r_2) \sqcup (r'_1,r'_2) = (r_1 \cup r'_1, r_2 \cup r'_2) | (r_1,r_2) \sqcup (r'_1,r'_2) = (r_1 \cup r'_1, r_2 \cup r'_2) | ||
| \] | \] | ||
| + | Note that: | ||
| + | \[ | ||
| + | G(\emptyset,\emptyset) = ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!], [\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) | ||
| + | \] | ||
| + | \[ | ||
| + | G(G(\emptyset,\emptyset)) = | ||
| + | \begin{array}[t]{@{}l@{}} | ||
| + | \bigg( ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!]) \cup | ||
| + | ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,\emptyset).\_2)\ , \\ | ||
| + | ([\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) \cup | ||
| + | ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,\emptyset).\_1) \bigg) | ||
| + | \end{array} | ||
| + | \] | ||
| + | where $p.\_1$ and $p.\_2$ denote first, respectively, second, element of the pair $p$. | ||
| + | |||
| The results extend to any number of call sites and any number of mutually recursive procedures, we just consider a function $G : {\cal R}^d \to {\cal R}^d$ where $d$ is the number of procedures; this mapping describes how, given one approximation of procedure semantics, compute a better approximation that is correct for longer executions. | The results extend to any number of call sites and any number of mutually recursive procedures, we just consider a function $G : {\cal R}^d \to {\cal R}^d$ where $d$ is the number of procedures; this mapping describes how, given one approximation of procedure semantics, compute a better approximation that is correct for longer executions. | ||
| Line 126: | 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)$. | 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 \mod 2) = 0)) | ||
| + | \] | ||
| + | \[ | ||
| + | r_{odd} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land | ||
| + | (wasEven' \leftrightarrow ((x \mod 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$. | ||