An Object-oriented Dynamic Logic with Updates

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 work captures the base calculus implemented in the KeY System, which is a deductive verification system for Java programs.

Keywords: dynamic logic, sequent calculus, program logic, software verification, logical foundations of programming languages, object-orientation

Contents

• PS-Version of this document
• PDF-Version of this document
• Slides from IJCAR 2006

[BP06]

Bernhard Beckert and André Platzer. Dynamic logic with non-rigid functions: A basis for object-oriented program verification. In U. Furbach and N. Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of LNCS, pages 266-280. Springer, 2006. (c) Springer Verlag
[pdf | slides]

[Pla04b]

André Platzer (2004). An Object-oriented Dynamic Logic with Updates. Master's Thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, September 2004.
[pdf]

BibTeX

@mastersthesis{Platzer_2004b,
  author = {Platzer, Andr\'e},
  title  = {An Object-oriented Dynamic Logic with Updates},
  school = {University of Karlsruhe, Department of Computer Science.
            Institute for Logic, Complexity and Deduction Systems},
  year   = {2004},
  month  = {September}
}