Article

Local Reasoning about Programs that Alter Data Structures

Authors:

Peter W. O'Hearn,

John C. Reynolds,

Hongseok YangAuthors Info & Claims

CSL '01: Proceedings of the 15th International Workshop on Computer Science Logic

Pages 1 - 19

Published: 10 September 2001 Publication History

Abstract

We describe an extension of Hoare's logic for reasoning about programs that alter data structures. We consider a low-level storage model based on a heap with associated lookup, update, allocation and deallocation operations, and unrestricted address arithmetic. The assertion language is based on a possible worlds model of the logic of bunched implications, and includes spatial conjunction and implication connectives alongside those of classical logic. Heap operations are axiomatized using what we call the "small axioms", each of which mentions only those cells accessed by a particular command. Through these and a number of examples we show that the formalism supports local reasoning: A specification and proof can concentrate on only those cells in memory that a program accesses.

This paper builds on earlier work by Burstall, Reynolds, Ishtiaq and O'Hearn on reasoning about data structures.

References

[1]

A. Borgida, J. Mylopoulos, and R. Reiter. On the frame problem in procedure specifications. IEEE Transactions of Software Engineering, 21:809-838, 1995.

[2]

R. Bornat. Proving pointer programs in Hoare logic. Mathematics of Program Construction, 2000.

[3]

R.M. Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, 7:23-50, 1972.

[4]

C. Calcagno, S. Isthiaq, and P. W. O'Hearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. Proceedings of the Second International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2000.

[5]

P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 843-993. Elsevier, Amsterdam, and The MIT Press, Cambridge, Mass., 1990.

[6]

C. A. R. Hoare and J. He. A trace model for pointers and objects. In Rachid Guerraoui, editor, ECCOP'99 - Object-Oriented Programming, 13th European Conference, pages 1-17, 1999. Lecture Notes in Computer Science, Vol. 1628, Springer.

[7]

S. Isthiaq and P.W. O'Hearn. BI as an assertion language for mutable data structures. In Conference Record of the Twenty-Eighth Annual ACM Symposium on Principles of Programming Languages, pages 39-46, London, January 2001.

[8]

K. R. M. Leino and G. Nelson. Data abstraction and information hiding. Technical Report Reearch Report 160, Compaq Systems Research Center, Palo Alto, CA, November 2000.

[9]

J. McCarthy and P. Hayes. Some philosophical problems from the standpoint of artificial intelligence. Machine Intelligence, 4:463-502, 1969.

[10]

P. W. O'Hearn. Resource interpretations, bunched implications and the αλ-calculus. In Typed λ-calculus and Applications, J-Y Girard editor, L'Aquila, Italy, April 1999. Lecture Notes in Computer Science 1581.

[11]

P. W. O'Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, June 99.

[12]

P. W. O'Hearn and J. C. Reynolds. From Algol to polymorphic linear lambda-calculus. J. ACM, 47(1):267-223, January 2000.

[13]

P. W. O'Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3):658-709, May 1995. Also in {14}, vol 2, pages 109-164.

[14]

P. W. O'Hearn and R. D. Tennent, editors. Algol-like Languages. Two volumes, Birkhauser, Boston, 1997.

[15]

F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. Ph.D. thesis, Syracuse University, Syracuse, N.Y., 1982.

[16]

F. J. Oles. Functor categories and store shapes. In O'Hearn and Tennent {14}, pages 3-12. Vol. 2.

[17]

D. J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Monograph to appear, 2001.

[18]

J. C. Reynolds. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39-46, Tucson, Arizona, January 1978. ACM, New York. Also in {14}, vol 1.

[19]

J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345-372, Amsterdam, October 1981. North-Holland, Amsterdam. Also in {14}, vol 1, pages 67-88.

[20]

J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Jim Davies, Bill Roscoe, and Jim Woodcock, editors, Millennial Perspectives in Computer Science, pages 303-321, Houndsmill, Hampshire, 2000. Palgrave.

[21]

J. C. Reynolds. Lectures on reasoning about shared mutable data structure. IFIP Working Group 2.3 School/Seminar on State-of-the-Art Program Design Using Logic. Tandil, Argentina, September 2000.

