34
S. Chakraborty et al.
Algorithm 6 FPIVerify(PN : program, ϕ(N ): pre-condn, ψ(N ): post-condn)
1: if Base case check {ϕ(1)} P1 {ψ(1)} fails then
2:
return “Counterexample found!”;
3: ∂ϕ(N ) := SyntacticDiff(ϕ(N ));
4: ∂PN := ProgramDiff(PN );
5: ∂PN := SimplifyDiff(∂PN );
Simplify and Accelerate loops
6: i := 0;
7: Prei(N ) := ψ(N );
8: c Prei(N ) := True;
Cumulative conjoined pre-condition
9: do
10:
if {c Prei(N − 1) ∧ ψ(N − 1) ∧ ∂ϕ(N )} ∂PN {c Prei(N ) ∧ ψ(N )} then
11:
return True;
Assertion verified
12:
i := i + 1;
13:
Prei(N − 1) := LoopFreeWP(Prei−1(N ), ∂PN );
Dijkstra’s WP sans WP-for-loops
14:
if no new Prei(N − 1) obtained then
Can happen if ∂PN has a loop
15:
return FPIVerify(∂PN , c Prei−1(N − 1) ∧ ψ(N − 1) ∧ ∂ϕ(N ), c Prei−1(N ) ∧ ψ(N ));
16:
else
17:
c Prei(N ) := c Prei−1(N ) ∧ Prei(N );
18: while Base case check {ϕ(1)} P1 {c Prei(1)} passes;
19: return False;
Failed to prove by full-program induction
can always be computed using quantifier elimination engines in state-of-the-art
SMT solvers like Z3 if ∂P N is loop-free. In such cases, we use a set of heuristics
to simplify the calculation of the weakest pre-condition before harnessing the
power of the quantifier elimination engine. If ∂P N contains a loop, it may still
be possible to obtain the weakest pre-condition if the loop doesn’t affect the
post-condition. Otherwise, we compute as much of the weakest pre-condition as
can be computed from the non-loopy parts of ∂P N , and then try to recursively
solve the problem by invoking full-program induction on ∂P N with appropriate
pre- and post-conditions.
Verification by Full-program Induction. The basic full-program induction
algorithm is presented as routine FPIVerify in Algorithm 6. The main steps
of this algorithm are: checking conditions 3(a), 3(b) and 3(c) of Theorem 1
(lines 1, 18 and 10), calculating the weakest pre-condition of the relevant part
of the post-condition (line 13), and strengthening the pre-condition and postcondition with the weakest pre-condition thus calculated (line 17). Since the
weakest pre-condition computed in every iteration of the loop (P re i (N − 1) in
line 13) is conjoined to strengthen the inductive pre-condition (c P re i (N ) in line
17), it suffices to compute the weakest pre-condition of P re i−1 (N ) (instead of
c P re i (N ) ∧ ψ(N )) in line 13. The possibly multiple iterations of strengthening
of pre- and post-conditions is effected by the loop in lines 9-18. In case the loop
terminates via the return statement in line 11, the inductive claim has been
successfully proved. If the loop terminates by a violation of the condition in line
18, we report that verification by full-program induction failed. In case ∂P N has
loops and no further weakest pre-conditions can be generated, we recursively
invoke FPIVerify on ∂P N in line 15. This situation arises if, for example, we
modify the example in Fig. 1(a) by having the statement C[t3] = N; (instead of
C[t3] = 0;) in line 10. In this case, ∂P N has a single loop corresponding to the
third loop in Fig. 1(a). The difference program of ∂P N is, however, loop-free, and
hence the recursive invocation of full-program induction on ∂P N easily succeeds.
S. Chakraborty et al.
Algorithm 6 FPIVerify(PN : program, ϕ(N ): pre-condn, ψ(N ): post-condn)
1: if Base case check {ϕ(1)} P1 {ψ(1)} fails then
2:
return “Counterexample found!”;
3: ∂ϕ(N ) := SyntacticDiff(ϕ(N ));
4: ∂PN := ProgramDiff(PN );
5: ∂PN := SimplifyDiff(∂PN );
Simplify and Accelerate loops
6: i := 0;
7: Prei(N ) := ψ(N );
8: c Prei(N ) := True;
Cumulative conjoined pre-condition
9: do
10:
if {c Prei(N − 1) ∧ ψ(N − 1) ∧ ∂ϕ(N )} ∂PN {c Prei(N ) ∧ ψ(N )} then
11:
return True;
Assertion verified
12:
i := i + 1;
13:
Prei(N − 1) := LoopFreeWP(Prei−1(N ), ∂PN );
Dijkstra’s WP sans WP-for-loops
14:
if no new Prei(N − 1) obtained then
Can happen if ∂PN has a loop
15:
return FPIVerify(∂PN , c Prei−1(N − 1) ∧ ψ(N − 1) ∧ ∂ϕ(N ), c Prei−1(N ) ∧ ψ(N ));
16:
else
17:
c Prei(N ) := c Prei−1(N ) ∧ Prei(N );
18: while Base case check {ϕ(1)} P1 {c Prei(1)} passes;
19: return False;
Failed to prove by full-program induction
can always be computed using quantifier elimination engines in state-of-the-art
SMT solvers like Z3 if ∂P N is loop-free. In such cases, we use a set of heuristics
to simplify the calculation of the weakest pre-condition before harnessing the
power of the quantifier elimination engine. If ∂P N contains a loop, it may still
be possible to obtain the weakest pre-condition if the loop doesn’t affect the
post-condition. Otherwise, we compute as much of the weakest pre-condition as
can be computed from the non-loopy parts of ∂P N , and then try to recursively
solve the problem by invoking full-program induction on ∂P N with appropriate
pre- and post-conditions.
Verification by Full-program Induction. The basic full-program induction
algorithm is presented as routine FPIVerify in Algorithm 6. The main steps
of this algorithm are: checking conditions 3(a), 3(b) and 3(c) of Theorem 1
(lines 1, 18 and 10), calculating the weakest pre-condition of the relevant part
of the post-condition (line 13), and strengthening the pre-condition and postcondition with the weakest pre-condition thus calculated (line 17). Since the
weakest pre-condition computed in every iteration of the loop (P re i (N − 1) in
line 13) is conjoined to strengthen the inductive pre-condition (c P re i (N ) in line
17), it suffices to compute the weakest pre-condition of P re i−1 (N ) (instead of
c P re i (N ) ∧ ψ(N )) in line 13. The possibly multiple iterations of strengthening
of pre- and post-conditions is effected by the loop in lines 9-18. In case the loop
terminates via the return statement in line 11, the inductive claim has been
successfully proved. If the loop terminates by a violation of the condition in line
18, we report that verification by full-program induction failed. In case ∂P N has
loops and no further weakest pre-conditions can be generated, we recursively
invoke FPIVerify on ∂P N in line 15. This situation arises if, for example, we
modify the example in Fig. 1(a) by having the statement C[t3] = N; (instead of
C[t3] = 0;) in line 10. In this case, ∂P N has a single loop corresponding to the
third loop in Fig. 1(a). The difference program of ∂P N is, however, loop-free, and
hence the recursive invocation of full-program induction on ∂P N easily succeeds.