ForOrderedType.3-G
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.