Non-deterministic expressions and predicate transformers

Non-determinacy is important in the formal specification and formal derivation of programs, but non-determinacy within expressions is theoretically problematical. The refinement calculus side-steps the problem by admitting non-determinacy only at the level of statements, leading to a style of programming that favours statements and procedures over expressions and functions. But expressions are easier to manipulate than statements, and the poverty of the expression notation has made the formal derivation of imperative programs tedious. Here we introduce non-deterministic expressions into the refinement calculus by constructing a weakest precondition semantics for imperative specifications and programs that holds good even when expressions may be non-deterministic.