• 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)
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)$.