Abstract
We introduce datatype specifications based on schemes, a slight generalization of first order specifications. For a schematic specification (Σ, \(\mathbb{E}\)), Hoare's Logic HL (Σ, \(\mathbb{E}\)) for partial correctness is defined as usual and on top of it a proof system (Σ, \(\mathbb{E}\)) ⊢ p → S ↓ for termination assertions is defined. The system is first order in nature, but we prove it sound and complete w.r.t. a second order semantics. We provide a translation of a standard proof system HLT(A) for total correctness on a structure A into our format.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
APT, K.R. & E.R. OLDEROG, Proof rules dealing with fairness, Bericht Nr. 8104, March 1981, Institut für Informatik und Praktische Mathematik, Christian Albrechts-universität Kiel.
BERGSTRA, J.A. & J.W. KLOP, Proving program inclusion using Hoare's Logic, Mathematical Centre, Department of Computer Science, Research Report IW 176, Amsterdam 1981.
BERGSTRA, J.A. & J.W. KLOP, A formalized proof system for total correctness of while programs, Mathematical Centre, Department of Computer Science, Research Report IW 175, Amsterdam 1981.
BERGSTRA, J.A. & J.V. TUCKER, Hoare's Logic and Peano's Arithmetic, Mathematical Centre, Department of Computer Science, Research Report IW 160, Amsterdam 1981.
BERGSTRA, J.A. & J.V. TUCKER, The axiomatic semantics of while programs using Hoare's Logic, manuscript May 1981, definitive version in preparation.
GRÜMBERG O., N. FRANCEZ, J.A. MAKOWSKY & W.P. DE ROEVER, A Proof Rule for fair Termination of Guarded Commands, Report RUU-CS-81-2, Vakgroep Informatica Utrecht.
HAREL, D., First Order Dynamic Logic, Springer Lecture Notes in Comp. Sc. 68, 1979.
HAREL, D., Proving the correctness of regular deterministic programs: a unifying survey using dynamic Logic, T.C.S. 12(1) 61–83.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bergstra, J.A., Klop, J.W. (1982). A formalized proof system for total correctness of while programs. In: Dezani-Ciancaglini, M., Montanari, U. (eds) International Symposium on Programming. Programming 1982. Lecture Notes in Computer Science, vol 137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11494-7_3
Download citation
DOI: https://doi.org/10.1007/3-540-11494-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11494-9
Online ISBN: 978-3-540-39184-5
eBook Packages: Springer Book Archive