Program verification using change information

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 modi... View More