Verifying Array Manipulating Programs with Full-Program Induction
25
also requires strong enough mid-conditions to be generated in the case of sequentially composed loops. We circumvent all of these requirements in the current
work. For some other techniques for analyzing array manipulating programs,
please see [7,19,18].
2 Overview of Full-program Induction
Recall that our objective is to check the validity of the parameterized Hoare triple
{ϕ(N )} P N {ψ(N )} for all N > 0. At a high level, our approach works like any
other inductive technique. Thus, we have a base case, where we verify that the
parameterized Hoare triple holds for some small values of N , say 0 < N ≤ M .
We then hypothesize that {ϕ(N − 1)} P N −1 {ψ(N − 1)} holds for some N > M,
and try to show that this implies {ϕ(N )} P N {ψ(N )}. While this sounds simple
in principle, there are several technical difficulties en route. Our contribution
lies in overcoming these difficulties algorithmically for a large class of programs
and assertions, thereby making full-program induction a viable and competitive
technique for proving properties of array manipulating programs.
We rely on an important, yet reasonable, assumption that can be stated
as follows: For every value of N (> 0), every loop in P N can be statically unrolled a fixed number (say f (N )) of times to yield a loop-free program
P N that
is semantically equivalent to P N . Note that this does not imply that reasoning about loops can be translated into loop-free reasoning. In general, f (N ) is
a non-constant function, and hence, the number of unrollings of loops in P N
may strongly depend on N . In our experience, loops in a vast majority of array
manipulating programs (including Fig. 1(a)) satisfy the above assumption. Consequently, the base case of our induction reduces to checking a Hoare triple for
a loop-free program. Checking such a Hoare triple is easily achieved by compiling the pre-condition, program and post-condition into an SMT formula, whose
(un)satisfiability can be checked with an off-the-shelf back-end SMT solver.
The inductive step is the most complex one, and is the focus of the rest of the
paper. Recall that the inductive hypothesis asserts that {ϕ(N −1)} P N −1 {ψ(N −
1)} is valid. To make use of this hypothesis in the inductive step, we must relate
the validity of {ϕ(N )} P N {ψ(N )} to that of {ϕ(N − 1)} P N −1 {ψ(N − 1)}.
We propose doing this, whenever possible, via two key notions – that of “difference” program and “difference” pre-condition. Given a parameterized program
P N , intuitively the “difference” program ∂P N is one such that P N −1 ; ∂P N is semantically equivalent to P N , where “;” denotes sequential composition. It turns
out that for our purposes, the semantic equivalence alluded to above is not really necessary; it suffices to have ∂P N such that {ϕ(N )} P N {ψ(N )} is valid iff
{ϕ(N )} P N −1 ; ∂P N {ψ(N )} is valid. We will henceforth use this interpretation of
a “difference” program. The “difference” pre-condition ∂ϕ(N ) is a formula such
that (i) ϕ(N ) → (ϕ(N − 1) ∧ ∂ϕ(N )) and (ii) the execution of P N −1 doesn’t
affect the truth of ∂ϕ(N ). Computing ∂P N and ∂ϕ(N ) is not easy in general,
and we discuss this in detail in the rest of the paper.
Assuming we have ∂P N and ∂ϕ(N ) with the properties stated above, the
proof obligation {ϕ(N )} P N {ψ(N )} can now be reduced to proving {ϕ(N −
25
also requires strong enough mid-conditions to be generated in the case of sequentially composed loops. We circumvent all of these requirements in the current
work. For some other techniques for analyzing array manipulating programs,
please see [7,19,18].
2 Overview of Full-program Induction
Recall that our objective is to check the validity of the parameterized Hoare triple
{ϕ(N )} P N {ψ(N )} for all N > 0. At a high level, our approach works like any
other inductive technique. Thus, we have a base case, where we verify that the
parameterized Hoare triple holds for some small values of N , say 0 < N ≤ M .
We then hypothesize that {ϕ(N − 1)} P N −1 {ψ(N − 1)} holds for some N > M,
and try to show that this implies {ϕ(N )} P N {ψ(N )}. While this sounds simple
in principle, there are several technical difficulties en route. Our contribution
lies in overcoming these difficulties algorithmically for a large class of programs
and assertions, thereby making full-program induction a viable and competitive
technique for proving properties of array manipulating programs.
We rely on an important, yet reasonable, assumption that can be stated
as follows: For every value of N (> 0), every loop in P N can be statically unrolled a fixed number (say f (N )) of times to yield a loop-free program
P N that
is semantically equivalent to P N . Note that this does not imply that reasoning about loops can be translated into loop-free reasoning. In general, f (N ) is
a non-constant function, and hence, the number of unrollings of loops in P N
may strongly depend on N . In our experience, loops in a vast majority of array
manipulating programs (including Fig. 1(a)) satisfy the above assumption. Consequently, the base case of our induction reduces to checking a Hoare triple for
a loop-free program. Checking such a Hoare triple is easily achieved by compiling the pre-condition, program and post-condition into an SMT formula, whose
(un)satisfiability can be checked with an off-the-shelf back-end SMT solver.
The inductive step is the most complex one, and is the focus of the rest of the
paper. Recall that the inductive hypothesis asserts that {ϕ(N −1)} P N −1 {ψ(N −
1)} is valid. To make use of this hypothesis in the inductive step, we must relate
the validity of {ϕ(N )} P N {ψ(N )} to that of {ϕ(N − 1)} P N −1 {ψ(N − 1)}.
We propose doing this, whenever possible, via two key notions – that of “difference” program and “difference” pre-condition. Given a parameterized program
P N , intuitively the “difference” program ∂P N is one such that P N −1 ; ∂P N is semantically equivalent to P N , where “;” denotes sequential composition. It turns
out that for our purposes, the semantic equivalence alluded to above is not really necessary; it suffices to have ∂P N such that {ϕ(N )} P N {ψ(N )} is valid iff
{ϕ(N )} P N −1 ; ∂P N {ψ(N )} is valid. We will henceforth use this interpretation of
a “difference” program. The “difference” pre-condition ∂ϕ(N ) is a formula such
that (i) ϕ(N ) → (ϕ(N − 1) ∧ ∂ϕ(N )) and (ii) the execution of P N −1 doesn’t
affect the truth of ∂ϕ(N ). Computing ∂P N and ∂ϕ(N ) is not easy in general,
and we discuss this in detail in the rest of the paper.
Assuming we have ∂P N and ∂ϕ(N ) with the properties stated above, the
proof obligation {ϕ(N )} P N {ψ(N )} can now be reduced to proving {ϕ(N −