article

BI as an assertion language for mutable data structures

Authors:

Samin S. Ishtiaq,

Peter W. O'HearnAuthors Info & Claims

ACM SIGPLAN Notices, Volume 36, Issue 3

Pages 14 - 26

https://doi.org/10.1145/373243.375719

Published: 01 January 2001 Publication History

Abstract

Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of bunched implications of O'Hearnand Pym. We begin by giving a model in which the law of the excluded middleholds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to a translation from intuitionistic logic into the modal logic S4. We also consider the question of completeness of the axioms. BI's spatial implication is used to express weakest preconditions for object-component assignments, and an axiom for allocating a cons cell is shown to be complete under an interpretation of triplesthat allows a command to be applied to states with dangling pointers. We make this latter a feature, by incorporating an operation, and axiom, for disposing of memory. Finally, we describe a local character enjoyed by specifications in the logic, and show how this enables a class of frame axioms, which say what parts of the heap don't change, to be inferred automatically.

References

[1]

Alur, R., and Grosu, R. Modular refinement of hierarchic reactive machines. In POPL {31}.]]

Digital Library

[2]

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

Digital Library

[3]

Bornat, R. Proving pointer programs in Hoare logic. In Fifth Internationsl Conference on Mathematics of Program Construction, LNCS 1837, Ponte de Lima, Portugal, 2000.]]

Digital Library

[4]

Brookes, S., Main, M., Melton, A., and Mislove, M., Eds. Mathematical Foundations of Programming Semantics, Eleventh Annual Conference (Tulane University, New Orleans, Louisiana, March 29-April 1 1995), vol. 1 of Electronic Notes in Theoretical Computer Science, Elsevier Science.]]

[5]

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

[6]

Calcagno, C., Ishtiaq, S., and O'Hearn, P. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000.]]

Digital Library

[7]

Cardelli, L., and Ghelli, G. A query language for semistructured data based on the ambient logic. Manuscript, 4 April 2000.]]

[8]

Cardelli, L., and Gordon, A. D. Anytime, anywhere. modal logics for mobile ambients. In POPL {31}.]]

Digital Library

[9]

Cervesato, I., and Pfenning, F. A linear logical framework. In Proceedings of the Eleventh Annual Symposium on Logic in Computer Science | LICS'96 (27-30 July 1996), IEEE Computer Society Press, pp. 264-275.]]

Digital Library

[10]

Cook, S. A. Soundness and completeness of an axiomatic system for program verification. SIAM J. on Computing 7 (1978), 70-90.]]

[11]

de Boer, F. A WP calculus for OO. In Proceedings of FOSSACS'99 (1999).]]

Digital Library

[12]

Girard, J.-Y. Linear logic. Theoretical Computer Science (1987), 1-102.]]

Digital Library

[13]

Girard, J.-Y. Towards a geometry of interaction. In Categories in Computer Science and Logic (1989), American Mathematical Society, pp. 69-108. Contemporary Mathematics Volume 92.]]

[14]

Guttag, J., Horning, J., and Wing, J. Larch in five easy pieces. TR 5, DEC Systems Research Center, 1985.]]

[15]

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

Digital Library

[16]

Hoare, C. A. R., and Wirth, N. An axiomatic definition of the programming language Pascal. Acta Informatica 2 (1973), 335-355.]]

Digital Library

[17]

Honsell, F., Mason, I. A., Smith, S., and Talcott, C. A variable typed logic of effects. Information and Computation 119, 1 (may 1995), 55-90.]]

Digital Library

[18]

Jenson, J., Jorgensen, M., Klarkund, N., and Schwartzback, M. Automatic verification of pointer programs using monadic second-order logic. In Proceedings of the ACM SIGPLAN'97 Conference on Programming Language Design and Implementation (1997), pp. 225-236. SIGPLAN Notices 32(5).]]

Digital Library

[19]

Kripke, S. A. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions, J. N. Crossley and M. A. E. Dummett, Eds. North-Holland, Amsterdam, 1965, pp. 92-130.]]

[20]

Leino, K. Toward Reliable Modular Programs. Ph.D. thesis, California Institute of Technology, Pasadena, California, 1995.]]

Digital Library

[21]

Miller, D. Observations about using logic as a specification language. In GULP-PRODE'95 - Joint Conference on Declarative Programming (Marina de Vietri, Salerno, Italy, September 1995).]]

[22]

Moller, B. Calculating with pointer structures. In Proceedings of Mathematics for Software Construction, (1997), Chapman and Hall, pp. 24-48.]]

Digital Library

[23]

Morris, J. A general axiom of assignment. Assignment and linked data structure. A proof of the Schorr-Waite algorithm. In Theoretical Foundations of Programming Methodology (1982), M. Broy and G. Schmidt, Eds., Reidel, pp. 25-51.]]

[24]

Necula, G. Proof-carrying code. In In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL '97) (1997).]]

Digital Library

[25]

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

[26]

O'Hearn, P., Pym, D., and Yang, H. Possible worlds and resources: The semantics of BI. Submitted, October 2000.]]

[27]

O'Hearn, P., and Yang, H. Local reasoning about pointer programs using bunched implications. In Preparation, 2000.]]

[28]

O'Hearn, P. W., Power, A. J., Takeyama, M., and Tennent, R. D. Syntactic control of interference revisited. Theoretical Computer Science 228, 1-2 (October 1999), 211-252. Preliminary version in {4} and in {29}, vol 2.]]

Digital Library

[29]

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

Digital Library

[30]

