Differences
This shows you the differences between two versions of the page.
| Next revision Both sides next revision | |||
|
sav08:collecting_semantics [2008/05/07 00:57] vkuncak created |
sav08:collecting_semantics [2008/05/07 01:00] vkuncak |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| 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, splitting states by program counter (control-flow graph node): **collecting semantics**. | ||
| - | $PS$ - the set of values of program variables (not including program counter). | + | $PS$ - states describing values of program variables (not including program counter). |
| For each program point $p$, we have the set of reachable states $C(p) \subseteq PS$. | For each program point $p$, we have the set of reachable states $C(p) \subseteq PS$. | ||
| Line 28: | Line 28: | ||
| 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. | 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. | ||
| + | |||
| + | **Example** | ||