Dynamic Logic for Java

Book Chapter

Author(s):Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Publisher:Springer
Series:LNCS 10001
Chapter:3
Year:2016
Pages:49-106
URL:http://dx.doi.org/10.1007/978-3-319-49812-6_3
DOI:10.1007/978-3-319-49812-6_3

Abstract

In this chapter, we introduce an instance of dynamic logic, called JavaDL, that allows us to reason about Java programs. Dynamic logic extends first-order logic and makes it possible to consider several program states in a single formula. Its principle is the formulation of assertions about program behavior by integrating programs and formulas within a single language. We present a sequent calculus for JavaDL, which is used in the KeY System for verifying Java programs. Deduction in this calculus is based on symbolic program execution and simple program transformations and is, thus, close to a programmer's understanding of Java. Besides rules for symbolic execution, the calculus contains rules for program abstraction and modularization, including invariant rules for reasoning about loops and rules that replace a method invocation by the method's contract.

BibTeX

@incollection{BeckertKlebanovWeiss2016,
  author       = {Bernhard Beckert and Vladimir Klebanov and Benjamin
                  Wei{\ss}},
  title        = {{D}ynamic {L}ogic for {J}ava},
  booktitle    = {Deductive Software Verification - The KeY Book: From Theory to
                  Practice},
  publisher    = {Springer},
  series       = {LNCS 10001},
  pages        = {49--106},
  chapter      = {3},
  url          = {http://dx.doi.org/10.1007/978-3-319-49812-6_3},
  doi          = {10.1007/978-3-319-49812-6_3},
  year         = {2016},
  month        = dec,
  abstract     = {In this chapter, we introduce an instance of dynamic logic,
                  called JavaDL, that allows us to reason about Java programs.
                  Dynamic logic extends first-order logic and makes it possible
                  to consider several program states in a single formula. Its
                  principle is the formulation of assertions about program
                  behavior by integrating programs and formulas within a single
                  language. We present a sequent calculus for JavaDL, which is
                  used in the \KeY System for verifying Java programs. Deduction
                  in this calculus is based on symbolic program execution and
                  simple program transformations and is, thus, close to a
                  programmer's understanding of Java. Besides rules for symbolic
                  execution, the calculus contains rules for program abstraction
                  and modularization, including invariant rules for reasoning
                  about loops and rules that replace a method invocation by the
                  method's contract.}
}