# 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,

## Collecting Semantics

Take .

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

where

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.