Make.2-P
The type property
must form a partial order, and must be equipped with a least element bottom
and with an equality test equal
. The partial order must satisfy the ascending chain condition: every monotone sequence must eventually stabilize.
We do not require an ordering test leq
or a join operation join
.
equal p q
determines whether the properties p
and q
are equal. In the implementation of this test, it is permitted to assume that p <= q
holds.
val is_maximal : property -> bool
is_maximal p
determines whether the property p
is maximal with respect to the partial order. A conservative check suffices: it is always permitted for is_maximal p
to be false
. If is_maximal p
is true
, then p
must have no strict upper bound. In particular, if properties form a lattice, then is_maximal p = true
implies that p
is the top element of the lattice.