Dynamic Logic for Java
Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß
In this chapter of the KeY Book, 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.