• 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) Both sides previous revision Previous revision 2008/05/07 22:58 giuliano 2008/04/30 11:05 vkuncak 2008/04/30 11:03 vkuncak 2008/04/30 10:54 vkuncak 2008/04/30 10:47 vkuncak 2008/04/30 10:43 vkuncak 2008/04/30 10:34 vkuncak 2008/04/30 10:18 vkuncak 2008/04/30 10:17 vkuncak 2008/04/29 23:24 vkuncak 2008/04/29 23:18 vkuncak 2008/04/29 23:05 vkuncak 2008/04/29 23:03 vkuncak 2008/04/28 16:10 vkuncak 2008/04/28 15:39 vkuncak 2008/04/28 14:52 vkuncak 2008/04/28 14:43 vkuncak 2008/04/28 14:41 vkuncak 2008/04/28 14:23 vkuncak 2008/04/28 14:21 vkuncak 2008/04/28 14:20 vkuncak 2008/04/28 14:19 vkuncak created Next revision Previous revision 2008/05/07 22:58 giuliano 2008/04/30 11:05 vkuncak 2008/04/30 11:03 vkuncak 2008/04/30 10:54 vkuncak 2008/04/30 10:47 vkuncak 2008/04/30 10:43 vkuncak 2008/04/30 10:34 vkuncak 2008/04/30 10:18 vkuncak 2008/04/30 10:17 vkuncak 2008/04/29 23:24 vkuncak 2008/04/29 23:18 vkuncak 2008/04/29 23:05 vkuncak 2008/04/29 23:03 vkuncak 2008/04/28 16:10 vkuncak 2008/04/28 15:39 vkuncak 2008/04/28 14:52 vkuncak 2008/04/28 14:43 vkuncak 2008/04/28 14:41 vkuncak 2008/04/28 14:23 vkuncak 2008/04/28 14:21 vkuncak 2008/04/28 14:20 vkuncak 2008/04/28 14:19 vkuncak created 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.