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.
@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},
part = {I: Foundations},
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.}
}