26
S. Chakraborty et al.
1)} P N −1 {ψ(N − 1)} and {ψ(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N )}. The first triple
follows from the inductive hypothesis. Proving the second triple may require
strengthening the pre-condition, say by a formula Pre(N − 1), in general. Recalling that we are in the inductive step of mathematical induction, we formulate the new proof sub-goal in such a case as {(ψ(N − 1) ∧ Pre(N − 1)) ∧
∂ϕ(N )} ∂P N {ψ(N ) ∧ Pre(N )}. While this is somewhat reminiscent of loop invariants, observe that Pre(N ) is not really a loop-specific invariant. Instead, it
is analogous to computing an invariant for the entire program, possibly containing multiple loops. Specifically, the above process strengthens both the preand post-condition of {ψ(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N )} simultaneously using
Pre(N − 1) and Pre(N ), respectively. The strengthened post-condition of the resulting Hoare triple may, in turn, require a new pre-condition Pre
(N − 1) to be
satisfied. This process of strengthening the pre- and post-conditions of the Hoare
triple involving ∂P N can be iterated until a fix-point is reached, i.e. no further
pre-conditions are needed for the parameterized Hoare triple to hold. While the
fix-point was quickly reached for all benchmarks we experimented with, we also
discuss how to handle cases where the above process may not converge easily.
Note that since we effectively strengthen the pre-condition of the Hoare triple in
the inductive step, for the overall induction to go through, it is also necessary to
check that the strengthened assertions hold at the end of each base case check.
The technique described above is called full-program induction, and the following
theorem guarantees its soundness.
Theorem 1. Given {ϕ(N )} P N {ψ(N )}, suppose the following are true:
1. For N > 1, {ϕ(N )} P N −1 ; ∂P N {ψ(N )} holds iff {ϕ(N )} P N {ψ(N )} holds.
2. For N > 1, there exists a formula ∂ϕ(N ) such that (a) ∂ϕ(N ) doesn’t refer
to any program variable or array element modified in P N −1 , and (b) ϕ(N ) →
ϕ(N − 1) ∧ ∂ϕ(N ).
3. There exists an integer M ≥ 1 and a parameterized formula Pre(M ) such
that (a) {ϕ(N )} P N {ψ(N )} holds for 0 < N ≤ M , (b) {ϕ(M )} P M {ψ(M )∧
Pre(M )} holds, and (c) {ψ(N − 1) ∧ Pre(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N ) ∧
Pre(N )} holds for N > M.
Then {ϕ N } P N {ψ N } holds for all N ≥ 1.
Proof. For 0 < N ≤ M , condition 3(a) ensures that {ϕ(N )} P N {ψ(N )} holds.
For N > M, note that by virtue of condition 1 and 2(b), {ϕ(N )} P N {ψ(N )}
holds if {ϕ(N − 1) ∧ ∂ϕ(N )} P N −1 ; ∂P N {ψ(N ) ∧ Pre(N )} holds. With ψ(N −
1) ∧ Pre(N − 1) as a mid-condition, and by virtue of condition 2(a), the latter
Hoare triple holds for N > M if {ϕ(M )} P M {ψ(M ) ∧ Pre(M )} holds and
{ψ(N − 1) ∧ Pre(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N ) ∧ Pre(N )} holds for all N > M.
Both these triples are seen to hold by virtue of conditions 3(b) and (c).
3 Algorithms for Full-program Induction
We now discuss the full-program induction algorithm, focusing on generation
of three crucial components: difference program ∂P N , difference pre-condition
∂ϕ(N ), and the formula Pre(N ) for strengthening pre- and post-conditions.
S. Chakraborty et al.
1)} P N −1 {ψ(N − 1)} and {ψ(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N )}. The first triple
follows from the inductive hypothesis. Proving the second triple may require
strengthening the pre-condition, say by a formula Pre(N − 1), in general. Recalling that we are in the inductive step of mathematical induction, we formulate the new proof sub-goal in such a case as {(ψ(N − 1) ∧ Pre(N − 1)) ∧
∂ϕ(N )} ∂P N {ψ(N ) ∧ Pre(N )}. While this is somewhat reminiscent of loop invariants, observe that Pre(N ) is not really a loop-specific invariant. Instead, it
is analogous to computing an invariant for the entire program, possibly containing multiple loops. Specifically, the above process strengthens both the preand post-condition of {ψ(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N )} simultaneously using
Pre(N − 1) and Pre(N ), respectively. The strengthened post-condition of the resulting Hoare triple may, in turn, require a new pre-condition Pre
(N − 1) to be
satisfied. This process of strengthening the pre- and post-conditions of the Hoare
triple involving ∂P N can be iterated until a fix-point is reached, i.e. no further
pre-conditions are needed for the parameterized Hoare triple to hold. While the
fix-point was quickly reached for all benchmarks we experimented with, we also
discuss how to handle cases where the above process may not converge easily.
Note that since we effectively strengthen the pre-condition of the Hoare triple in
the inductive step, for the overall induction to go through, it is also necessary to
check that the strengthened assertions hold at the end of each base case check.
The technique described above is called full-program induction, and the following
theorem guarantees its soundness.
Theorem 1. Given {ϕ(N )} P N {ψ(N )}, suppose the following are true:
1. For N > 1, {ϕ(N )} P N −1 ; ∂P N {ψ(N )} holds iff {ϕ(N )} P N {ψ(N )} holds.
2. For N > 1, there exists a formula ∂ϕ(N ) such that (a) ∂ϕ(N ) doesn’t refer
to any program variable or array element modified in P N −1 , and (b) ϕ(N ) →
ϕ(N − 1) ∧ ∂ϕ(N ).
3. There exists an integer M ≥ 1 and a parameterized formula Pre(M ) such
that (a) {ϕ(N )} P N {ψ(N )} holds for 0 < N ≤ M , (b) {ϕ(M )} P M {ψ(M )∧
Pre(M )} holds, and (c) {ψ(N − 1) ∧ Pre(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N ) ∧
Pre(N )} holds for N > M.
Then {ϕ N } P N {ψ N } holds for all N ≥ 1.
Proof. For 0 < N ≤ M , condition 3(a) ensures that {ϕ(N )} P N {ψ(N )} holds.
For N > M, note that by virtue of condition 1 and 2(b), {ϕ(N )} P N {ψ(N )}
holds if {ϕ(N − 1) ∧ ∂ϕ(N )} P N −1 ; ∂P N {ψ(N ) ∧ Pre(N )} holds. With ψ(N −
1) ∧ Pre(N − 1) as a mid-condition, and by virtue of condition 2(a), the latter
Hoare triple holds for N > M if {ϕ(M )} P M {ψ(M ) ∧ Pre(M )} holds and
{ψ(N − 1) ∧ Pre(N − 1) ∧ ∂ϕ(N )} ∂P N {ψ(N ) ∧ Pre(N )} holds for all N > M.
Both these triples are seen to hold by virtue of conditions 3(b) and (c).
3 Algorithms for Full-program Induction
We now discuss the full-program induction algorithm, focusing on generation
of three crucial components: difference program ∂P N , difference pre-condition
∂ϕ(N ), and the formula Pre(N ) for strengthening pre- and post-conditions.