• English only

# Differences

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

 sav08:collecting_semantics [2008/05/08 12:36]vkuncak sav08:collecting_semantics [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/05/08 12:37 vkuncak 2008/05/08 12:36 vkuncak 2008/05/08 12:36 vkuncak 2008/05/08 12:36 vkuncak 2008/05/07 23:25 giuliano 2008/05/07 08:10 vkuncak 2008/05/07 08:08 vkuncak 2008/05/07 07:56 vkuncak 2008/05/07 01:24 vkuncak 2008/05/07 01:10 vkuncak 2008/05/07 01:09 vkuncak 2008/05/07 01:00 vkuncak 2008/05/07 00:57 vkuncak created Next revision Previous revision 2008/05/08 12:37 vkuncak 2008/05/08 12:36 vkuncak 2008/05/08 12:36 vkuncak 2008/05/08 12:36 vkuncak 2008/05/07 23:25 giuliano 2008/05/07 08:10 vkuncak 2008/05/07 08:08 vkuncak 2008/05/07 07:56 vkuncak 2008/05/07 01:24 vkuncak 2008/05/07 01:10 vkuncak 2008/05/07 01:09 vkuncak 2008/05/07 01:00 vkuncak 2008/05/07 00:57 vkuncak created Line 20: Line 20: 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_1),​r(p_1,​p_2))) \subseteq C(p_2) \bigwedge_{(p_1,​p_2) \in E} sp(C(p_1),​r(p_1,​p_2))) \subseteq C(p_2) -$ + \end{equation*} over variables $C(p)$ for all of finitely many program points $p$. over variables $C(p)$ for all of finitely many program points $p$. The last condition is equivalent to The last condition is equivalent to - $+ \begin{equation*} - \bigwedge_{p_2 \in V}\ \left( C(p_2) = C(p_2) \bigcup_{(p_1,​p_2) \in E} sp(C(p_1),​r(p_1,​p_2))) \right) + \bigwedge_{p_2 \in V}\ \left( C(p_2) = C(p_2) ​\cup \bigcup_{(p_1,​p_2) \in E} sp(C(p_1),​r(p_1,​p_2))) \right) -$ + \end{equation*} Here $r(p_1,​p_2)$ is the relation giving semantics for the command associated with edge $(p_1,​p_2)$. Here $r(p_1,​p_2)$ is the relation giving semantics for the command associated with edge $(p_1,​p_2)$.