Run.G
type variable = M.key
The type of variables, or graph vertices.
type property = P.property
The type of properties.
foreach_root
describes the root nodes of the data flow graph as well as the properties associated with them. foreach_root contribute
must call contribute x p
to indicate that x
is a root and that p
is a lower bound on the solution at x
. It may call contribute x _
several times at a single root x
.
foreach_successor
describes the edges of the data flow graph as well as the manner in which a property at the source of an edge is transformed into a property at the target. The property at the target must of course be a monotonic function of the property at the source. Furthermore, if the property at the source is bottom
then the property that is transmitted to each target should be bottom
as well.