Differences

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

--- sav08:relational_semantics_of_procedures [2009/05/26 17:48]
vkuncak
+++ sav08:relational_semantics_of_procedures [2009/05/26 20:35]
vkuncak
@@ Line 10: / Line 10: @@
 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 =====
@@ Line 115: / Line 117: @@
 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)
 \]
+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.