Partial Clock Functions in ACL2
John Matthews and Daron Vroon
J Moore has discovered an elegant approach for verifying state
invariants of imperative programs without having to write a
verification condition generator (VCG) or clock function. Users need
only make assertions about selected cutpoint instructions of a
program, such as loop tests and subroutine entry and exit
points. ACL2's rewriter is then used to automatically propagate these
assertions through the intervening instructions.
We extend this methodology so that users can similarly prove
termination properties of programs via induction over the sequence of
cutpoint instructions the program executes. Just as with Moore's
methodology, there is no need to specify a VCG or program-specific clock
functions. These termination proofs can then be used to write efficient
executable program simulators in ACL2 that don't require step-counters
but are still guaranteed to terminate.