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:48] vkuncak |
sav08:relational_semantics_of_procedures [2009/05/26 17:59] vkuncak |
||
---|---|---|---|
Line 115: | Line 115: | ||
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. | ||