# Collecting Semantics

## Transitive Closure as Least Fixedpoint

Recall the definition of transitive closure for a binary relation

where .

Lemma: Reflexive transitive closure is the least relation for which , where is given by .

(We call for which the fixpoint (or fixed point) of .)

Note that is monotonic: if then .

## Reachable States and Collecting Semantics

Question we wish to answer: What are the sets of reachable states at each program point?

We represent programs by control-flow graphs (CFG).

Program points are CFG nodes, denoted by . Statements are labels on CFG edges.

We look at a particular way of representing and computing sets of reachable states, splitting states by program counter (control-flow graph node): collecting semantics.

- the set of 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 .

Let

The set of reachable states is defined as the least solution of constraints

where is command associated with edge , and is the relation giving semantics for this command.

By least we mean least with respect to the following ordering on functions from control-flow graph points to sets: iff .

Lemma: Let be a least solution of the collecting semantics constraints. Then iff: there exists and there exists a finite path through CFG that starts in with state and ends in with state .

Proof: Consider the following given by collecting all states for which there exists such a path terminating at point in state . We show that is the least solution of the constraints.

We first show that it is a solution. It satisfies equation . For the second equation, if we take element then it is given by some path of length terminating at node . Then the elements in are given by a path of length terminating at . Therefore, these elements are in . Thus, for all , we have

so the constraint is satisfied and is a solution.

Next, we show that is the least solution. Consider any solution . We then show for all . We show that all states given by paths (i.e. all states in ) are included in , by induction on the lengths of paths. Paths of length 0 are included by . The second condition guarantees that if all paths of length are included, then all paths of length are included.

Thus, we have shown that is the least solution, so the lemma follows by definition of .

End of Proof.

## Equivalent Form of the Constraints

Using the fact that the conjunction of constraints and is equivalent to

the above constraints for collecting semantics are equivalent to: