code:: dfa:: MonotonicInterp
A monotonic abstract interpretation.
Monotonic abstract interpretations impose two additional requirements:
- the abstract state must be a
- the state propagation methods (transfer functions) must all be monotonic with regard to the partial order induced by the lattice: if f is a transfer function and L is the lattice, then a ⊑ b ⇒ f(a) ⊑ f(b) for a, b ∈ L.
Interpretations used with the fixpoint executor are required to be monotonic.