Skip to main content
SpringerLink
Log in

Separation Logic Contracts for a Java-Like Language with Fork/Join

  • Conference paper
Algebraic Methodology and Software Technology (AMAST 2008)

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

Abstract

We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional permissions with abstract predicates. As an example, we present a separation logic contract for iterators that prevents data races and concurrent modifications. Our program logic is presented in an algorithmic style: we avoid structural rules for Hoare triples and formalize logical reasoning about typed heaps by natural deduction rules and a set of sound axioms. We show that verified programs satisfy the following properties: data race freedom, absence of null-dereferences and partial correctness.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6) (2004)

    Google Scholar 

  2. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: Formal Methods for Components and Objects (2005)

    Google Scholar 

  3. Bierhoff, K., Aldrich, J.: Modular typestate verification of aliased objects. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (2007)

    Google Scholar 

  4. Bornat, R., O’Hearn, P., Calcagno, C., Parkinson, M.: Permission accounting in separation logic. In: Principles of Programming Languages. ACM Press, New York (2005)

    Google Scholar 

  5. Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Boyland, J.: Semantics of fractional permissions with nesting. Technical report, University of Wisconsin at Milwaukee (2007)

    Google Scholar 

  7. Boyland, J., Retert, W.: Connecting effects and uniqueness with adoption. In: Principles of Programming Languages (2005)

    Google Scholar 

  8. Boyland, J., Retert, W., Zhao, Y.: Iterators can be independent ”from” their collections. In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (2007)

    Google Scholar 

  9. Chin, W., David, C., Nguyen, H., Qin, S.: Enhancing modular OO verification with separation logic. In: Principles of Programming Languages (2008)

    Google Scholar 

  10. Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Principles of Programming Languages (1999)

    Google Scholar 

  11. DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Programming Languages Design and Implementation (2001)

    Google Scholar 

  12. DeLine, R., Fähndrich, M.: Typestates for objects. In: European Conference on Object-Oriented Programming (2004)

    Google Scholar 

  13. Girard, J.-Y.: Linear logic: Its syntax and semantics. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. Cambridge University Press, Cambridge (1995)

    Google Scholar 

  14. Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Asian Programming Languages and Systems Symposium (2007)

    Google Scholar 

  15. Haack, C., Hurlin, C.: Resource usage protocols for iterators, http://www.cs.ru.nl/~chaack/papers/iterators.pdf

  16. Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork/join. Technical Report 6430, INRIA (2008)

    Google Scholar 

  17. Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3) (2001)

    Google Scholar 

  18. Ishtiaq, S., O’Hearn, P.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages (2001)

    Google Scholar 

  19. Krishnaswami, G.: Reasoning about iterators with separation logic. In: Specification and Verification of Component-Based Systems (2006)

    Google Scholar 

  20. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Software Engineering Notes 31(3) (2006)

    Google Scholar 

  21. Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (1998)

    Google Scholar 

  22. O’Hearn, P.: Resources, concurrency and local reasoning. Theor. Comp. Science 375(1–3) (2007)

    Google Scholar 

  23. O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2) (1999)

    Google Scholar 

  24. O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Principles of Programming Languages, Venice, Italy. ACM Press, New York (2004)

    Google Scholar 

  25. Parkinson, M.: Local reasoning for Java. Technical Report UCAM-CL-TR-654, University of Cambridge (2005)

    Google Scholar 

  26. Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Principles of Programming Languages (2005)

    Google Scholar 

  27. Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Principles of Programming Languages (2008)

    Google Scholar 

  28. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark. IEEE Press, Los Alamitos (2002)

    Google Scholar 

  29. Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol. 1782. Springer, Heidelberg (2000)

    Google Scholar 

  30. Wadler, P.: A taste of linear logic. In: Mathematical Foundations of Computer Science (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Radboud Universiteit Nijmegen, The Netherlands

    Christian Haack

  2. INRIA Sophia Antipolis - Méditerranée, France

    Clément Hurlin

Authors
  1. Christian Haack
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Clément Hurlin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

José Meseguer Grigore Roşu

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Haack, C., Hurlin, C. (2008). Separation Logic Contracts for a Java-Like Language with Fork/Join. In: Meseguer, J., Roşu, G. (eds) Algebraic Methodology and Software Technology. AMAST 2008. Lecture Notes in Computer Science, vol 5140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79980-1_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-79980-1_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-79979-5

  • Online ISBN: 978-3-540-79980-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation