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 Both sides next revision
sav08:collecting_semantics [2008/05/07 08:10]
vkuncak
sav08:collecting_semantics [2008/05/07 23:25]
giuliano
Line 9: Line 9:
 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$ - states describing values of program variables (not including program counter). $PS$ - states describing values of program variables (not including program counter).
Line 53: Line 53:
 } }
 </​code>​ </​code>​
 +After the assignment of $x$ to 2, the set of reachable states $C$ is $C = \{ (x,2), (i,20), (y,t) \}$