Differences

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

--- sav08:forward_symbolic_execution [2009/03/11 14:35]
vkuncak
+++ sav08:forward_symbolic_execution [2015/04/21 17:30] (current)
@@ Line 18: / Line 18: @@
 Maintain symbolic state formula $R(x_0,y_0,x,y)$ in the following normal form:
-\[
+\begin{equation*}
     x = e_x \land y = e_y \land P
-\]
+\end{equation*}
 where $e_x$ is term describing symbolic state of $x$ and $e_y$ describes symbolic state of $y$.  The remaining part of the formula $R$ is given in //path condition// $P$.  It is a conjunction of all branch conditions up to current program point.  We require $P$ to be expressed only in terms of $x_0,y_0$, not $x,y$.
@@ Line 29: / Line 29: @@
 ++++What should it do when encountering assert(F)?
 |Generate proof obligation
-\[
+\begin{equation*}
     \forall x,y.\ ((\exists x_0,y_0.R(x_0,y_0,x,y)) \rightarrow F(x,y))
-\]
+\end{equation*}
 that is, check the validity of $R \rightarrow F$.
@@ Line 56: / Line 56: @@
 ++++How does this follow from relation composition?|
-\[
+\begin{equation*}
 \{((x0,y0),(x,y)) \mid (x = e_x \land y = e_y \land P)\} \circ \{ ((x,y),(x',y') \mid x' = f(x,y) \land y' = y \}
-\]
+\end{equation*}
-\[
+\begin{equation*}
 \{((x0,y0),(x',y')) \mid \exists x,y. (x = e_x \land y = e_y \land P \land x' = f(x,y) \land y' = y \}
-\]
+\end{equation*}
-\[
+\begin{equation*}
 \{((x0,y0),(x',y')) \mid (x' = f(e_x,e_y) \land y' = e_y \land P \}
-\]
+\end{equation*}
-\[
+\begin{equation*}
 \{((x0,y0),(x,y)) \mid (x = f(e_x,e_y) \land y = e_y \land P \}
-\]
+\end{equation*}
 ++++
@@ Line 90: / Line 90: @@
   assert(F(x,y))
 emit proof obligation:
-\[
+\begin{equation*}
    (x = e_x \land y = e_y \land P) \rightarrow F(e_x,e_y)
-\]
+\end{equation*}
 and change the state:
   x := x_k (fresh)