Transitive Closure as Least Fixedpoint
Recall the definition of transitive closure for a binary relation
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 .
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: