LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav08:collecting_semantics [2008/05/07 23:25]
giuliano 		sav08:collecting_semantics [2008/05/08 12:37]
vkuncak
Line 27: Line 27:
 \] \]
 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
 +\[
 +  \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)
 +\]
  
 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)$.