Dynamic Logic

Book Chapter

Author(s):Bernhard Beckert, Vladimir Klebanov, and Steffen Schlager
In:Verification of Object-Oriented Software: The KeY Approach
Publisher:Springer-Verlag
Series:LNCS 4334
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.

BibTeX

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