Verifying Array Manipulating Programs with Full-Program Induction
35
Algorithm 7 FPIDecomposeVerify( i : integer )
1: do
2:
Pre
i (N − 1), ∂ϕ
i (N ) := NextDecomposition(Prei(N − 1));
3:
Check if (a) ∂ϕ
i (N ) ∧ Pre
i (N − 1) → Prei(N − 1),
4:
(b) ϕ(N ) → ϕ(N − 1) ∧
∂ϕ
i (N ) ∧ ∂ϕ(N )
,
5:
(c) PN−1 does not update any variable or array element in ∂ϕ
i (N )
6:
if any check in lines 3-5 fails then
7:
if HasNextDecomposition(Prei(N − 1)) then
8:
continue;
9:
else
10:
return False;
11:
if {c Prei−1(N − 1) ∧ ψ(N − 1) ∧ Prei(N − 1) ∧ ∂ϕ(N )} ∂PN {c Prei−1(N ) ∧ ψ(N ) ∧ Pre
i (N )}
then
12:
return True;
Assertion verified
13:
else
14:
c Prei(N ) := c Prei−1(N ) ∧ Pre
i (N );
15:
i := i + 1;
16:
Prei(N − 1) := LoopFreeWP(Pre
i−1 (N ), ∂PN );
Dijkstra’s WP sans WP-for-loops
17:
if {ϕ(1)} P1 {c Prei−1(1) ∧ Prei(1)} does not hold then
18:
i := i − 1;
19:
else
20:
prev ∂ϕ(N ) := ∂ϕ(N );
21:
∂ϕ(N ) := ∂ϕ
i−1 (N ) ∧ ∂ϕ(N );
22:
if FPIDecomposeVerify(i) returns False then
23:
i := i − 1; ∂ϕ(N ) := prev ∂ϕ(N );
24:
else
25:
return True;
26: while HasNextDecomposition(Prei(N − 1));
27: return False;
Generalized FPI Algorithm. While algorithm FPIVerify suffices for all of
our experiments, we may not always be so lucky. Specifically, even if ∂P N is loopfree, the analysis may exit the loop in lines 9-18 of FPIVerify by violating the
base case check in line 18. To handle (at least partly) such cases, we propose the
following strategy. Whenever a (weakest) pre-condition Pre i (N − 1) is generated,
instead of using it directly to strengthen the current pre- and post-conditions,
we “decompose” it into two formulas Pre
i (N − 1) and ∂ϕ
i (N ) with a two-fold
intent: (a) potentially weaken Pre i (N − 1) to Pre
i (N − 1), and (b) potentially
strengthen the difference formula ∂ϕ(N ) to ∂ϕ
i (N ) ∧ ∂ϕ(N ). The checks for
these intended usages of Pre
i (N − 1) and ∂ϕ
i (N ) are implemented in lines 3, 4,
5, 11 and 17 of routine FPIDecomposeVerify, shown as Algorithm 7. This
routine is meant to be invoked as FPIDecomposeVerify(i) after each iteration of the loop in lines 9-18 of routine FPIVerify (so that Pre i (N ), c Pre i (N )
etc. are initialized properly). In general, several “decompositions” of Pre i (N )
may be possible, and some of them may work better than others. FPIDecompseVerify permits multiple decompositions to be tried through the use of the
NextDecomposition and HasNextDecomposition functions. Lines 22-25 of
FPIDecomposeVerify implement a simple back-tracking strategy, allowing a
search of the space of decompositions of Pre i (N − 1). Observe that when we
use FPIDecomposeVerify, we simultaneously compute a difference formula
(∂ϕ
i (N ) ∧ ∂ϕ(N )) and an inductive pre-condition (c Pre i−1 (N ) ∧ Pre
i (N )).
Lemma 5. Algorithms FPIVerify and FPIDecomposeVerify ensure conditions 2 and 3 of Theorem 1 upon successful termination.
35
Algorithm 7 FPIDecomposeVerify( i : integer )
1: do
2:
Pre
i (N − 1), ∂ϕ
i (N ) := NextDecomposition(Prei(N − 1));
3:
Check if (a) ∂ϕ
i (N ) ∧ Pre
i (N − 1) → Prei(N − 1),
4:
(b) ϕ(N ) → ϕ(N − 1) ∧
∂ϕ
i (N ) ∧ ∂ϕ(N )
,
5:
(c) PN−1 does not update any variable or array element in ∂ϕ
i (N )
6:
if any check in lines 3-5 fails then
7:
if HasNextDecomposition(Prei(N − 1)) then
8:
continue;
9:
else
10:
return False;
11:
if {c Prei−1(N − 1) ∧ ψ(N − 1) ∧ Prei(N − 1) ∧ ∂ϕ(N )} ∂PN {c Prei−1(N ) ∧ ψ(N ) ∧ Pre
i (N )}
then
12:
return True;
Assertion verified
13:
else
14:
c Prei(N ) := c Prei−1(N ) ∧ Pre
i (N );
15:
i := i + 1;
16:
Prei(N − 1) := LoopFreeWP(Pre
i−1 (N ), ∂PN );
Dijkstra’s WP sans WP-for-loops
17:
if {ϕ(1)} P1 {c Prei−1(1) ∧ Prei(1)} does not hold then
18:
i := i − 1;
19:
else
20:
prev ∂ϕ(N ) := ∂ϕ(N );
21:
∂ϕ(N ) := ∂ϕ
i−1 (N ) ∧ ∂ϕ(N );
22:
if FPIDecomposeVerify(i) returns False then
23:
i := i − 1; ∂ϕ(N ) := prev ∂ϕ(N );
24:
else
25:
return True;
26: while HasNextDecomposition(Prei(N − 1));
27: return False;
Generalized FPI Algorithm. While algorithm FPIVerify suffices for all of
our experiments, we may not always be so lucky. Specifically, even if ∂P N is loopfree, the analysis may exit the loop in lines 9-18 of FPIVerify by violating the
base case check in line 18. To handle (at least partly) such cases, we propose the
following strategy. Whenever a (weakest) pre-condition Pre i (N − 1) is generated,
instead of using it directly to strengthen the current pre- and post-conditions,
we “decompose” it into two formulas Pre
i (N − 1) and ∂ϕ
i (N ) with a two-fold
intent: (a) potentially weaken Pre i (N − 1) to Pre
i (N − 1), and (b) potentially
strengthen the difference formula ∂ϕ(N ) to ∂ϕ
i (N ) ∧ ∂ϕ(N ). The checks for
these intended usages of Pre
i (N − 1) and ∂ϕ
i (N ) are implemented in lines 3, 4,
5, 11 and 17 of routine FPIDecomposeVerify, shown as Algorithm 7. This
routine is meant to be invoked as FPIDecomposeVerify(i) after each iteration of the loop in lines 9-18 of routine FPIVerify (so that Pre i (N ), c Pre i (N )
etc. are initialized properly). In general, several “decompositions” of Pre i (N )
may be possible, and some of them may work better than others. FPIDecompseVerify permits multiple decompositions to be tried through the use of the
NextDecomposition and HasNextDecomposition functions. Lines 22-25 of
FPIDecomposeVerify implement a simple back-tracking strategy, allowing a
search of the space of decompositions of Pre i (N − 1). Observe that when we
use FPIDecomposeVerify, we simultaneously compute a difference formula
(∂ϕ
i (N ) ∧ ∂ϕ(N )) and an inductive pre-condition (c Pre i−1 (N ) ∧ Pre
i (N )).
Lemma 5. Algorithms FPIVerify and FPIDecomposeVerify ensure conditions 2 and 3 of Theorem 1 upon successful termination.