Dynamic Logic with Non-rigid Functions:
A Basis for Object-oriented Program Verification

Bernhard Beckert and Andre Platzer


We introduce a dynamic logic that is enriched by non-rigid functions,
i.e., functions that may change their value from state to state
(during program execution), and we present a (relatively) complete
sequent calculus for this logic.In conjunction with dynamically typed
object enumerators, non-rigid functions allow to embed notions of
object-orientation in dynamic logic, thereby forming a basis for
verification of object-oriented programs.  A semantical generalisation
of substitutions, called state update, which we add to the logic,
constitutes the central technical device for dealing with object
aliasing during function modification.  With these few extensions, our
dynamic logic captures the essential aspects of the complex
verification system KeY and, hence, constitutes a foundation for
object-oriented verification with the principles of reasoning that
underly the successful KeY case studies.