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

article

Separation logic and abstraction

Authors:

Matthew Parkinson,

Gavin BiermanAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 247 - 258

https://doi.org/10.1145/1047659.1040326

Published: 12 January 2005 Publication History

Abstract

In this paper we address the problem of writing specifications for programs that use various forms of modularity, including procedures and Java-like classes. We build on the formalism of separation logic and introduce the new notion of an abstract predicate and, more generally, abstract predicate families. This provides a flexible mechanism for reasoning about the different forms of abstraction found in modern programming languages, such as abstract datatypes and objects. As well as demonstrating the soundness of our proof system, we illustrate its utility with a series of examples.

References

[1]

M. Abadi and L. Cardelli. A theory of objects. Springer, 1996.]]

Digital Library

[2]

M. Barnett, R. DeLine, M. Fähndrich, K.R.M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 2004.]]

[3]

G.M. Bierman and M.J. Parkinson. Effects and effect inference for a core Java calculus. In Proceedings of WOOD, volume 82 of ENTCS, 2004.]]

[4]

L. Birkedal, N. Torp-Smith, and J.C. Reynolds. Local reasoning about a copying garbage collector. In Proceedings of POPL, 2004.]]

Digital Library

[5]

R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permissions accounting in separation logic. Proceedings of POPL, 2005.]]

Digital Library

[6]

D. Clarke and S. Drossopolou. Ownership, encapsulation and the disjointness of type and effect. In Proceedings of OOPSLA, 2002.]]

Digital Library

[7]

S. Drossopoulou and M. Smith. Cheaper reasoning with ownership types. In Proceedings of IWACO, 2003.]]

[8]

J. Ellis and L. Ho. JDBC 3.0 specification, 2001. http://java.sun.com/products/jdbc/download.html.]]

[9]

M. Grand. Patterns in Java, volume 1. Wiley, second edition, 2002.]]

[10]

J. Guttag. The Specification and Applications to Programming of Abstract Data Types. PhD thesis, Dept. of Computer Science, University of Toronto, 1975.]]

Digital Library

[11]

C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.]]

Digital Library

[12]

B. W. Kernighan and D. M. Ritchie. The C Programming Language, Second Edition. Prentice-Hall, 1988.]]

Digital Library

[13]

J. Lamping. Typing the specialization interface. In Proceedings of OOPSLA, 1993.]]

Digital Library

[14]

K.R.M. Leino. Data groups: Specifying the modification of extended state. In Proceedings of OOPSLA, 1998.]]

Digital Library

[15]

K.R.M. Leino and G. Nelson. Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems, 24:491--553, September 2002.]]

Digital Library

[16]

B. Liskov and S.N. Zilles. Programming with abstract data types. In Proceedings of Symposium on Very High Level Programming Languages, 1974.]]

Digital Library

[17]

B.H. Liskov and J.M. Wing. A behavioral notion of subtyping. ACM TOPLAS, 16(6):1811--1841, 1994.]]

Digital Library

[18]

R. Middelkoop, K. Huizing, and R. Kuiper. A Separation Logic Proof System for a Class-based Language. In Proceedings of LRPP, 2004.]]

[19]

I. Mijajlović and N. Torp-Smith. Refinement in a separation context. In Proceedings of FSTTCS, 2004.]]

Digital Library

[20]

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

Digital Library

[21]

P.W. O'Hearn. Resources, concurrency and local reasoning. Invited paper, inphProceedings of CONCUR, 2004.]]

[22]

P.W. O'Hearn, H.Yang, and J.C. Reynolds. Separation and information hiding. In Proceedings of POPL, 2004.]]

Digital Library

[23]

P.W. O'Hearn, J.C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In Proceedings of CSL, 2001.]]

Digital Library

[24]

D. Oheimb and T. Nipkow. Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In Formal Methods Europe, 2002.]]

Digital Library

[25]

D.L. Parnas. The secret history of information hiding. In Software Pioneers: Contributions to Software Engineering. Springer, 2002.]]

Digital Library

[26]

