Module type Monotone_framework_sigs.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).