Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Dynamic Logic with Non-rigid Functions

A Basis for Object-Oriented Program Verification

  • Conference paper
Automated Reasoning (IJCAR 2006)

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

Included in the following conference series:

  • 1119 Accesses

Abstract

We introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a (relatively) complete sequent calculus for this logic. In conjunction with dynamically typed object enumerators, non-rigid functions allow to embed notions of object-orientation in dynamic logic, thereby forming a basis for verification of object-oriented programs. A semantical generalisation of substitutions, called state update, which we add to the logic, constitutes the central technical device for dealing with object aliasing during function modification. With these few extensions, our dynamic logic captures the essential aspects of the complex verification system KeY and, hence, constitutes a foundation for object-oriented verification with the principles of reasoning that underly the successful KeY case studies.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  2. Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4, 32–54 (2005)

    Article  Google Scholar 

  3. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe,, et al. (eds.) [4] (2004)

    Google Scholar 

  4. Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.): CASSIS 2004. LNCS, vol. 3362. Springer, Heidelberg (2005)

    Google Scholar 

  5. Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6–24. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Beckert, B., Mostowski, W.: A program logic for handling Java Card’s transaction mechanism. In: Pezzé, M. (ed.) ETAPS 2003 and FASE 2003. LNCS, vol. 2621, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 626–641. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Beckert, B., Schlager, S.: Software verification with integrated data type refinement for integer arithmetic. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 207–226. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Cok, D.R., Kiniry, J.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe,, et al. (eds.) [4], pp. 108–128 (2004)

    Google Scholar 

  10. Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Kluwer Academic Publishers, Dordrecht (1999)

    Google Scholar 

  11. Harel, D.: First-Order Dynamic Logic. Springer, New York (1979)

    MATH  Google Scholar 

  12. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)

    Article  Google Scholar 

  13. Jacobs, B., Poll, E.: A logic for the Java modeling language JML. In: Hussmann, H. (ed.) ETAPS 2001 and FASE 2001. LNCS, vol. 2029, pp. 284–299. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Miller, R., Tripathi, A.: Issues with exception handling in object-oriented systems. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 85–103. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  15. Mostowski, W.: Formal Development of Safe and Secure Java Card Applets. PhD thesis, Chalmers University of Technology, Göteborg, Sweden (February 2005)

    Google Scholar 

  16. Nipkow, T.: Jinja: Towards a comprehensive formal semantics for a Java-like language. In: Proc. Marktoberdorf Summer School (2003)

    Google Scholar 

  17. Pierik, C., de Boer, F.S.: A syntax-directed Hoare logic for object-oriented programming concepts. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 64–78. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Platzer, A.: An object-oriented dynamic logic with updates. Master’s thesis, University of Karlsruhe (September 2004), available at www.key-project.org

  19. Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential Java. In: Swierstra, D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol. 1576, Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  20. Stärk, R., Nanchen, S.: A logic for abstract state machines. J. UCS 7(11) (2001)

    Google Scholar 

  21. van den Berg, J., Huisman, M., Jacobs, B., Poll, E.: A type-theoretic memory model for verification of sequential Java programs. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 1–21. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. von Oheimb, D., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 89–105. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Koblenz-Landau,  

    Bernhard Beckert

  2. Department of Computing Science, University of Oldenburg,  

    André Platzer

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. André Platzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Artificial Intelligence Research Group, University of Koblenz-Landau, Universitätsstr. 1, 56070, Koblenz

    Ulrich Furbach

  2. SRI International, MS EL256,, 333 Ravenswood Avenue, 94025-3493, Menlo Park, CA, USA

    Natarajan Shankar

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beckert, B., Platzer, A. (2006). Dynamic Logic with Non-rigid Functions. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814771_23

Download citation

  • DOI: https://doi.org/10.1007/11814771_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37187-8

  • Online ISBN: 978-3-540-37188-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation