Parameter Make.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.

bottom is the least property.

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.

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.