Abstract

This paper expands the notion of finite nondeterminism by allowing also cofinite nondeterminism. We characterise a class of programs 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