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.