[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

False Failure: Creating Failure Models for Separation Logic

  • Conference paper
  • First Online:
Relational and Algebraic Methods in Computer Science (RAMiCS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11194))

Abstract

Separation logic, an extension of Floyd-Hoare logic, finds countless applications in areas of program verification, but does not allow forward reasoning in the setting of total or generalised correctness. To support forward reasoning, separation logic needs to be equiped with a failure element. We present several ways on how to add such an element. We show that none of the ‘obvious’ extensions preserve all the algebraic properties desired. We develop more complicated models, satisfying the desired properties, and discuss their use for forward reasoning.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    We introduce its syntax implicitly; see e.g. [30] for an explicit definition.

  2. 2.

    Often one assumes .

  3. 3.

    We omit straightforward proofs; most of them are available online (see Sect. 6).

References

  1. Bannister, C., Höfner, P., Klein, G.: Backwards and forwards with separation logic. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 68–87. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94821-8_5

    Chapter  Google Scholar 

  2. Birkhoff, G.: Lattice Theory, Colloquium Publications, vol. XXV. Annals of Mathematics Studies, 3rd edn. (1967)

    Google Scholar 

  3. Brotherston, J., Calcagno, C.: Classical BI: its semantics and proof theory. Log. Methods Comput. Sci. 6(3) (2010)

    Google Scholar 

  4. Brotherston, J., Villard, J.: Sub-classical Boolean bunched logics and the meaning of par. In: Kreutzer, S. (ed.) Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 41, pp. 325–342. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  5. Campbell, H.E.: The Structure of Arithmetic. Appleton-Century-Crofts, New York (1970)

    Google Scholar 

  6. Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)

    MATH  Google Scholar 

  7. Dang, H.H.: Algebraic calculi for separation logic. Ph.D. thesis, University of Augsburg, Germany (2014)

    Google Scholar 

  8. Dang, H.H., Höfner, P., Möller, B.: Algebraic separation logic. J. Logic Algebraic Program. 80(6), 221–247 (2011)

    Article  Google Scholar 

  9. Desharnais, J., Möller, B.: Non-associative Kleene algebra and temporal logics. In: Höfner, P., Pous, D., Struth, G. (eds.) RAMiCS 2017. LNCS, vol. 10226, pp. 93–108. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57418-9_6

    Chapter  MATH  Google Scholar 

  10. Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  11. Dongol, B., Hayes, I.J., Struth, G.: Relational convolution, generalised modalities and incidence algebras. arXiv:1702.04603 (2017)

  12. Dunn, J.: Star and perp. Philos. Perspect. 7, 331–357 (1993)

    Article  Google Scholar 

  13. Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19–32 (1967)

    Article  MathSciNet  Google Scholar 

  14. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969)

    Article  Google Scholar 

  15. Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Logic Algebraic Program. 80(6), 266–296 (2011)

    Article  MathSciNet  Google Scholar 

  16. Höfner, P., Möller, B.: An algebra of hybrid systems. J. Logic Algebraic Program. 78, 74–97 (2009)

    Article  MathSciNet  Google Scholar 

  17. Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. SIGPLAN Not. 36, 14–26 (2001)

    Article  Google Scholar 

  18. Jacobs, D., Gries, D.: General correctness: a unification of partial and total correctness. Acta Inf. 22(1), 67–83 (1985)

    Article  MathSciNet  Google Scholar 

  19. Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Logic 1(1), 60–76 (2000)

    Article  MathSciNet  Google Scholar 

  20. Mares, E.: Relevance logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Spring 2014 edn. (2014)

    Google Scholar 

  21. Möller, B.: Residuals and detachments. Technical report 2005–20, Institut für Informatik, Universität Augsburg (2005)

    Google Scholar 

  22. Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theor. Comput. Sci. 351(2), 221–239 (2006)

    Article  MathSciNet  Google Scholar 

  23. Möller, B., Struth, G.: wp Is wlp. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 200–211. Springer, Heidelberg (2006). https://doi.org/10.1007/11734673_16

    Chapter  Google Scholar 

  24. Mulvey, C.:&. In: Second Topology Conference (1986). Rendiconti del Circolo Matematico di Palermo 2(12), 99–104

    Google Scholar 

  25. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  26. O’Hearn, P.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 271–307 (2007)

    Article  MathSciNet  Google Scholar 

  27. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  28. Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, Boston (2002)

    Book  Google Scholar 

  29. Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, pp. 303–321. Palgrave (2000)

    Google Scholar 

  30. Reynolds, J.C.: An introduction to separation logic. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 22, pp. 285–310. IOS Press (2009)

    Google Scholar 

  31. Rosenthal, K.: Quantales and Their Applications. Pitman Research Notes in Mathematics Series, vol. 234 (1990)

    Google Scholar 

  32. Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_18

    Chapter  Google Scholar 

Download references

Acknowledgement

We are grateful to Gerwin Klein and Bernhard Möller for fruitful discussions and inspiring ideas. We also thank the anonymous referees for their valuable feedback.

Author information

Authors and Affiliations

  1. Data61, CSIRO, Sydney, Australia

    Callum Bannister & Peter Höfner

  2. Computer Science and Engineering, University of New South Wales, Sydney, Australia

    Callum Bannister & Peter Höfner

Authors
  1. Callum Bannister
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Höfner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Höfner .

Editor information

Editors and Affiliations

  1. Université Laval, Québec, QC, Canada

    Jules Desharnais

  2. University of Canterbury, Christchurch, New Zealand

    Walter Guttmann

  3. Open Universiteit, Heerlen, The Netherlands

    Stef Joosten

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bannister, C., Höfner, P. (2018). False Failure: Creating Failure Models for Separation Logic. In: Desharnais, J., Guttmann, W., Joosten, S. (eds) Relational and Algebraic Methods in Computer Science. RAMiCS 2018. Lecture Notes in Computer Science(), vol 11194. Springer, Cham. https://doi.org/10.1007/978-3-030-02149-8_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02149-8_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02148-1

  • Online ISBN: 978-3-030-02149-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics