First International Conference on Software Engineering and Formal Methods (SEFM'03) Program Verification Using Change Information Brisbane, Australia September 22-September 27 ISBN: 0-7695-1949-0
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.
Citation:
Bernhard Beckert, Peter H. Schmitt, "Program Verification Using Change Information," sefm, pp.91, First International Conference on Software Engineering and Formal Methods (SEFM'03), 2003 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||