Lab for Automated Reasoning and Analysis 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] (current)
Line 4: Line 4:
  
 In [[Relational Semantics]] for a language without procedures we had semantic function that maps programs to relations In [[Relational Semantics]] for a language without procedures we had semantic function that maps programs to relations
-\[+\begin{equation*}
    r_c : C \to {\cal R}    r_c : C \to {\cal R}
-\]+\end{equation*}
 so $r_c(c_1)$ was the relation corresponding to the command $c_1$, and we denote it by $[\![c_1]\!]$. so $r_c(c_1)$ was the relation corresponding to the command $c_1$, and we denote it by $[\![c_1]\!]$.
  
Line 41: Line 41:
 </​code>​ </​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: 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:
-\[+\begin{equation*}
    ​r_{move} = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!]    ​r_{move} = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!]
-\]+\end{equation*}
 Denoting the right-hand side by $F(r_{move})$,​ we can write the above as Denoting the right-hand side by $F(r_{move})$,​ we can write the above as
-\[+\begin{equation*}
    ​r_{move} = F(r_{move})    ​r_{move} = F(r_{move})
-\]+\end{equation*}
 Thus, the meaning of the procedure is the fixpoint of function $F : {\cal R} \to {\cal R}$ given by Thus, the meaning of the procedure is the fixpoint of function $F : {\cal R} \to {\cal R}$ given by
-\[+\begin{equation*}
    F(t) = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!]    F(t) = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!]
-\]+\end{equation*}
 Note that $F$ is monotonic in its argument, because the operators $\circ$, $\cup$ are monotonic: 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\ (r_1 \circ s) \subseteq (r_2 \circ s)$
Line 57: Line 57:
   * $r_1 \subseteq r_2\ \rightarrow\ r_1 \cup s \subseteq r_2 \cup s$   * $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 Similarly, the function is $\omega$-continuous (see [[sav08:​Tarski'​s Fixpoint Theorem]]). Thus, it has the least fixpoint, and this fixpoint is given by
-\[+\begin{equation*}
     r_{move} = \bigcup_{n \ge 0} F^n(\emptyset)     r_{move} = \bigcup_{n \ge 0} F^n(\emptyset)
-\]+\end{equation*}
 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 In this example, we have
-\[+\begin{equation*}
    ​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) \}    ​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) \}
-\]+\end{equation*}
  
 ===== Multiple Mutually Recursive Procedures ===== ===== Multiple Mutually Recursive Procedures =====
Line 106: Line 106:
 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 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 relations $r_{even}$, $r_{odd}$ such that
-\[+\begin{equation*}
    ​(r_{even},​r_{odd}) = G(r_{even},​r_{odd})    ​(r_{even},​r_{odd}) = G(r_{even},​r_{odd})
-\]+\end{equation*}
 where the function $G : {\cal R}^2 \to {\cal R}^2$ is given by: where the function $G : {\cal R}^2 \to {\cal R}^2$ is given by:
-\[+\begin{equation*}
 G(E,O) =  G(E,O) = 
 \begin{array}[t]{@{}l@{}} \begin{array}[t]{@{}l@{}}
Line 118: Line 118:
       ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) \bigg)       ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) \bigg)
 \end{array} \end{array}
-\]+\end{equation*}
  
 We define lattice structure on ${\cal R}^2$ by  We define lattice structure on ${\cal R}^2$ by 
-\[+\begin{equation*}
    ​(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)
-\] +\end{equation*} 
-\[+\begin{equation*}
    ​(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)
-\]+\end{equation*}
 Note that: Note that:
-\[+\begin{equation*}
    ​G(\emptyset,​\emptyset) = ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!],​ [\![assume(x==0)]\!] \circ [\![wasEven=false]\!])    ​G(\emptyset,​\emptyset) = ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!],​ [\![assume(x==0)]\!] \circ [\![wasEven=false]\!])
-\] +\end{equation*} 
-\[+\begin{equation*}
    ​G(G(\emptyset,​\emptyset)) =    ​G(G(\emptyset,​\emptyset)) =
 \begin{array}[t]{@{}l@{}} \begin{array}[t]{@{}l@{}}
Line 139: Line 139:
       ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,​\emptyset).\_1) \bigg)       ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,​\emptyset).\_1) \bigg)
 \end{array} \end{array}
-\]+\end{equation*}
 where $p.\_1$ and $p.\_2$ denote first, respectively,​ second, element of the pair $p$. where $p.\_1$ and $p.\_2$ denote first, respectively,​ second, element of the pair $p$.
  
Line 151: Line 151:
  
 In the example above, we can prove that In the example above, we can prove that
-\[+\begin{equation*}
    ​r_{even} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land    ​r_{even} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land
-     ​(wasEven'​ \leftrightarrow (x \pmod 2 = 0)) +     ​(wasEven'​ \leftrightarrow ​((x \mod 2= 0)) 
-\] +\end{equation*} 
-\[+\begin{equation*}
    ​r_{odd} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land    ​r_{odd} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land
-     ​(wasEven'​ \leftrightarrow (x \pmod 2 \ne 0)) +     ​(wasEven'​ \leftrightarrow ​((x \mod 2\ne 0)) 
-\]+\end{equation*}
  
 === Remark ===  === Remark === 
 
sav08/relational_semantics_of_procedures.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice