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 17:44] vkuncak |
sav08:relational_semantics_of_procedures [2009/05/26 17:48] vkuncak |
||
---|---|---|---|
Line 105: | Line 105: | ||
\[ | \[ | ||
G(E,O) = | G(E,O) = | ||
- | \big( | ||
\begin{array}[t]{@{}l@{}} | \begin{array}[t]{@{}l@{}} | ||
- | ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!]) \cup | + | \bigg( ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!]) \cup |
([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ O)\ , \\ | ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ O)\ , \\ | ||
([\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) \cup | ([\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) \cup | ||
- | ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) | + | ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) \bigg) |
- | \end{array}\big) | + | \end{array} |
\] | \] | ||
- | 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. We have operations $\sqsubseteq$ and $\sqcup$ analogous to $\subseteq$ and $\cup$ (indeed, the domain ${\cal R}^d$, that is $(2^{S\times S})^d$, is isomorphic to $2^{S\times S \times \{1,2,\ldots,d\}}$). | + | 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) \sqcup (r'_1,r'_2) = (r_1 \cup r'_1, r_2 \cup r'_2) | ||
+ | \] | ||
+ | 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 meaning of all procedures is therefore the tuple $p_* \in {\cal R}^n$ given by $\bigsqcup\limits_{n \ge 0} G^n(\emptyset,\ldots,\emptyset)$. | + | We define $\sqsubseteq$ and $\sqcup$ analogous to $\subseteq$ and $\cup$ (indeed, the domain ${\cal R}^d$, that is $(2^{S\times S})^d$, is isomorphic to $2^{S\times S \times \{1,2,\ldots,d\}}$). |
- | **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$. | + | 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$. | ||