Program verification using change information

Abstract

We propose an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, information is also provided on which parts of the state are not changed by running the program. This is done in the form of modifier sets. We present a precise semantics of modifier sets and theorems on how to use them in program-correctness proofs. This technique has been implemented as part of the KeY system.