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.
Preview
Unable to display preview. Download preview PDF.
4. Bibliography
Dijkstra, E. W., A Discipline of Programming. Prentice Hall, Englewood Cliffs, 1978.
Gries, D. The Science of Programming. Springer-Verlag, New York, Heidelberg, Berlin, 1981.
Herrlich, H., and Strecker, G. E., Category Theory, Allyn and Bacon, Boston, 1973.
Plotkin, G.D., "Dijkstra's Predicate Transformers and Smyth's Powerdomains," Abstract Software Specifications, Proceedings of the 1979 Copenhagen Winter School, LNCS 86 (Edited by D. Bjorner) 527–553.
Smyth, M.B., "Power Domains and Predicate Transformers: a topological view," Proceedings of ICALP'83 (Barcelona), LNCS 154, pp 662–675.
Manes, E., Talk at the Workshop on Category Theory and Computer Programming, University of Surrey, Guildford, England, Sept 1985. (Manuscript in preparation)
Reynolds, J.C., The Craft of Programming, Prentice-Hall International (1981).
Hoare, C.A.R., "An Axiomatic Basis for Computer Programming," Comm. ACM 12 (October 1969) 576–580 and 583.
Jones, C.B., Software Development: A Rigorous Approach," Prentice-Hall International (1980).
Gierz, G, Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., and Scott, D., A compendium of Continuous Lattices, Springer-Verlag, 1980.
Wagner, E.G. "An Algebraic Approach to Pre-conditions, Post-Conditions, and Predicate Transformers," to appear.
MacLane, S., Categories for the Working Mathematician, Springer-Verlag, New York, 1971.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Wagner, E.G. (1986). A categorical view of weakest liberal preconditions. In: Pitt, D., Abramsky, S., Poigné, A., Rydeheard, D. (eds) Category Theory and Computer Programming. Lecture Notes in Computer Science, vol 240. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17162-2_123
Download citation
DOI: https://doi.org/10.1007/3-540-17162-2_123
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17162-1
Online ISBN: 978-3-540-47213-1
eBook Packages: Springer Book Archive