Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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)$.
 
sav08/collecting_semantics.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice