Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Next revision Both sides next revision | ||
sav08:collecting_semantics [2008/05/07 00:57] vkuncak created |
sav08:collecting_semantics [2008/05/07 01:09] 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 27: | Line 27: | ||
\] | \] | ||
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** | ||
+ | |||
+ | <code> | ||
+ | i = 20; | ||
+ | x = 2; | ||
+ | while (i > 0) { | ||
+ | x = x + 4; | ||
+ | i = i - 1; | ||
+ | } | ||
+ | if (x==0) { | ||
+ | error; | ||
+ | } else { | ||
+ | y = 1000/x; | ||
+ | } | ||
+ | </code> | ||