Generic Theories as Proof Strategies: A Case Study for Weakest Precondition Style Proofs
Wilfred J. Legato · 2004
This paper presents several techniques, motivated by the study of weakest preconditions, for structuring proofs about recursive functions using generic theories. The theories can be implemented on a variety of theorem provers that support introduction and instantiation of partial functions (PVS, HOL, ACL2, NQTHM). The focus here is on the Boyer-Moore (NQTHM [1,2]) and Kaufmann-Moore (ACL2 [6]) theorem provers. 2.0 Background The automated generation of weakest preconditions described in [7] introduces new recursive functions with no known properties other than their definitions. Interesting properties of these recursive functions must be established using induction, and induction is complicated by the fact that many of the required properties are for specific applications of the recursive functions. A standard means for overcoming this difficulty is to generalize the required properties, perform induction, and then instantiate the result. We illustrate this approach with the following simple example. Consider a program loop that sums the integers from 1 to n. It employs an accumulator, A that is initially set to 0, and a variable X that is initially set to n. On each iteration of the loop, X is added to A and then decreased by 1 provided it is not 0. When X is 0, control exits from the loop. Our goal is to prove that A = (n * (n + 1))/2 upon exit. We ignore for now constraints placed upon A and n due to finite precision arithmetic. The weakest precondition for the program loop is wp(A,X) = ((X> 0) ∧ wp(A + X, X- 1)) ∨ ((X ≤ 0) ^ (A = (n * (n + 1))/2)) Backing this predicate up over the loop initialization instructions replaces A by 0 and X by n, yielding wp(0,n). Since n is a variable, we must use induction to prove wp(0,n). The standard induction suggested by NQTHM and ACL2 is patterned after the recursive definition of wp, and its effectiveness relies upon both A and X being variables. ACL2 and NQTHM’s induction heuristic will generate the two cases: wp(0,0) base case n> 0 ∧ wp(0,n- 1) ⇒ wp(0,n) induction step The base case proves easily, but the induction step presents a problem. The only property available is the definition of wp. Replacing wp(0,n) by its definition yields the proof goal