Skip to main content
SpringerLink
Log in
Book cover

Asian Symposium on Programming Languages and Systems

APLAS 2012: Programming Languages and Systems pp 332–349Cite as

A Case for Behavior-Preserving Actions in Separation Logic

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7705))

Abstract

Separation Logic is a widely-used tool that allows for local reasoning about imperative programs with pointers. A straightforward definition of this ”local reasoning” is that, whenever a program runs safely on some state, adding more state would have no effect on the program’s behavior. However, for a mix of technical and historical reasons, local reasoning is defined in a more subtle way, allowing a program to lose some behaviors when extra state is added. In this paper, we propose strengthening local reasoning to match the straightforward definition mentioned above. We argue that such a strengthening does not have any negative effect on the usability of Separation Logic, and we present four examples that illustrate how this strengthening simplifies some of the metatheoretical reasoning regarding Separation Logic. In one example, our change even results in a more powerful metatheory.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Appel, A.W., Blazy, S.: Separation Logic for Small-Step Cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: Proc. 20th IEEE Symp. on Logic in Computer Science, pp. 260–269 (2005)

    Google Scholar 

  3. Brookes, S.: A Semantics for Concurrent Separation Logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16–34. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 366–378 (July 2007)

    Google Scholar 

  5. Costanzo, D., Shao, Z.: A case for behavior-preserving actions in separation logic. Technical report, Dept. of Computer Science, Yale University, New Haven, CT (June 2012), http://flint.cs.yale.edu/publications/bpsl.html

  6. Filipovic, I., O’Hearn, P.W., Torp-Smith, N., Yang, H.: Blaming the client: on data refinement in the presence of pointers. Formal Asp. Comput. 22(5), 547–583 (2010)

    Article  MATH  Google Scholar 

  7. Huet, G., Paulin-Mohring, C., et al.: The Coq proof assistant reference manual. The Coq release v6.3.1 (May 2000)

    Google Scholar 

  8. Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM Symposium on Principles of Programming Languages, pp. 14–26 (January 2001)

    Google Scholar 

  9. Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice Hall (1988)

    Google Scholar 

  10. O’Hearn, P.W.: Resources, Concurrency and Local Reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49–67. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. ACM Trans. Program. Lang. Syst. 31(3), 1–50 (2009)

    Article  Google Scholar 

  12. Raza, M., Gardner, P.: Footprints in local reasoning. Journal of Logical Methods in Computer Science 5(2) (2009)

    Google Scholar 

  13. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symp. on Logic in Computer Science, pp. 55–74 (July 2002)

    Google Scholar 

  14. Yang, H.: Relational separation logic. Theor. Comput. Sci. 375(1-3), 308–334 (2007)

    Article  MATH  Google Scholar 

  15. Yang, H., O’Hearn, P.W.: A Semantic Basis for Local Reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Yale University, USA

    David Costanzo & Zhong Shao

Authors
  1. David Costanzo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhong Shao
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of California, San Diego, 9500 Gilman Drive, 92092-6237, La Jolla, CA, USA

    Ranjit Jhala

  2. Graduate School of Informatics, Kyoto University, Yoshida-Honmachi, 606-8501, Sakyo-ku, Kyoto, Japan

    Atsushi Igarashi

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Costanzo, D., Shao, Z. (2012). A Case for Behavior-Preserving Actions in Separation Logic. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-35182-2_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-35181-5

  • Online ISBN: 978-3-642-35182-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation