Transition System and Collecting Semantics
- program counter values. Denoted (program point) or (vertex in CFG)
- values of other variables
Transition system semantics:
- state is set of pairs
- element of concrete lattice is a set of such pairs , i.e.
- post maps set of such pairs to an extended set of such pairs,
Because is an arbitrary set, for a given , there can be any number of such that is in (in fact, is a relation on ).
We can equivalently represent this relation as the following multi-valued function, by grouping all for a given :
Collecting semantics simply works with instead of , which is just notational change.
- lattice element is a function i.e.
- we have function that transforms such functions and directly corresponds to
Control-flow graph: where
- is set of program points
- are control-flow graph edges
- , so each is relation describing the meaning of command between and
Compute the big relation on global states in terms of and .
Then derive a nice expression for where .
Now we come back to the definition of post, which was
so we obtain
Now instead of , consider , and define a new sp on such different representation. Then
We also represent as , then we obtain function that corresponds to :
Note that will be except at the entry into our control-flow graph.
If we compute , we obtain such that gives precisely the set of all reachable states at a program point . Such is isomorphic to .
We call this way of defining the collecting semantics of the program, because it collects all states for each program point. It will be convenient to define how abstract interpretation works.