HoareDomainAbstract domains with Hoare ordering.
module HoarePO (E : Lattice.PO) : sig ... endmodule type SetS = sig ... endSet of Lattice.S elements with Hoare ordering. This abstracts a set by its maximal elements.
module Set_LiftTop
(B : Lattice.S)
(N : SetDomain.ToppedSetNames) :
SetS with type elt = B.tmodule MapBot (SpecD : Lattice.S) (R : SetDomain.S) : sig ... end