Abstract
In this paper we define a categorical interpretation of the first-order Hoare logic of a small programming language, by giving a weakest precondition semantics for the language. To this end, we extend the well-known notion of (first-order) hyperdoctrine to include partial maps. The most important new aspect of the resulting partial (first order) hyperdoctrine is a different notion of morphism between the fibers. We also use this partial hyperdoctrine to give a model for Beeson's Partial Function Logic such that (a version of) his axiomatization is complete w.r.t. this model. This shows the usefulness of the notion independent of its intended use as a model for Hoare logic. Further new results of the paper include a formulation of intuitionistic Hoare logic, and Hoare logic with partial functions.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K.R. Apt. Ten years of Hoare's logic. ACM Trans. on Prog. Lan. and Syst., 3:431–483, 1981.
M.J. Beeson. Proving programs and programming proofs. In B. Marcus et al., editor, Logic, Methodology and Philosophy of Science VII. Elsevier, 1986.
P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier, 1990. Vol. B.
J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88:205–232, 1980.
C.A.R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576–580, 1969.
F.W. Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In A. Heller, editor, Proc. New York Symp. on Applications of Categorical Algebra, pages 1–14. Amer. Math. Soc., 1970.
A.M. Pitts. Notes on categorical logic. Technical report, Computer Laboratory, Univ. of Cambridge, 1989.
G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, Univ. of Oxford, 1986.
E. Robinson and G. Rosolini. Categories of partial maps. Information and Computation, 79:95–130, 1988.
D.S. Scott. Identity and existence in intuitionistic logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, Applications of Sheaves, 1979.
R.D. Tennent. A note on undefined expression values in programming logics. Inf. Proc. Letters, 24:331–333, 1987.
D. van Dalen and A.S. Troelstra. Constructivism in Mathematics, volume I. North Holland, 1988.
E.G Wagner. A categorical treatment of pre-and post-conditions. Theor. Comp. Sc., 53:3–24, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Knijnenburg, P.M.W., Nordemann, F. (1992). A categorical interpretation of partial function logic and Hoare logic. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023877
Download citation
DOI: https://doi.org/10.1007/BFb0023877
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55707-4
Online ISBN: 978-3-540-47276-6
eBook Packages: Springer Book Archive