Abstract
This paper presents sound and complete Hoare logics for partial and total correctness of recursive parameterless procedures in the context of unbounded nondeterminism. For total correctness, the literature so far has either restricted recursive procedures to be deterministic or has studied unbounded nondeterminism only in conjunction with loops rather than procedures. We consider both single procedures and systems of mutually recursive procedures. All proofs have been checked with the theorem prover Isabelle/HOL.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Pierre America and Frank de Boer. Proving total correctness of recursive procedures. Information and Computation, 84:129–162, 1990.
Krzysztof Apt. Ten Years of Hoare’s Logic: A Survey — Part I. ACM Trans. Programming Languages and Systems, 3(4):431–483, 1981.
Krzysztof Apt. Ten Years of Hoare’s Logic: A Survey — Part II: Nondeterminism. Theoretical Computer Science, 28:83–109, 1984.
Krzysztof Apt and Gordon Plotkin. Countable nondeterminism and random assignment. Journal of the ACM, 33:724–767, 1986.
Robert Cartwright and Derek Oppen. The logic of aliasing. Acta Informatica, 15:365–384, 1981.
Gerald Arthur Gorelick. A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report 75, Dept. of Computer Science, Univ. of Toronto, 1975.
Peter Hitchcock and David Park. Induction rules and termination proofs. In M. Nivat, editor, Automata, languages, and programming, pages 225–251. North-Holland, 1973.
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:567–580,583, 1969.
C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In E. En-geler, editor, Semantics of algorithmic languages, volume 188 of Lecture Notes in Mathematics, pages 102–116. Springer-Verlag, 1971.
Martin Hofmann. Semantik und Verifikation. Lecture notes, Universität Marburg. In German, 1997.
Peter V. Homeier and David F. Martin. Mechanical verification of mutually recursive procedures. In M. A. McRobbie and J. K. Slaney, editors, Automated Deduction — CADE-13, volume 1104 of Lect. Notes in Comp. Sci., pages 201–215. Springer-Verlag, 1996.
Peter V. Homeier and David F. Martin. Mechanical verification of total correctness through diversion verification conditions. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics (TPHOLs’98), volume 1479 of Lect. Notes in Comp. Sci., pages 189–206. Springer-Verlag, 1998.
Thomas Kleymann. Hoare logic and auxiliary variables. Formal Aspects of Computing, 11:541–566, 1999.
J. H. Morris. Comments on “procedures and parameters”. Undated and unpublished.
David Naumann. Calculating sharp adaptation rules. Information Processing Letters, 77:201–208, 2000.
Hanne Riis Nielson and Flemming Nielson. Semantics with Applications. Wiley, 1992.
Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of Lect. Notes in Comp. Sci., pages 180–192. Springer-Verlag, 1996.
Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171–186, 1998.
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL —A Proof Assistant for Higher-Order Logic, volume 2283 of Lect. Notes in Comp. Sci. Springer-Verlag, 2002.
David von Oheimb. Hoare logic for mutual recursion and local variables. In C. Pandu Rangan, V. Raman, and R. Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science (FST&TCS), volume 1738 of Lect. Notes in Comp. Sci., pages 168–180. Springer-Verlag, 1999.
Ernst-Rüdiger Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science, 24:337–347, 1983.
P. Pandya and M. Joseph. A structure-directed total correctness proof rule for recursive procedure calls. The Computer Journal, 29:531–537, 1986.
Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.
Thomas Schreiber. Auxiliary variables and recursive procedures. In TAP-SOFT’97: Theory and Practice of Software Development, volume 1214 of Lect. Notes in Comp. Sci., pages 697–711. Springer-Verlag, 1997.
Stefan Sokołowski. Total correctness for procedures. In Mathematical Foundations of Computer Science (MFCS), volume 53 of Lect. Notes in Comp. Sci., pages 475–483. Springer-Verlag, 1977.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nipkow, T. (2002). Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_8
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive