Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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