Fixpoints for general correctness

AbstractWe investigate various fixpoint operators in a semiring-based setting that models a general correctness semantics of programs. They arise as combinations of least/greatest (pre/post)fixpoints with respect to refinement/approximation. In particular, we show isotony of these operators and give representations of fixpoints in terms of other fixpoints. Some results require completeness of the Egli–Milner order, for which we provide conditions.A new perspective is reached by exchanging the semirings with distributive lattices. They can be augmented in a natural way with a second order that is similar to the Egli–Milner order.We extend our discussion of fixpoint operators to this induced order. We show the impact on general correctness by connecting the lattice- and the semiring-based treatments to obtain results about the Egli–Milner order