C. Pierik and F.S. de Boer. A syntax-directed Hoare logic for object-oriented programming concepts. In Formal Methods for Open Object-Based Distributed Systems, 2003.]]

[27]

A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In Proceedings of ESOP, 1999.]]

Digital Library

[28]

U.S. Reddy. Objects and classes in Algol-like languages. Information and Computation, 2002.]]

Digital Library

[29]

J.C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of LICS, 2002.]]

Digital Library

[30]

R. Stata. Modularity in the presence of subclassing. Technical Report 145, Digital Equipment Corporation Systems Research Center, April 1997.]]

Digital Library

[31]

H. Yang. Local reasoning for stateful programs. PhD thesis, University of Illinois, July 2001.]]

Digital Library

Cited By

Zimmerman CDiVincenzo JAldrich J(2024)Sound Gradual Verification with Symbolic ExecutionProceedings of the ACM on Programming Languages10.1145/36329278:POPL(2547-2576)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632927
Eilers MSchwerhoff MMüller P(2024)Verification Algorithms for Automated Separation Logic VerifiersComputer Aided Verification10.1007/978-3-031-65627-9_18(362-386)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_18
Wolf FSchwerhoff MMüller P(2023)Concise outlines for a complex logic: a proof outline checker for TaDAFormal Methods in System Design10.1007/s10703-023-00427-w61:1(110-136)Online publication date: 31-Jul-2023
https://doi.org/10.1007/s10703-023-00427-w
Show More Cited By

Index Terms

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

Recommendations

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

In this paper we address the problem of writing specifications for programs that use various forms of modularity, including procedures and Java-like classes. We build on the formalism of separation logic and introduce the new notion of an abstract ...
Separation logic, abstraction and inheritance
POPL '08

Inheritance is a fundamental concept in object-oriented programming, allowing new classes to be defined in terms of old classes. When used with care, inheritance is an essential tool for object-oriented programmers. Thus, for those interested in ...
A relational modal logic for higher-order stateful ADTs
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

The method of logical relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

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

Copyright © 2005 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: 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

263
Total Citations
View Citations
1,461
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)5

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zimmerman CDiVincenzo JAldrich J(2024)Sound Gradual Verification with Symbolic ExecutionProceedings of the ACM on Programming Languages10.1145/36329278:POPL(2547-2576)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632927
Eilers MSchwerhoff MMüller P(2024)Verification Algorithms for Automated Separation Logic VerifiersComputer Aided Verification10.1007/978-3-031-65627-9_18(362-386)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_18
Wolf FSchwerhoff MMüller P(2023)Concise outlines for a complex logic: a proof outline checker for TaDAFormal Methods in System Design10.1007/s10703-023-00427-w61:1(110-136)Online publication date: 31-Jul-2023
https://doi.org/10.1007/s10703-023-00427-w
Beringer LAppel A(2021)Abstraction and subsumption in modular verification of C programsFormal Methods in System Design10.1007/s10703-020-00353-158:1-2(322-345)Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s10703-020-00353-1
Wolf FSchwerhoff MMüller P(2021)Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDAFormal Methods10.1007/978-3-030-90870-6_22(407-426)Online publication date: 10-Nov-2021
https://doi.org/10.1007/978-3-030-90870-6_22
Wolf FArquint LClochard MOortwijn WPereira JMüller P(2021)Gobra: Modular Specification and Verification of Go ProgramsComputer Aided Verification10.1007/978-3-030-81685-8_17(367-379)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_17
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
Krishna SSummers AWies T(2020)Local Reasoning for Global Graph PropertiesProgramming Languages and Systems10.1007/978-3-030-44914-8_12(308-335)Online publication date: 27-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-44914-8_12
Ter-Gabrielyan ASummers AMüller P(2019)Modular verification of heap reachability properties in separation logicProceedings of the ACM on Programming Languages10.1145/33605473:OOPSLA(1-28)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360547
Sadiq ALi YLing S(2019)A survey on the use of access permission-based specifications for program verificationJournal of Systems and Software10.1016/j.jss.2019.110450(110450)Online publication date: Oct-2019
https://doi.org/10.1016/j.jss.2019.110450
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