• English only

# Differences

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

sav08:review_of_fixpoints_in_semantics [2008/04/30 11:05]
vkuncak
sav08:review_of_fixpoints_in_semantics [2015/04/21 17:30] (current)
Line 4: Line 4:

Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation
-$+\begin{equation*} r^* = \bigcup_{n \ge 0} r^n r^* = \bigcup_{n \ge 0} r^n -$+\end{equation*}
where $r^0 = \Delta_D$. where $r^0 = \Delta_D$.

Line 23: Line 23:

This can be written as  This can be written as
-$+\begin{equation*} p = F(p) p = F(p) -$+\end{equation*}
where  where
F(p) = if (c) then (s;p) else skip   F(p) = if (c) then (s;p) else skip
Line 35: Line 35:

If $r_s$ is meaning of $s$ and $\Delta_c$ is meaning of //assume( c )//, the meaning is the fixpoint of function If $r_s$ is meaning of $s$ and $\Delta_c$ is meaning of //assume( c )//, the meaning is the fixpoint of function
-$+\begin{equation*} f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c} f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c} -$+\end{equation*}

Any program can be reduced to a loop: Any program can be reduced to a loop:
Line 60: Line 60:
Program points are CFG nodes. ​ Statements are labels on CFG edges. Program points are CFG nodes. ​ Statements are labels on CFG edges.

-We look at a particular way of representing and computing sets of reachable, splitting states by program counter (control-flow graph node): **collecting semantics**.+We look at a particular way of representing and computing sets of reachable ​states, splitting states by program counter (control-flow graph node): **collecting semantics**.

$PS$ - the set of values of program variables (not including program counter). $PS$ - the set of values of program variables (not including program counter).
Line 71: Line 71:

The set of reachable states is defined as the least solution of constraints:​ The set of reachable states is defined as the least solution of constraints:​
-$+\begin{equation*} I \subseteq C(p_0) I \subseteq C(p_0) -$ +\end{equation*}
-$+\begin{equation*} \bigwedge_{(p_1,​p_2) \in E} sp(C(p),​r(c(p_1,​p_2)))) \subseteq C(p_2) \bigwedge_{(p_1,​p_2) \in E} sp(C(p),​r(c(p_1,​p_2)))) \subseteq C(p_2) -$+\end{equation*}
where $c(p_1,​p_2)$ is command associated with edge $(p_1,​p_2)$,​ and $r(c(p_1,​p_2))$ is the relation giving semantics for this command. where $c(p_1,​p_2)$ is command associated with edge $(p_1,​p_2)$,​ and $r(c(p_1,​p_2))$ is the relation giving semantics for this command.