Interpreting Nondeterminism in the Refinement Calculus

We introduce a simple programming language and define its predicate transformer semantics. We motivate the choice of the constructs for the language by algebraic arguments, showing that the constructs are essentially the basic algebraic operations that are available for predicate transformers, when these are viewed as forming a complete lattice enriched category. We then show that the statements in the language can be given a simple operational interpretation, as describing the interaction between a user and a computing system. This gives a general intuitive interpretation of angelic and demonic nondeterminism. We also consider the notion of correctness and refinement of program statements that this intuitive interpretation gives rise to, and show the connection between the user-system interpretation and the interpretation of program execution as a game.