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:review_of_fixpoints_in_semantics [2008/04/30 11:03]
vkuncak
sav08:review_of_fixpoints_in_semantics [2008/05/07 22:58]
giuliano
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 77: Line 77:
   \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)
 \] \]
-where $c(p_1,​p_2)$ is command associated with edge $(p_1,​p_2)$,​ $r(c(p_1,​p_2))$ is relation 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.