Module type Sig.JOIN_SEMI_LATTICE

A JOIN_SEMI_LATTICE is the minimal structure needed for abstract interpretation. It represents a mathematical join semi-lattice: i.e. a set (type t) with an inclusion order (includes : t -> t -> bool) that orders those values. The key operation is join : t -> t -> t, which merges information from two elements to form their least upper bound (an over-approximation of both).

In program analysis, join is used at control-flow merge points, e.g., after an if or while, to unify information from different paths.

The widen operator ensures convergence when computing fixpoints in loops, by accelerating growth of abstract states.

This minimal signature doesn't require meet or top operations.

include Datatype_sig.S
type t
val equal : t -> t -> bool

Any notion of equality is allowed, as long as it is an equivalence relation, and that if a == b, then equal a b.

val compare : t -> t -> int

compare is a total order, and should be compatible with equal.

val hash : t -> int

hash requires that equal values have the same hash.

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

Computes the least upper bound of two elements.

val includes_or_widen : previous:t -> t -> bool * t

In a fixpoint iteration of a function \mathcal{F}, previous is the previous element of the fixpoint iteration sequence. The other element is the newly computed (tentative) element, i.e. \mathcal{F}(previous). If the new element is included in previous, true is returned, together with new (the smaller element): the post-fixpoint of \mathcal{F} has been found (further calls to \mathcal{F} can decrease the sequence). Else, the returned element should be used as the next element of the fixpoint iteration sequence; the operator guarantees its convergence. For lattices of finite height, the widening part can just perform an over-approximation of the join; however note that it is not required that the sequence is monotonic.

val includes : t -> t -> bool

includes a b holds if b \sqsubseteq a, i.e., b is at least as precise as a.

val widen : previous:t -> t -> t

Widening operator used in fixpoint iteration to enforce convergence.