Oppen, D. C., and Cook, S. A. Proving assertions about programs that manipulate data structures. In Conference Record of Seventh Annual ACM Symposium on Theory of Computation (Albuquerque, New Mexico, 5-7 May 1975), pp. 107-116.]]

Digital Library

[31]

Conference Record of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2000), ACM, New York.]]

[32]

Pym, D. The semantics and proof theory of the logic of bunched implications. Monograph in Preparation, 2000. See http://www.dcs.qmw.ac.uk/~pym.]]

[33]

Reiter, R. The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 359-380. Academic Press, 1991.]]

Digital Library

[34]

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

Digital Library

[35]

Reynolds, J. C. Intuitionistic reasoning about shared mutable data structure. In Millenial Perspectives in Computer Science, Palgrove, 2000.]]

[36]

Reynolds, J. C. 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.]]

[37]

Sagiv, M., Reps, T., and Wilhelm, R. Parametric shape analysis via 3valued logic. In POPL'99.]]

Digital Library

[38]

Smith, F., Walker, D., and Morrisett, G. Alias types. Proceedings of ESOP'99.]]

Digital Library

[39]

Walker, D., and Morrisett, G. Alias types for recursive data structures. Manuscript, April 2000.]]

[40]

Xu, Z., Miller, B., and Reps, T. Safety checking of machine code. In PLDI'00.]]

Digital Library

Cited By

Xu QSanan DHou ZLuan XWatt CLiu Y(2025)Generically Automating Separation Logic by Functors, Homomorphisms, and ModulesProceedings of the ACM on Programming Languages10.1145/37049039:POPL(1992-2024)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704903
Bednarczyk BDemri SFervari RMansutti A(2023)On Composing Finite Forests with Modal LogicsACM Transactions on Computational Logic10.1145/356995424:2(1-46)Online publication date: 3-Apr-2023
https://dl.acm.org/doi/10.1145/3569954
Matheja CPagel JZuleger F(2023)A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive DefinitionsACM Transactions on Computational Logic10.1145/353492724:1(1-76)Online publication date: 18-Jan-2023
https://dl.acm.org/doi/10.1145/3534927
Show More Cited By

Index Terms

BI as an assertion language for mutable data structures

Recommendations

BI as an assertion language for mutable data structures
POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the ...
BI as an assertion language for mutable data structures

Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the ...
Bi-Simulating in Bi-Intuitionistic Logic

Bi-intuitionistic logic is the result of adding the dual of intuitionistic implication to intuitionistic logic. In this note, we characterize the expressive power of this logic by showing that the first order formulas equivalent to translations of bi-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 36, Issue 3

March 2001

303 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/373243

Editors:
Cindy Norris
Appalachian State Univ., Boone, NC
,
James B. Fenwick
Appalachian State Univ., Boone, NC

Issue’s Table of Contents

POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2001
304 pages
ISBN:1581133367
DOI:10.1145/360204
Chairmen:
Chris Hankin
Imperial College, London, U. K.
,
Dave Schmidt
Kansas State Univ., Manhattan

Copyright © 2001 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2001

Published in SIGPLAN Volume 36, Issue 3

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

452
Total Citations
View Citations
1,041
Total Downloads

Downloads (Last 12 months)85
Downloads (Last 6 weeks)7

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Xu QSanan DHou ZLuan XWatt CLiu Y(2025)Generically Automating Separation Logic by Functors, Homomorphisms, and ModulesProceedings of the ACM on Programming Languages10.1145/37049039:POPL(1992-2024)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704903
Bednarczyk BDemri SFervari RMansutti A(2023)On Composing Finite Forests with Modal LogicsACM Transactions on Computational Logic10.1145/356995424:2(1-46)Online publication date: 3-Apr-2023
https://dl.acm.org/doi/10.1145/3569954
Matheja CPagel JZuleger F(2023)A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive DefinitionsACM Transactions on Computational Logic10.1145/353492724:1(1-76)Online publication date: 18-Jan-2023
https://dl.acm.org/doi/10.1145/3534927
Echenim MPeltier N(2023)An undecidability result for separation logic with theory reasoningInformation Processing Letters10.1016/j.ipl.2023.106359(106359)Online publication date: Jan-2023
https://doi.org/10.1016/j.ipl.2023.106359
Echenim MPeltier N(2023)A Proof Procedure for Separation Logic with Inductive Definitions and DataJournal of Automated Reasoning10.1007/s10817-023-09680-467:3Online publication date: 9-Sep-2023
https://dl.acm.org/doi/10.1007/s10817-023-09680-4
Peltier N(2023)Testing the Satisfiability of Formulas in Separation Logic with PermissionsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_23(427-445)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_23
Le QLe X(2023)An Efficient Cyclic Entailment Procedure in a Fragment of Separation LogicFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_23(477-497)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_23
Colvin R(2023)A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory ModelsFormal Methods10.1007/978-3-031-27481-7_18(301-320)Online publication date: 3-Mar-2023
https://doi.org/10.1007/978-3-031-27481-7_18
Gheorghiu ADocherty SPym D(2023)Reductive Logic, Proof-Search, and Coalgebra: A Perspective from Resource SemanticsSamson Abramsky on Logic and Structure in Computer Science and Beyond10.1007/978-3-031-24117-8_23(833-875)Online publication date: 2-Aug-2023
https://doi.org/10.1007/978-3-031-24117-8_23
Haase DGrädel EWilke R(2022)Separation logic and logics with team semanticsAnnals of Pure and Applied Logic10.1016/j.apal.2021.103063173:10(103063)Online publication date: Dec-2022
https://doi.org/10.1016/j.apal.2021.103063
Show More Cited By

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.

Figures

Tables

Media

View Issue’s Table of Contents