Verifying Array Manipulating Programs with Full-Program Induction
23
// assume(true)
1. for (int t1=0; t1
if (t1==0) { A[t1] = 6; }
3.
else { A[t1] = A[t1-1]+6; }
4. }
5. for (int t2=0; t2
if (t2==0) { B[t2] = 1; }
7.
else { B[t2] = B[t2-1]+A[t2-1]; }
8. }
9. for (int t3=0; t3
11. else { C[t3] = C[t3-1]+B[t3-1]; }
12.}
// assert(forall i in 0..N-1, C[i]= i^3)
(a)
// assume(true)
1. A[0] = 6;
2. B[0] = 1;
3. C[0] = 0;
// assert((C[0] = 0^3) and (B[0] = 1^3 - 0^3) and
//
(A[0] = 2^3 - 2*1^3 + 0^3))
(b)
// assume((N > 1) and (C_Nm1[N-2] = (N-2)^3) and
//
(B_Nm1[N-2] = (N-1)^3 - (N-2)^3) and
//
(A_Nm1[N-2] = N^3 - 2*(N-1)^3 + (N-2)^3))
1. A[N-1] = A_Nm1[N-2] + 6;
2. B[N-1] = B_Nm1[N-2] + A_Nm1[N-2];
3. C[N-1] = C_Nm1[N-2] + B_Nm1[N-2];
// assert((C[N-1] = (N-1)^3) and
//
(B[N-1] = N^3 - (N-1)^3) and
//
(A[N-1] = (N+1)^3 - 2*N^3 + (N-1)^3))
(c)
Fig. 1. Original and simplified Hoare triples
which the inductive claim is formulated and proved differs significantly. Specifically, (i) we do not require explicit or implicit loop-specific invariants to be
provided by the user or generated by a solver (viz. by constrained Horn clause
solvers [21,15,10] or recurrence solvers [26,17]), (ii) we induct on the full program
(possibly containing multiple loops) with parameter N and not on iterations of
individual loops in the program, and (iii) we perform non-trivial correct-byconstruction code transformations, whenever feasible, to simplify the inductive
step of reasoning. The combination of these factors often reduces reasoning about
a program with multiple loops to reasoning about one with fewer (sometimes
even none) and “simpler” loops, thereby simplifying proof goals. In this paper, we demonstrate this, focusing on programs with sequentially composed, but
non-nested loops.
As an illustration of simplifications that can result from application of fullprogram induction, consider the problem in Fig. 1(a) again. Full-program induction reduces checking the validity of the Hoare triple in Fig. 1(a) to checking the
validity of two “simpler” Hoare triples, represented in Figs. 1(b) and 1(c). Note
that the programs in Figs. 1(b) and 1(c) are loop-free. In addition, their pre- and
post-conditions are quantifier-free. The validity of these Hoare triples (Figs. 1(b)
and 1(c)) can therefore be easily proved, e.g. by bounded model checking [6] with
a back-end SMT solver like Z3 [25]. Note that the value computed in each iteration of each loop in Fig. 1(a) is data-dependent on previous iterations of the
respective loops. Hence, none of these loops can be trivially translated to a set
of parallel assignments.
Invariant-based techniques, viz. [13,16,23,7,14,30,2,19], are popularly used
to reason about array manipulating programs. If we were to prove the assertion in Fig. 1(a) using such techniques, it would be necessary to use appropriate loop-specific invariants for each of the three loops in Fig. 1(a). The
weakest loop invariants needed to prove the post-condition in this example are:
∀i ∈ [0...t1 − 1] (A[i] = 6i + 6) for the first loop (lines 1-4), ∀j ∈ [0...t2 −
1] (B[j] = 3j
2 + 3j + 1) ∧ (A[j] = 6j + 6) for the second loop (lines 5-8), and
∀k ∈ [0...t3 − 1] (C[k] = k
3 ) ∧ (B[k] = 3k
2 + 3k + 1) for the third loop (lines
23
// assume(true)
1. for (int t1=0; t1
if (t1==0) { A[t1] = 6; }
3.
else { A[t1] = A[t1-1]+6; }
4. }
5. for (int t2=0; t2
if (t2==0) { B[t2] = 1; }
7.
else { B[t2] = B[t2-1]+A[t2-1]; }
8. }
9. for (int t3=0; t3
11. else { C[t3] = C[t3-1]+B[t3-1]; }
12.}
// assert(forall i in 0..N-1, C[i]= i^3)
(a)
// assume(true)
1. A[0] = 6;
2. B[0] = 1;
3. C[0] = 0;
// assert((C[0] = 0^3) and (B[0] = 1^3 - 0^3) and
//
(A[0] = 2^3 - 2*1^3 + 0^3))
(b)
// assume((N > 1) and (C_Nm1[N-2] = (N-2)^3) and
//
(B_Nm1[N-2] = (N-1)^3 - (N-2)^3) and
//
(A_Nm1[N-2] = N^3 - 2*(N-1)^3 + (N-2)^3))
1. A[N-1] = A_Nm1[N-2] + 6;
2. B[N-1] = B_Nm1[N-2] + A_Nm1[N-2];
3. C[N-1] = C_Nm1[N-2] + B_Nm1[N-2];
// assert((C[N-1] = (N-1)^3) and
//
(B[N-1] = N^3 - (N-1)^3) and
//
(A[N-1] = (N+1)^3 - 2*N^3 + (N-1)^3))
(c)
Fig. 1. Original and simplified Hoare triples
which the inductive claim is formulated and proved differs significantly. Specifically, (i) we do not require explicit or implicit loop-specific invariants to be
provided by the user or generated by a solver (viz. by constrained Horn clause
solvers [21,15,10] or recurrence solvers [26,17]), (ii) we induct on the full program
(possibly containing multiple loops) with parameter N and not on iterations of
individual loops in the program, and (iii) we perform non-trivial correct-byconstruction code transformations, whenever feasible, to simplify the inductive
step of reasoning. The combination of these factors often reduces reasoning about
a program with multiple loops to reasoning about one with fewer (sometimes
even none) and “simpler” loops, thereby simplifying proof goals. In this paper, we demonstrate this, focusing on programs with sequentially composed, but
non-nested loops.
As an illustration of simplifications that can result from application of fullprogram induction, consider the problem in Fig. 1(a) again. Full-program induction reduces checking the validity of the Hoare triple in Fig. 1(a) to checking the
validity of two “simpler” Hoare triples, represented in Figs. 1(b) and 1(c). Note
that the programs in Figs. 1(b) and 1(c) are loop-free. In addition, their pre- and
post-conditions are quantifier-free. The validity of these Hoare triples (Figs. 1(b)
and 1(c)) can therefore be easily proved, e.g. by bounded model checking [6] with
a back-end SMT solver like Z3 [25]. Note that the value computed in each iteration of each loop in Fig. 1(a) is data-dependent on previous iterations of the
respective loops. Hence, none of these loops can be trivially translated to a set
of parallel assignments.
Invariant-based techniques, viz. [13,16,23,7,14,30,2,19], are popularly used
to reason about array manipulating programs. If we were to prove the assertion in Fig. 1(a) using such techniques, it would be necessary to use appropriate loop-specific invariants for each of the three loops in Fig. 1(a). The
weakest loop invariants needed to prove the post-condition in this example are:
∀i ∈ [0...t1 − 1] (A[i] = 6i + 6) for the first loop (lines 1-4), ∀j ∈ [0...t2 −
1] (B[j] = 3j
2 + 3j + 1) ∧ (A[j] = 6j + 6) for the second loop (lines 5-8), and
∀k ∈ [0...t3 − 1] (C[k] = k
3 ) ∧ (B[k] = 3k
2 + 3k + 1) for the third loop (lines