An Improved Rule for While Loops in Deductive Program Verification
Bernhard Beckert, Steffen Schlager, Peter H. Schmitt
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.