In the previous chapter, we have introduced a variant of
classical predicate logic that has a rich type system and
a sequent calculus for that logic. This predicate logic
can easily be used to describe and reason about data
structures, the relations between objects, the values of
variables—in short: about the states of (Java) programs.

Now, we extend the logic and the calculus such that we
can describe and reason about the behaviour of programs,
which requires to consider not just one but several
program states.

As a trivial example, consider the Java statement
x++;. We want to be able to express that this
statement, when started in a state where x is zero, terminates in
a state where x is one.

@incollection{BeckertKlebanovSchlager07,
author = {Bernhard Beckert and Vladimir Klebanov and Steffen Schlager},
title = {Dynamic Logic},
chapter = {3},
part = {I: Foundations},
pages = {69--175},
editor = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
booktitle = {Verification of Object-Oriented Software: The {\KeY} Approach},
year = {2007},
series = {LNCS 4334},
publisher = {Springer-Verlag},
doi = {10.1007/978-3-540-69061-0_3},
abstract = {In the previous chapter, we have introduced a variant of
classical predicate logic that has a rich type system and
a sequent calculus for that logic. This predicate logic
can easily be used to describe and reason about data
structures, the relations between objects, the values of
variables—in short: about the states of (Java) programs.
\newline
Now, we extend the logic and the calculus such that we
can describe and reason about the behaviour of programs,
which requires to consider not just one but several
program states.
\newline
As a trivial example, consider the Java statement
x++;. We want to be able to express that this
statement, when started in a state where x is zero, terminates in
a state where x is one.}
}