Dijkstra's weakest precondition semantics, as presented in textbook form by Gries, may be viewed as an equational algebra. The problem then is to find a reasonable (set-theoretic ) model of this algebra. This paper provides one.

The refinement calculus, based on weakest preconditions, elaborates imperative program developments as a series of steps linked by a mathematical refinement relation. Specifications and executable code are regarded equally ...