article

Context logic and tree update

Authors:

Cristiano Calcagno,

Philippa Gardner,

Uri ZarfatyAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 271 - 282

https://doi.org/10.1145/1047659.1040328

Published: 12 January 2005 Publication History

Get Access

Abstract

Spatial logics have been used to describe properties of tree-like structures (Ambient Logic) and in a Hoare style to reason about dynamic updates of heap-like structures (Separation Logic). We integrat this work by analyzing dynamic updates to tree-like structures with pointers (such as XML with identifiers and idrefs). Naíve adaptations of the Ambient Logic are not expressive enough to capture such local updates. Instead we must explicitly reason about arbitrary tree contexts in order to capture updates throughout the tree. We introduce Context Logic, study its proof theory and models, and show how it generalizes Separation Logic and its general theory BI. We use it to reason locally about a small imperative programming language for updating trees, using a Hoare logic in the style of O'Hearn, Reynolds and Yang, and show that weakest preconditions are derivable. We demonstrate the robustness of our approach by using Context Logic to capture the locality of term rewrite systems.

References

[1]

S. Abiteboul, P. Buneman, and D. Suciu. Data on the Web: from relations to semistructured data and XML. Morgan Kaufmann, 1999.]]

Digital Library

Google Scholar

[2]

N. Biri and D. Galmich. A separation logic for resource distribution. In 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2003.]]

Crossref

Google Scholar

[3]

C. Calcagno, P. Gardner, and U. Zarfaty. A context logic for tree update. In Proceedings of Workshop on Logics for Resources, Processes and Programs (LRPP '04), 2004.]]

Google Scholar

[4]

L. Cardelli, P. Gardner, and G. Ghelli. Querying trees with pointers. Unpublished Notes, 2003; talk at APPSEM 2001.]]

Google Scholar

[5]

L. Cardelli and A. D. Gordon. Mobil ambients. Theoretical Comput. Sci., 240:177--213, 2000.]]

Digital Library

Google Scholar

[6]

S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In 28th POPL, pages 14--26, London, January 2001.]]

Digital Library

Google Scholar

[7]

P. O'Harn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In L. Fribourg, editor, Computer Science Logic (CSL'01), pages 1--19. Springer-Verlag, 2001. LNCS 2142.]]

Digital Library

Google Scholar

[8]

D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implicetions. Applied Logic Series. Kluwer Academic Publishers, 2002. http://www.dcs.qmul.ac.uk/~pym/Papersage/bunch.ps.]]

Crossref

Google Scholar

[9]

J. Reynolds. Separation logic: a logic for shared mutable data structures. Invited Paper, LICS '02, 2002.]]

Digital Library

Google Scholar

[10]

I. Tatarinov, Z. G. Ives, A. Y. Halevy, and D. S. Weld. Updating XML. SIGMOD 2001, Santa Barbara, CA.]]

Digital Library

Google Scholar

[11]

H. Yang and C. Calcagno. Completeness results for Context Logic and BI. In preparation, 2004.]]

Google Scholar

[12]

H. Yang and P. O'Hearn. A semantic basis for local reasoning. Proceedings of FOSSACS, 2002.]]

Digital Library

Google Scholar

Cited By

View all

Bednarczyk BDemri SFervari RMansutti A(2022)On Composing Finite Forests with Modal LogicsACM Transactions on Computational Logic10.1145/3569954Online publication date: 29-Dec-2022
https://doi.org/10.1145/3569954
Jipsen PLitak T(2021)An Algebraic Glimpse at Bunched Implications and Separation LogicHiroakira Ono on Substructural Logics10.1007/978-3-030-76920-8_5(185-242)Online publication date: 14-Dec-2021
https://doi.org/10.1007/978-3-030-76920-8_5
Gardner PNtzik GWright A(2014)Local Reasoning for the POSIX File SystemProceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 841010.1007/978-3-642-54833-8_10(169-188)Online publication date: 5-Apr-2014
https://dl.acm.org/doi/10.1007/978-3-642-54833-8_10
Show More Cited By

Index Terms

Context logic and tree update

Recommendations

Context logic and tree update
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Spatial logics have been used to describe properties of tree-like structures (Ambient Logic) and in a Hoare style to reason about dynamic updates of heap-like structures (Separation Logic). We integrat this work by analyzing dynamic updates to tree-like ...
Context logic as modal logic: completeness and parametric inexpressivity
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Separation Logic, Ambient Logic and Context Logic are based on a similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) ...
Context logic as modal logic: completeness and parametric inexpressivity
Proceedings of the 2007 POPL Conference

Separation Logic, Ambient Logic and Context Logic are based on a similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 40, Issue 1

Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

391 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1047659

Issue’s Table of Contents

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
402 pages
ISBN:158113830X
DOI:10.1145/1040305
General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

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: 12 January 2005

Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

72
Total Citations
View Citations
601
Total Downloads

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

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Bednarczyk BDemri SFervari RMansutti A(2022)On Composing Finite Forests with Modal LogicsACM Transactions on Computational Logic10.1145/3569954Online publication date: 29-Dec-2022
https://doi.org/10.1145/3569954
Jipsen PLitak T(2021)An Algebraic Glimpse at Bunched Implications and Separation LogicHiroakira Ono on Substructural Logics10.1007/978-3-030-76920-8_5(185-242)Online publication date: 14-Dec-2021
https://doi.org/10.1007/978-3-030-76920-8_5
Gardner PNtzik GWright A(2014)Local Reasoning for the POSIX File SystemProceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 841010.1007/978-3-642-54833-8_10(169-188)Online publication date: 5-Apr-2014
https://dl.acm.org/doi/10.1007/978-3-642-54833-8_10
Dinsdale-Young TGardner PWheelhouse M(2010)Abstraction and refinement for local reasoningProceedings of the Third international conference on Verified software: theories, tools, experiments10.5555/1884866.1884888(199-215)Online publication date: 16-Aug-2010
https://dl.acm.org/doi/10.5555/1884866.1884888
Bolander THansen R(2010)Hybrid logical analyses of the ambient calculusInformation and Computation10.1016/j.ic.2009.01.006208:5(433-449)Online publication date: 1-May-2010
https://dl.acm.org/doi/10.1016/j.ic.2009.01.006
Raza MGardner P(2009)Footprints in Local ReasoningLogical Methods in Computer Science10.2168/LMCS-5(2:4)20095:2Online publication date: 24-Apr-2009
https://doi.org/10.2168/LMCS-5(2:4)2009
Michel PPoetzsch-Heffter A(2009)Maintaining XML Data Integrity in ProgramsProceedings of the 36th Conference on Current Trends in Theory and Practice of Computer Science10.1007/978-3-642-11266-9_50(600-611)Online publication date: 8-Dec-2009
https://dl.acm.org/doi/10.1007/978-3-642-11266-9_50
Zarfaty UGardner P(2006)Local Reasoning About Tree UpdateElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2006.04.020158(399-424)Online publication date: 1-May-2006
https://dl.acm.org/doi/10.1016/j.entcs.2006.04.020
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
Raad ASantos JGardner P(2016)DOM: Specification and Client ReasoningProgramming Languages and Systems10.1007/978-3-319-47958-3_21(401-422)Online publication date: 9-Oct-2016
https://doi.org/10.1007/978-3-319-47958-3_21
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.

Cited By

Index Terms

Recommendations

Context logic and tree update

Context logic as modal logic: completeness and parametric inexpressivity

Context logic as modal logic: completeness and parametric inexpressivity