@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.} }

# Dynamic Logic

Author(s): | Bernhard Beckert, Vladimir Klebanov, and Steffen Schlager |
---|---|

In: | Verification of Object-Oriented Software: The KeY Approach |

Publisher: | Springer-Verlag |

Series: | LNCS 4334 |

Part: | I: Foundations |

Chapter: | 3 |

Year: | 2007 |

Pages: | 69-175 |

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.

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.