Module type Dataflows.JOIN_SEMILATTICE

module type JOIN_SEMILATTICE = sig .. end

type t 

val join : t ->
       t -> t

Must be idempotent (join a a = a), commutative, and associative.

val bottom : t

Must verify that forall a, join a bottom = a.

val join_and_is_included : t ->
       t -> t * bool

This function is used by the dataflow algorithm to determine if something has to be recomputed. Joining and inclusion testing are similar operations, so it is often more efficient to do both at the same time (e.g. when joining with bottom). Note that the names smaller and larger are actually correct only if there is an inclusion.

Instead of defining it directly, it can be defined from join and equal, or from is_included, for instance by if is_included new old then (true,old) else (false, join old new) or let j = join old new in (equal j new, j).

val pretty : Format.formatter -> t -> unit

Display the contents of an element of the lattice.