A categorical view of weakest liberal preconditions

Abstract

In this paper we reformulate the concepts of liberal pre- and post-conditions, and weakest liberal preconditions in a general categorical setting. We employ this setting to re-examine weakest liberal precondition semantics, and provide a new interpretation which is sounder mathematically and, we claim, more in line with what is really needed in program specification. We begin by replacing predicates by equalizers. Weakest liberal preconditions are then easily formulated in terms of pull backs. We then examine Dijkstra's use of predicate transformers and weakest liberal preconditions to provide semantics for various program constructs. Dijkstra's contention that predicate transformers define relations and that the semantics is thereby non-deterministic, does not carry over to the general setting. However, it is easily seen to be intuitively natural, in the general setting, to regard predicate transformers as defining sets of morphisms. A precise formulation of this idea shows that it is mathematically natural. We give two constructions: one, Fns, taking predicate transformers to sets of morphisms; and the other, Spc taking sets of morphisms to predicate transformers The naturality is shown by a proof that these constructions form a Galois connection (i.e., viewed as functors between the appropriate posets viewed as categories, they form an adjoint situation). These constructions can be carried out in any well-powered category with small limits.