More Web Proxy on the site http://driver.im/

Article

Reasoning about recursive procedures with parameters

Authors:

Ralph-Johan Back,

Viorel PreoteasaAuthors Info & Claims

MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding

Pages 1 - 7

https://doi.org/10.1145/976571.976573

Published: 26 August 2003 Publication History

Abstract

In this paper we extend the model of program variables from the Refinement Calculus [2] in order to be able to reason more algebraically about recursive procedures with parameters and local variables. We extend the meaning of variable substitution or freeness from the syntax to the semantics of program expressions. We give a predicate transformer semantics to recursive procedures with parameters and prove a refinement rule for introduction of recursive procedure calls. We also prove a Hoare total correctness rule for our recursive procedures. These rules have no side conditions and are easier to apply to programs than the ones in the literature. The theory is built having in mind mechanical verification support using theorem provers like PVS [18] or HOL [11].

References

[1]

R. J. Back and V. Preoteasa. Reasoning about recursive procedures with parameters. Technical Report 500, TUCS - Turku Centre for Computer Science, January 2003.]]

Digital Library

[2]

R. J. Back and J. von Wright. Refinement Calculus. A systematic Introduction. Springer, 1998.]]

Digital Library

[3]

R. J. Back and J. von Wright. Compositional action system refinement. In J. Derrick, E. Boiten, J. Woodcock, and J. von Wright, editors, Electronic Notes in Theoretical Computer Science, volume 70. Elsevier Science Publishers, 2002.]]

[4]

O. Celiku and J. von Wright. Theorem prover support for precondition and correctness calculation. In 4th International Conference on Formal Engineering Methods, volume 2495 of Lecture Notes in Computer Science, pages 299--310. Springer-Verlag, October 2002.]]

Digital Library

[5]

A. Church. A formulation of the simple theory of types. J. Symbolic logic, 5:56--68, 1940.]]

[6]

B. A. Davey and H. A. Priestley. Introduction to lattices and order. Cambridge University Press, New York, second edition, 2002.]]

[7]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM, 18(8):453--457, 1975.]]

Digital Library

[8]

E. W. Dijkstra. A discipline of programming. Prentice-Hall Inc., Englewood Cliffs, N.J., 1976. With a foreword by C. A. R. Hoare, Prentice-Hall Series in Automatic Computation.]]

Digital Library

[9]

J. E. Donahue. Complementary definitions of programming language semantics. Springer-Verlag, Berlin, 1976. Lecture Notes in Computer Science, Vol. 42.]]

Digital Library

[10]

M. J. C. Gordon. Mechanizing programming logics in higher-order logic. In Birtwistle, G. M. and Subrahmanyam, P. A., editors, Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification), pages 387--439, Banff, Canada, 1988. Springer-Verlag, Berlin.]]

Digital Library

[11]

M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL. Cambridge University Press, Cambridge, 1993. A theorem proving environment for higher order logic, Appendix B by R. J. Boulton.]]

Digital Library

[12]

W. M. Hesselink. Predicate transformers for recursive procedures with local variables. Formal Aspect of Computing, 11:616--336, 1999.]]

[13]

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, 1969.]]

Digital Library

[14]

T. Kleymann. Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, 1998.]]

[15]

T. Kleymann. Hoare logic and auxiliary variables. Formal Aspect of Computing, 11:541--566, 1999.]]

[16]

L. Laibinis. Mechanised Formal Reasoning About Modular Programs. PhD dissertation, Turku Centre for Computer Science, April 2000.]]

[17]

C. Morgan. Procedures, parameters, and abstraction: separate concerns. Sci. Comput. Programming, 11(1):17--27, 1988.]]

Digital Library

[18]

S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Clavert. PVS Language Reference, 1999.]]

[19]

J. C. Reynolds. The Craft of Programming. Prentice-Hall Inc., London, 1981.]]

Digital Library

[20]

J. C. Reynolds. The essence of ALGOL. In Algorithmic languages (Amsterdam, 1981), pages 345--372. North-Holland, Amsterdam, 1981.]]

[21]

