Article

Separation and information hiding

Authors:

Peter W. O'Hearn,

John C. ReynoldsAuthors Info & Claims

POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 268 - 280

https://doi.org/10.1145/964001.964024

Published: 01 January 2004 Publication History

Abstract

We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical connective gives rise to a form of dynamic partitioning, where we track the transfer of ownership of portions of heap storage between program components. It also enables us to enforce separation in the presence of mutable data structures with embedded addresses that may be aliased.

References

[1]

A. Ahmed, L. Jia, and D. Walker. Reasoning about hierarchical storage. In 18th LICS, 2003.]]

Digital Library

[2]

T. Ball and S. Rajamani. Checking temporal properties of software with boolean programs. Proceedings of the Workshop on Advances in Verification, 2000.]]

[3]

A. Banerjee and D. Naumann. Representation independence, confinement and access control. In 29th POPL, 2002.]]

Digital Library

[4]

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

Digital Library

[5]

L. Cardelli and L~Caires. A spatial logic for concurrency. In TACS'01, LNCS 2255:1--37, Springer, 2001.]]

Digital Library

[6]

L. Cardelli, P. Gardner, and G. Ghelli. Querying trees with pointers. Unpublished notes, 2003.]]

[7]

L. Cardelli, P. Gardner, and G. Ghelli. A spatial logic for querying graphs. Proceedings of ICALP'02.]]

Digital Library

[8]

L. Cardelli and G. Ghelli. A query language for semistructured data based on the ambient logic. Proceedings of ESOP'01.]]

Digital Library

[9]

L. Cardelli and A. D. Gordon. Anytime, anywhere. Modal logics for mobile ambients. In 27th POPL, 2000.]]

Digital Library

[10]

D. Clarke, J. Noble, and J. Potter. Simple ownership types for object containment. ECOOP, LNCS 2072, 2001.]]

Digital Library

[11]

J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pǎsǎreanu, Robby, and H. Zheng. Bandera: extracting finite-state models from Java source code. In International Conference on Software Engineering, pages 439--448, 2000.]]

Digital Library

[12]

K.R.M. Leino D. Detlefs and G. Nelson. Wrestling with rep exposure. Digital SRC Research Report 156, 1998.]]

[13]

F. de Boer. A WP calculus for OO. In FOSSACS, 1999.]]

Digital Library

[14]

M. Gabbay and A. Pitts. A new approach to abstract syntax involving binders. In 14th LICS, 1999.]]

Digital Library

[15]

C. Grothoff, J. Palsberg, and J. Vitek. Encapsulating objects with confined types. OOPSLA, pp241--253, 2001.]]

Digital Library

[16]

C.A.R. Hoare. Towards a theory of parallel programming. In Hoare and Perrot, editors, Operating Systems Techniques. Academic Press, 1972.]]

[17]

C.A.R. Hoare. Monitors: An operating system structuring concept. C.ACM, 17(10):549--557, October 1974.]]

Digital Library

[18]

J. Hogg, D. Lea, R. Holt, A. Wills, and D. de Champeaux. The Geneva convention on the treatment of object aliasing. OOPS Messenger, April, 1992.]]

Digital Library

[19]

S. Isthiaq and P.W. O'Hearn. BI as an assertion language for mutable data structures. In 28th POPL, 2001.]]

Digital Library

[20]

C.B. Jones. Specification and design of (parallel) programs. IFIP Conference, 1983.]]

[21]

B. Kernighan and D. Ritchie. The C programming language. Prentice Hall, 1988.]]

Digital Library

[22]

K.R.M. Leino and G. Nelson. Data abstraction and information hiding. ACM TOPLAS 24(5): 491--553, 2002.]]

Digital Library

[23]

J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions of Software Engineering, July, 1981.]]

Digital Library

[24]

J.C. Mitchell and G.D. Plotkin. Abstract types have existential type. ACM TOPLAS 10(3):470--502, 1988.]]

Digital Library

[25]

P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In Proceedings of Computer Science Logic, pages 1--19, 2001. LNCS 2142.]]

Digital Library

[26]

S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319--340, 1976.]]

Digital Library

[27]

D.L. Parnas. Information distribution aspects of design methodology. IFIP Congress (1) 1971: 339--344, 1972.]]

[28]

D.L. Parnas. On the criteria to be used in decomposing systems into modules. C.ACM, 15(12):1053--1058, 1972.]]

Digital Library

[29]

B.C. Pierce and D.N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207--247, 1994.]]

