Program Verification Using Change Information
Bernhard Beckert and Peter H. Schmitt
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, also information is 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.