M. Staples. A Mechanised Theory of Refinement. PhD dissertation, Computer Laboratory, University of Cambridge, November 1998.]]

[22]

M. Staples. Representing WP semantics in Isabelle/ZF. In Theorem proving in higher order logics (Nice, 1999), volume 1690 of Lecture Notes in Comput Sci., pages 239--254. Springer, Berlin, 1999.]]

Digital Library

[23]

M. Staples. Interfaces for refining recursion and procedures. Formal Aspect of Computing, 12:372--391, 2000.]]

[24]

A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math., 5:285--309, 1955.]]

[25]

D. 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, volume 1738 of LNCS, pages 168--180. Springer, 1999.]]

Digital Library

Cited By

Foster SZeyda FWoodcock J(2016)Unifying Heterogeneous State-Spaces with LensesTheoretical Aspects of Computing – ICTAC 201610.1007/978-3-319-46750-4_17(295-314)Online publication date: 22-Sep-2016
https://doi.org/10.1007/978-3-319-46750-4_17
Zeyda FCavalcanti A(2013)Higher-Order UTP for a Theory of MethodsUnifying Theories of Programming10.1007/978-3-642-35705-3_10(204-223)Online publication date: 2013
https://doi.org/10.1007/978-3-642-35705-3_10
Almeida JFrade MPinto JMelo de Sousa SAlmeida JFrade MPinto JMelo de Sousa S(2011)Procedures and ContractsRigorous Software Development10.1007/978-0-85729-018-2_8(195-227)Online publication date: 2011
https://doi.org/10.1007/978-0-85729-018-2_8
Show More Cited By

Index Terms

Reasoning about recursive procedures with parameters
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
    2. Program semantics

Recommendations

Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic
We provide a sound and relatively complete Hoare logic for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism and in which the correctness proofs support contracts and are ...
Propositional Dynamic Logic for Recursive Procedures
VSTTE '08: Proceedings of the 2nd international conference on Verified Software: Theories, Tools, Experiments

We present a simple and natural deductive formalism <em>μ</em>PDL for propositional dynamic logic for recursive procedures, including simultaneous recursion. Though PDL with recursive programs is known to be highly undecidable, natural deductive ...
Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding

August 2003

97 pages

ISBN:1581138008

DOI:10.1145/976571

Copyright © 2003 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

ACM: Association for Computing Machinery

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 August 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

MERLIN03

Sponsor:

ACM

MERLIN03: Mechanized Reasoning about Languages with Variable Binding 2003 Wokshop

26 08 2003

Uppsala, Sweden

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
270
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Foster SZeyda FWoodcock J(2016)Unifying Heterogeneous State-Spaces with LensesTheoretical Aspects of Computing – ICTAC 201610.1007/978-3-319-46750-4_17(295-314)Online publication date: 22-Sep-2016
https://doi.org/10.1007/978-3-319-46750-4_17
Zeyda FCavalcanti A(2013)Higher-Order UTP for a Theory of MethodsUnifying Theories of Programming10.1007/978-3-642-35705-3_10(204-223)Online publication date: 2013
https://doi.org/10.1007/978-3-642-35705-3_10
Almeida JFrade MPinto JMelo de Sousa SAlmeida JFrade MPinto JMelo de Sousa S(2011)Procedures and ContractsRigorous Software Development10.1007/978-0-85729-018-2_8(195-227)Online publication date: 2011
https://doi.org/10.1007/978-0-85729-018-2_8
Preoteasa V(2009)Frame rule for mutually recursive procedures manipulating pointersTheoretical Computer Science10.1016/j.tcs.2009.05.016410:42(4216-4233)Online publication date: 1-Sep-2009
https://dl.acm.org/doi/10.1016/j.tcs.2009.05.016
Back RXiaocong Fan Preoteasa V(2003)Reasoning about pointers in refinement calculusTenth Asia-Pacific Software Engineering Conference, 2003.10.1109/APSEC.2003.1254398(425-434)Online publication date: 2003
https://doi.org/10.1109/APSEC.2003.1254398

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents