*Result*: Dynamic Logic.
*Further Information*
*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. [ABSTRACT FROM AUTHOR]
Copyright of Verification of Object-Oriented Software. The KeY Approach is the property of Springer eBooks and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)*