Module type Monotone_framework_sigs.LATTICE

The API for a complete (possibly non-distributive) lattice, needed for the mfp algorithm in the monotone framework

include LATTICE_NO_BOT
type properties
val leq : properties -> properties -> bool
val initial : properties

An initial value, which might not be the top element. The idea is that this is the property that you start with (you assume to be true at the start of your analysis).

val bottom : properties