Abstract
Much research in axiomatic semantics suffers from a lack of formality. In particular, most proposed verification calculi for imperative programs dealing with recursive procedures are known to be unsound or incomplete. Focussing on total correctness, we present a new consequence rule which yields a sound and complete Hoare-style calculus in the presence of parameterless recursive procedures. Both, the standard consequence and an improved rule of adaptation are instances of our new rule. This work has been developed under the auspices of the computer-aided proof system Lego. The rigorous treatment of auxiliary variables has been crucial for establishing our results. A comparison with VDM reinforces our view that auxiliary variables deserve to be treated seriously.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Peter Aczel. A system of proof rules for the correctness of iterative programs — some notational and organisational suggestions. Unpublished, August 1982.
Pierre America and Frank de Boer. Proving total correctness of recursive procedures. Information and Computation, 84(2): 129–162, 1990.
Krzysztof R. Apt. Ten years of Hoare's logic: A survey — part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, October 1981.
Krzysztof R. Apt and Lambert G. L. T. Meertens. Completeness with finite systems of intermediate assertions for recursive program schemes. SIAM Journal on Computing, 9(4):665–671, November 1980.
Stephen A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1):70–90, February 1978.
P. Cousot. Methods and logics for proving programs. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 15, pages 841–993. Elsevier, 1990.
Ole-Johan Dahl. Verifiable Programming. International Series in Computer Science. Prentice Hall, 1992.
R.W, Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Proc. Symp. in Applied Mathematics, volume 19, pages 19–32, 1967.
Michael J.C. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwhistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving (Banff, Alberta), number 15 in Workshops in Computing, pages 387–439. Springer, 1991.
David Gries. The Science of Computer Programming, chapter 16, pages 193–215. Springer, 1981.
D. Harel. First-order Dynamic Logic, volume 68 of Lecture Notes in Computer Science. Springer, 1979.
C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576–580, 1969. Also in [14].
C.A.R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pages 102–116. Springer, 1971. Also in [14].
C.A.R. Hoare and Cliff B. Jones, editors. Essays in Computing Science. International Series in Computer Science. Prentice Hall, 1989.
Cliff B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, 2 edition, 1990.
The Lego World Wide Web page. http://www.dcs.ed.ac.uk/home/lego.
James H. Morris. Comments on “procedures and parameters”. Undated and unpublished.
Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Proceedings of 16th Conference on Foundations of Software Technology and Theoretical Computer Science (Hyderabad, India, December 18–20, 1996), volume 1180 of Lecture Notes in Computer Science, pages 180–192. Springer, 1996.
Ernst-Rüdiger Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science, 24:337–347, 1983.
Stefan Sokołowski. Total correctness for procedures. In J. Gruska, editor, Sixth Mathematical Foundations of Computer Science (Tatranská Lomnica), volume 53 of Lecture Notes in Computer Science, pages 475–483. Springer, 1977.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schreiber, T. (1997). Auxiliary variables and recursive procedures. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030635
Download citation
DOI: https://doi.org/10.1007/BFb0030635
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive