Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Logic, Language, Information, and Computation

WoLLIC 2011: Logic, Language, Information and Computation pp 52–66Cite as

Hoare Logic for Higher Order Store Using Simple Semantics

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6642))

Abstract

We revisit the problem of providing a Hoare logic for higher order store programs, considered by Reus and Streicher (ICALP, 2005). In a higher order store program, the procedures/commands of the program are not fixed, but can be manipulated at runtime by the program itself; such programs provide a foundation to study language features such as reflection, dynamic loading and runtime code generation. By adapting the semantics of a proof system for a language with conventional (fixed) mutually recursive procedures, studied by von Oheimb (FSTTCS, 1999), we construct the same logic as Reus and Streicher, but using a much simpler model and avoiding unnecessary restrictions on the use of the proof rules. Furthermore our setup handles nondeterministic programs “for free”. We also explain and demonstrate with an example that, contrary to what has been stated in the literature, such a proof system does support proofs which are (in a specific sense) modular.

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.: Intensional equality ;=) for continuations. SIGPLAN Not. 31, 55–57 (1996)

    Article  Google Scholar 

  2. Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (2001)

    Article  Google Scholar 

  3. Benton, N., Hur, C.K.: Step-indexing: The good, the bad and the ugly. In: Modelling, Controlling and Reasoning About State. No. 10351 in Dagstuhl Seminar Proceedings, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2010)

    Google Scholar 

  4. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL, pp. 119–132 (2011)

    Google Scholar 

  6. Birkedal, L., Reus, B., Schwinghammer, J., Yang, H.: A simple model of separation logic for higher-order store. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 348–360. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Charlton, N., Horsfall, B., Reus, B.: Formal reasoning about runtime code update. In: Proceedings of HotSWUp (Hot Topics in Software Upgrades) (to appear, 2011)

    Google Scholar 

  8. Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS, pp. 270–279 (2005)

    Google Scholar 

  9. Landin, P.J.: The mechanical evaluation of expressions. Computer Journal 6(4), 308–320 (1964)

    Article  MATH  Google Scholar 

  10. Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI 2001 (Programming Language Design and Implementation), pp. 221–231. ACM Press, New York (2001)

    Chapter  Google Scholar 

  11. Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 103–119. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. von Oheimb, D.: Hoare logic for mutual recursion and local variables. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 168–180. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Parkinson, M.J.: Local reasoning for Java. Ph.D. thesis, University of Cambridge, Computer Laboratory (November 2005)

    Google Scholar 

  14. Pitts, A.M.: Relational properties of domains. Inf. Comput. 127(2), 66–90 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  15. Pottier, F.: Hiding local state in direct style: a higher-order anti-frame rule. In: LICS, Pittsburgh, Pennsylvania, pp. 331–340 (June 2008)

    Google Scholar 

  16. Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 575–590. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Reus, B., Streicher, T.: About Hoare logics for higher-order store. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1337–1348. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)

    Google Scholar 

  19. Richards, G., Lebresne, S., Burg, B., Vitek, J.: An analysis of the dynamic behavior of JavaScript programs. In: PLDI, pp. 1–12 (2010)

    Google Scholar 

  20. Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 440–454. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B.: A semantic foundation for hidden state. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 2–17. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Informatics, University of Sussex, UK

    Nathaniel Charlton

Authors
  1. Nathaniel Charlton
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Steklov Mathematical Institute, Gubkina 8, 117966, Moscow, Russia

    Lev D. Beklemishev

  2. Centro de Informática, Universidade Federal de Pernambuco, Avenida Prof Luis Freire s/n, Cidade Universitária, 50740-540, Recife, PE, Brazil

    Ruy de Queiroz

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Charlton, N. (2011). Hoare Logic for Higher Order Store Using Simple Semantics. In: Beklemishev, L.D., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2011. Lecture Notes in Computer Science(), vol 6642. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20920-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20920-8_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20919-2

  • Online ISBN: 978-3-642-20920-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation