Logic and Formal Methods

Verification of Modifies Clauses in Dynamic Logic with Non-rigid Functions

  • Author(s):

    Christian Engel
    Andreas Roth
    Peter H. Schmitt
    Benjamin Weiß

  • Source:

    Technical Report 2009-9, Department of Computer Science, University of Karlsruhe, 2009

  • For modular verification of object-oriented programs, it is necessary to constrain what may be changed by a method in addition to how it is changed. Doing so with the classical means of pre- and postconditions is cumbersome, and even impossible if the program context is not entirely known. Therefore, specifications make use of an additional construct, known as a "frame property" or "modifies clause", which lists the memory locations that can at most be modified. Deductively verifying the correctness of such modifies clauses is difficult because the focus is on those locations which are not mentioned in the modifies clause. We present a novel approach to encode the correctness of modifies clauses as compact and readable proof obligations in dynamic logic. These proof obligations can be discharged efficiently with existing dynamic logic calculi, such as the one implemented in the KeY verification system. Additionally, we describe how a variant of our technique can be used for the verification of loops.


author = {Christian Engel and Andreas Roth and Peter H. Schmitt and Benjamin Wei{\ss}},
title = {Verification of Modifies Clauses in Dynamic Logic with Non-rigid Functions},
number = {2009-9},
institution = {Department of Computer Science, University of Karlsruhe},
year = {2009}