[30]

D.J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Applied Logic series, 2002.]]

[31]

D.J. Pym, P.W. O'Hearn, and H. Yang. Possible worlds and resources: the semantics of BI. TCS, to appear, 2003.]]

Digital Library

[32]

U. Reddy and H. Yang. Correctness of data representations involving heap data structures. Proceedings of ESOP, 2003.]]

[33]

B. Reus, M. Wirsing, and R. Hennicker. A Hoare calculus for verifying Java realizations of OCL-constrained design models. FASE Proceedings, LNCS 2029, pp300--316, 2001.]]

Digital Library

[34]

J.C. Reynolds. Types, abstraction and parametric polymorphism. IFIP Proceedings, pp513--523, 1983.]]

[35]

J.C. Reynolds. Separation logic: a logic for shared mutable data structures. Invited Paper, 17th LICS, 2002.]]

Digital Library

[36]

D. Walker and J.G. Morrisett. Alias types for recursive data structures. In Types in Compilation, pp177--206, 2000.]]

Digital Library

[37]

R. Wilhelm, M. Sagiv, and T. Reps. Shape analysis. In Compiler Construction, pp1--17, 2000.]]

Digital Library

[38]

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

Digital Library

Cited By

Wang ZCao QTao Y(2024)Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow EmbeddingJournal of Automated Reasoning10.1007/s10817-024-09706-568:3Online publication date: 10-Aug-2024
https://doi.org/10.1007/s10817-024-09706-5
Eilers MDardinier TMüller P(2023)CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract CommutativityProceedings of the ACM on Programming Languages10.1145/35912897:PLDI(1682-1707)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591289
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
Show More Cited By

Index Terms

Separation and information hiding
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Classes and objects
        Modules / packages
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

Separation and information hiding

We investigate proof rules for information hiding, using the formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical ...
Separation and information hiding
POPL '04

We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2004

364 pages

ISBN:158113729X

DOI:10.1145/964001

General Chair:
Neil D. Jones
DIKU, University of Copenhagen
,
Program Chair:
Xavier Leroy
INRIA Rocquencourt

ACM SIGPLAN Notices Volume 39, Issue 1
POPL '04
January 2004
352 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/982962
Issue’s Table of Contents

Copyright © 2004 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL04

Sponsor:

POPL04: The 31st Annual ACM Symposium on Principles of Programming Languages

January 14 - 16, 2004

Venice, Italy

Acceptance Rates

POPL '04 Paper Acceptance Rate 29 of 176 submissions, 16%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

210
Total Citations
View Citations
1,092
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)1

Reflects downloads up to 06 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang ZCao QTao Y(2024)Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow EmbeddingJournal of Automated Reasoning10.1007/s10817-024-09706-568:3Online publication date: 10-Aug-2024
https://doi.org/10.1007/s10817-024-09706-5
Eilers MDardinier TMüller P(2023)CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract CommutativityProceedings of the ACM on Programming Languages10.1145/35912897:PLDI(1682-1707)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591289
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
Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Oortwijn WGurov DHuisman M(2020)An Abstraction Technique for Verifying Shared-Memory ConcurrencyApplied Sciences10.3390/app1011392810:11(3928)Online publication date: 5-Jun-2020
https://doi.org/10.3390/app10113928
Murali APeña LLöding CMadhusudan P(2020)A First-Order Logic with FramesProgramming Languages and Systems10.1007/978-3-030-44914-8_19(515-543)Online publication date: 27-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-44914-8_19
Oortwijn WGurov DHuisman M(2020)Practical Abstractions for Automated Verification of Shared-Memory ConcurrencyVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_19(401-425)Online publication date: 16-Jan-2020
https://dl.acm.org/doi/10.1007/978-3-030-39322-9_19
Bao YLeavens GErnst G(2018)Unifying separation logic and region logic to allow interoperabilityFormal Aspects of Computing10.1007/s00165-018-0455-530:3-4(381-441)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0455-5
Utterback RAgrawal KLee IKulkarni M(2017)Processor-Oblivious Record and ReplayACM SIGPLAN Notices10.1145/3155284.301876452:8(145-161)Online publication date: 26-Jan-2017
https://dl.acm.org/doi/10.1145/3155284.3018764
Cao QCuellar SAppel A(2017)Bringing Order to the Separation Logic JungleProgramming Languages and Systems10.1007/978-3-319-71237-6_10(190-211)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_10
Show More Cited By

View Options

Get Access

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