This is an old revision of the document!
Describing Reachable States using Collecting Semantics
Main question: What values can variables of the program take at different program points?
We can represent programs by control-flow graphs (CFG).
Definition: Control flow-graph is a graph with nodes , edges and for each edge a command , with initial and final node
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.
- states describing values of program variables (not including program counter).
For each program point , we have the set of reachable states .
The set of all reachable states of the program is .
Let be initial program counter and the set of values of program variables in .
The set of reachable states is defined as the least solution of constraints: \[
I \subseteq C(p_0)
\] \[
\bigwedge_{(p_1,p_2) \in E} sp(C(p_1),r(c(p_1,p_2)))) \subseteq C(p_2)
\] where is command associated with edge , and is the relation giving semantics for this command.
Set of recursive inequations in the lattice of products of sets. Note is equivalent to , so we have equations in lattice.
Example
Sets of states at selected points:
i = 20; x = 2; while (i > 0) { x = x + 4; i = i - 1; } if (x==0) { error; } else { y = 1000/x; }