[22]

M. Shanahan. Solving the Frame Problem: A Mathematical Investigation of the Common Sense Law of Inertia. MIT Press, 1997.

[23]

H. Yang. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. Manuscript, October 2000.

[24]

H. Yang. Local Reasoning for Stateful Programs. Ph.D. thesis, University of Illinois, Urbana-Champaign, Illinois, USA, 2001 (expected).

Cited By

Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Murali APeña LLöding CMadhusudan P(2023)A First-order Logic with FramesACM Transactions on Programming Languages and Systems10.1145/358305745:2(1-44)Online publication date: 15-May-2023
https://dl.acm.org/doi/10.1145/3583057
Krogmeier PLin ZMurali AMadhusudan P(2022)Synthesizing axiomatizations using logic learningProceedings of the ACM on Programming Languages10.1145/35633486:OOPSLA2(1697-1725)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563348
Show More Cited By

Local Reasoning about Programs that Alter Data Structures
1. Theory of computation

Recommendations

Epistemic reasoning in logic programs
IJCAI'07: Proceedings of the 20th international joint conference on Artifical intelligence

Although epistemic logic programming has an enhanced capacity to handle complex incomplete information reasoning and represent agents' epistemic behaviours, it embeds a significantly higher computational complexity than non-disjunctive and disjunctive ...
Reasoning about probabilistic sequential programs

A complete and decidable Hoare-style calculus for iteration-free probabilistic sequential programs is presented using a state logic with truth-functional propositional (not arithmetical) connectives.
Reasoning about states of probabilistic sequential programs
CSL'06: Proceedings of the 20th international conference on Computer Science Logic

A complete and decidable propositional logic for reasoning about states of probabilistic sequential programs is presented. The state logic is then used to obtain a sound Hoare-style calculus for basic probabilistic sequential programs. The Hoare ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CSL '01: Proceedings of the 15th International Workshop on Computer Science Logic

September 2001

613 pages

ISBN:3540425543

Editor:
Laurent Fribourg

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 10 September 2001

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

249
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Murali APeña LLöding CMadhusudan P(2023)A First-order Logic with FramesACM Transactions on Programming Languages and Systems10.1145/358305745:2(1-44)Online publication date: 15-May-2023
https://dl.acm.org/doi/10.1145/3583057
Krogmeier PLin ZMurali AMadhusudan P(2022)Synthesizing axiomatizations using logic learningProceedings of the ACM on Programming Languages10.1145/35633486:OOPSLA2(1697-1725)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563348
Ahrens EBozga MIosif RKatoen J(2022)Reasoning about distributed reconfigurable systemsProceedings of the ACM on Programming Languages10.1145/35632936:OOPSLA2(145-174)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563293
Bao YWei GBračevac OJiang YHe QRompf T(2021)Reachability types: tracking aliasing and separation in higher-order functional programsProceedings of the ACM on Programming Languages10.1145/34855165:OOPSLA(1-32)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485516
Hill AKomendantskaya EDaggitt MPetrick RKo HOrchard D(2021)Actions you can handle: dependent types for AI plansProceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3471875.3472990(1-13)Online publication date: 18-Aug-2021
https://dl.acm.org/doi/10.1145/3471875.3472990
Demri SLozes EMansutti A(2021)The Effects of Adding Reachability Predicates in Quantifier-Free Separation LogicACM Transactions on Computational Logic10.1145/344826922:2(1-56)Online publication date: 21-Jun-2021
https://dl.acm.org/doi/10.1145/3448269
Jung RJourdan JKrebbers RDreyer D(2021)Safe systems programming in RustCommunications of the ACM10.1145/341829564:4(144-152)Online publication date: 22-Mar-2021
https://dl.acm.org/doi/10.1145/3418295
Bao JDocherty SHsu JSilva AGorla D(2021)A bunched logic for conditional independenceProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470712(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470712
Zhou LBarthe GHsu JYing MYu NGorla D(2021)A quantum interpretation of bunched logic & quantum separation logicProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470673(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470673
Show More Cited By

View Options

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

Media

Figures

Other

Tables

View Table of Contents