A Calculus for Modular Loop Acceleration
67
Finally, we present a variant of Thm. 4 for conditional acceleration. The
idea is similar to the approach for deducing metering functions of the form
x → I q
ϕ (x) · f (x) from [16] (see Sec. 3.3 for details). But in contrast to [16], in
our setting the “conditional” part q
ϕ does not need to be an invariant of the loop.
Theorem 9 (Conditional Acceleration via Metering Functions). Let
mf : Z
d
→ Q. If
q
ϕ(x) ∧ χ(x) =⇒ mf (x) − mf (a(x)) ≤ 1
and
q
ϕ(x) ∧ ¬χ(x) =⇒ mf (x) ≤ 0,
then the following conditional acceleration technique is sound:
(χ, a, q
ϕ) → x
= a
n (x) ∧ χ(x) ∧ n < mf (x) + 1
6 Acceleration via Eventual Monotonicity
The combination of the calculus from Sec. 4 and the conditional acceleration
techniques from Sec. 5 still fails to handle certain interesting classes of loops.
Thus, to improve the applicability of our approach we now present two new
acceleration techniques based on eventual monotonicity.
6.1 Acceleration via Eventual Decrease
All (combinations of) techniques presented so far fail for the following example.
while x 1 > 0 do (
x1
x2 ) ←
x1+x2
x2−1
(T ev-dec )
The reason is that x 1 does not behave monotonically, i.e., x 1 > 0 is neither an
invariant nor a converse invariant. Essentially, T ev-dec proceeds in two phases: In
the first (optional) phase, x 2 is positive and hence the value of x 1 is monotonically
increasing. In the second phase, x 2 is non-positive and consequently the value of
x 1 decreases (weakly) monotonically. The crucial observation is that once the
value of x 1 decreases, it can never increase again. Thus, despite the non-monotonic
behavior of x 1 , it suffices to require that x 1 > 0 holds before the first and before
the n
th loop iteration to ensure that the loop can be iterated at least n times.
Theorem 10 (Acceleration via Eventual Decrease). If ϕ(x) ≡
k
i=1 C i
where each C i contains an inequation expr i (x) > 0 such that
expr i (x) ≥ expr i (a(x)) =⇒ expr i (a(x)) ≥ expr i (a
2 (x)),
then the following acceleration technique is sound:
T loop → x
= a
n (x) ∧
k
i=1
expr i (x) > 0 ∧ expr i (a
n−1 (x)) > 0
If C i ≡ expr i > 0 for all i ∈ [1, k], then it is exact.
67
Finally, we present a variant of Thm. 4 for conditional acceleration. The
idea is similar to the approach for deducing metering functions of the form
x → I q
ϕ (x) · f (x) from [16] (see Sec. 3.3 for details). But in contrast to [16], in
our setting the “conditional” part q
ϕ does not need to be an invariant of the loop.
Theorem 9 (Conditional Acceleration via Metering Functions). Let
mf : Z
d
→ Q. If
q
ϕ(x) ∧ χ(x) =⇒ mf (x) − mf (a(x)) ≤ 1
and
q
ϕ(x) ∧ ¬χ(x) =⇒ mf (x) ≤ 0,
then the following conditional acceleration technique is sound:
(χ, a, q
ϕ) → x
= a
n (x) ∧ χ(x) ∧ n < mf (x) + 1
6 Acceleration via Eventual Monotonicity
The combination of the calculus from Sec. 4 and the conditional acceleration
techniques from Sec. 5 still fails to handle certain interesting classes of loops.
Thus, to improve the applicability of our approach we now present two new
acceleration techniques based on eventual monotonicity.
6.1 Acceleration via Eventual Decrease
All (combinations of) techniques presented so far fail for the following example.
while x 1 > 0 do (
x1
x2 ) ←
x1+x2
x2−1
(T ev-dec )
The reason is that x 1 does not behave monotonically, i.e., x 1 > 0 is neither an
invariant nor a converse invariant. Essentially, T ev-dec proceeds in two phases: In
the first (optional) phase, x 2 is positive and hence the value of x 1 is monotonically
increasing. In the second phase, x 2 is non-positive and consequently the value of
x 1 decreases (weakly) monotonically. The crucial observation is that once the
value of x 1 decreases, it can never increase again. Thus, despite the non-monotonic
behavior of x 1 , it suffices to require that x 1 > 0 holds before the first and before
the n
th loop iteration to ensure that the loop can be iterated at least n times.
Theorem 10 (Acceleration via Eventual Decrease). If ϕ(x) ≡
k
i=1 C i
where each C i contains an inequation expr i (x) > 0 such that
expr i (x) ≥ expr i (a(x)) =⇒ expr i (a(x)) ≥ expr i (a
2 (x)),
then the following acceleration technique is sound:
T loop → x
= a
n (x) ∧
k
i=1
expr i (x) > 0 ∧ expr i (a
n−1 (x)) > 0
If C i ≡ expr i > 0 for all i ∈ [1, k], then it is exact.