LARA

Differences

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

Link to this comparison view

sav08:relational_semantics_of_procedures [2009/05/26 23:02]
vkuncak
sav08:relational_semantics_of_procedures [2015/04/21 17:30]
Line 1: Line 1:
-====== Relational Semantics of Procedures ====== 
- 
-Let $S$ be the set of states and ${\cal R}$ denote $2^{S\times S}$, the set of all relations on $S$. 
- 
-In [[Relational Semantics]] for a language without procedures we had semantic function that maps programs to relations 
-\[ 
-   r_c : C \to {\cal R} 
-\] 
-so $r_c(c_1)$ was the relation corresponding to the command $c_1$, and we denote it by $[\![c_1]\!]$. 
- 
-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 ===== 
- 
-We first illustrate the semantics for one recursive procedure. The definition only relies on the [[sav08:​Lattices]] structure, so it generalizes to recursive definitions with multiple procedures, and recursive definitions in general. 
- 
-**Example:​** Consider the following procedure that, if $x,y$ are positive, moves the content of x into y. 
-<​code>​ 
-  var x,y; 
-  proc move() { 
-     if (x > 0) { 
-       x = x - 1; 
-       ​move();​ 
-       y = y + 1; 
-     } 
-  } 
-</​code>​ 
-or, expressed using non-deterministic choice and assume: 
-<​code>​ 
-  var x,y; 
-  proc move() { 
-     ( assume(x>​0);​ 
-       x = x - 1; 
-       ​move();​ 
-       y = y + 1; 
-     ​) ​ 
-     [] (assume (!(x>0)) 
-  } 
-</​code>​ 
-Suppose we have relation $r_{move}$ describing the meaning of the procedure. By [[Relational Semantics]],​ this procedure should behave similarly as the meanings of commands, so we should have the following equation: 
-\[ 
-   ​r_{move} = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!] 
-\] 
-Denoting the right-hand side by $F(r_{move})$,​ we can write the above as 
-\[ 
-   ​r_{move} = F(r_{move}) 
-\] 
-Thus, the meaning of the procedure is the fixpoint of function $F : {\cal R} \to {\cal R}$ given by 
-\[ 
-   F(t) = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!] 
-\] 
-Note that $F$ is monotonic in its argument, because the operators $\circ$, $\cup$ are monotonic: 
-  * $r_1 \subseteq r_2\ \rightarrow\ (r_1 \circ s) \subseteq (r_2 \circ s)$ 
-  * $r_1 \subseteq r_2\ \rightarrow\ (s \circ r_1) \subseteq (s \circ r_2)$ 
-  * $r_1 \subseteq r_2\ \rightarrow\ r_1 \cup s \subseteq r_2 \cup s$ 
-Similarly, the function is $\omega$-continuous (see [[sav08:​Tarski'​s Fixpoint Theorem]]). Thus, it has the least fixpoint, and this fixpoint is given by 
-\[ 
-    r_{move} = \bigcup_{n \ge 0} F^n(\emptyset) 
-\] 
-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 ===== 
- 
-**Example:​** Consider the following example. The idea is that after execution of the procedure even(), the boolean variable wasEven shows whether the initial value of x was even. 
-<​code>​ 
-var x : int 
-var wasEven : bool 
- 
-proc even() { 
-  if (x==0) { 
-    wasEven = true; 
-  } else { 
-    x = x - 1; 
-    odd(); 
-  } 
-} 
-proc odd() { 
-  if (x==0) { 
-    wasEven = false; 
-  } else { 
-    x = x - 1; 
-    even(); 
-  } 
-} 
-</​code>​ 
-We can write the bodies as follows: 
-<​code>​ 
-even() = 
-   ​(assume(x==0);​ wasEven = true) 
-   [] 
-   ​(assume(x!=0);​ x = x - 1; odd()) 
- 
-odd() =  
-   ​(assume(x==0);​ wasEven = false) 
-   [] 
-   ​(assume(x!=0);​ x = x - 1; even()) 
-</​code>​ 
-Now, we turn mutually recursive definition into a simple recursive definition by taking the pair of the meaning of odd and even. We need to find 
-relations $r_{even}$, $r_{odd}$ such that 
-\[ 
-   ​(r_{even},​r_{odd}) = G(r_{even},​r_{odd}) 
-\] 
-where the function $G : {\cal R}^2 \to {\cal R}^2$ is given by: 
-\[ 
-G(E,O) =  
-\begin{array}[t]{@{}l@{}} 
-      \bigg( ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!]) \cup 
-      ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ O)\ , \\ 
-      ([\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) \cup 
-      ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) \bigg) 
-\end{array} 
-\] 
- 
-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) 
-\] 
-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. ​ 
- 
-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\}}$). 
- 
-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)$. 
- 
-=== 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$.