Finite-cofinite program relations
Chris Brink · Logic Journal of IGPL · 1999
This paper expands the notion of finite nondeterminism by allowing also cofinite nondeterminism. We characterise a class of programs (via their input-output relations) and a class of predicates, such that each predicate is either finite or cofinite, and programs, when viewed as predicate transformers, preserve this distinction. So as not to be too closely tied to the specifics of any semantic approach, we require our relational model of programs to be translatable also into a predicate transformer model, as well as a Hoare-logical model, by considerations of duality. This make for a well-behaved class of programs and predicates, albeit fairly restricted. One advantage of this approach is that we need not equate either nontermination or non-finite nondeterminism with chaos. Key words: Hoare logic, predicate transformer semantics, predicate relator semantics, relational model, weakest precondition, Boolean algebra, Jónsson/Tarski duality.