An improved rule for while loops in deductive program verification

The performance and usability of deductive program verification systems can be greatly enhanced if specifications of programs and program parts not only consist of the usual pre-/post-condition pairs and invariants but also include additional information on which memory locations are changed by executing a program. This allows to separate the aspects of (a) which locations change and (b) how they change, state the change information in a compact way, and make the proof process more efficient. In this paper, we extend this idea from method specifications to loop invariants; and we define a proof rule for while loops that makes use of the change information associated with the loop body. It has been implemented and is successfully used in the KeY software verification system