66
F. Frohn
Theorem 8 (Conditional Acceleration via Monotonic Increase). If
q
ϕ(x) ∧ χ(x) =⇒ χ(a(x)),
then the following conditional acceleration technique is exact:
(χ, a, q
ϕ) → x
= a
n (x) ∧ χ(x)
Example 3. For the canonical acceleration problem of T 2-invs , we obtain:
x
= a
n
2-invs (x)
x 1 > 0 ∧ x 2 > 0
a 2-invs :=
x1+x2
x2−1
T hm. 7
e x
= a
n
2-invs (x) ∧ x 2 − n + 1 > 0 | x 2 > 0 | x 1 > 0 | a 2-invs
T hm. 8
e x
= a
n
2-invs (x) ∧ x 2 − n + 1 > 0 ∧ x 1 > 0 | x 2 > 0 ∧ x 1 > 0 | | | a 2-invs
While we could also use Thm. 1 for the first step, Thm. 2 is inapplicable in the
second step. The reason is that we need the converse invariant x 2 > 0 to prove
invariance of x 1 > 0.
It is not a coincidence that T 2-invs , which could also be accelerated with
acceleration via monotonicity (cf. Thm. 3) directly, can be handled by applying
our novel calculus with Theorems 7 and 8.
Remark 1. If applying acceleration via monotonicity to T loop yields ψ, then
x
= a
n (x) | | | ϕ(x) | a(x)
≤3
e ψ(y) | ϕ(x) | | | a(x)
where either Thm. 7 or Thm. 8 is applied in each e -step.
Thus, there is no need for a conditional variant of acceleration via monotonicity.
Note that combining Theorems 7 and 8 with our calculus is also useful for loops
where acceleration via monotonicity is inapplicable.
Example 4. Consider the following loop, which can be accelerated by splitting
its guard into one invariant and two converse invariants.
while x 1 > 0 ∧ x 2 > 0 ∧ x 3 > 0 do
x1
x2
x3
←
x1−1
x2+x1
x3−x2
(T 2-c-invs )
Let
ϕ 2-c-invs := x 1 > 0 ∧ x 2 > 0 ∧ x 3 > 0,
a 2-c-invs :=
x1−1
x2+x1
x3−x2
,
ψ
init
2-c-invs := x
= a
n
2-c-invs (x),
and let x
(m)
i
be the i
th component of a
m
2-c-invs (x). Starting with the canonical
acceleration problem of T 2-c-invs , we obtain:
ψ
init
2-c-invs
ϕ 2-c-invs
a 2-c-invs
T hm. 7
e
ψ
init
2-c-invs ∧ x
(n−1)
1
> 0
x 1 > 0
x 2 > 0 ∧ x 3 > 0
a 2-c-invs
T hm. 8
e
ψ
init
2-c-invs ∧ x
(n−1)
1
> 0 ∧ x 2 > 0
x 1 > 0 ∧ x 2 > 0
x 3 > 0
a 2-c-invs
T hm. 7
e
ψ
init
2-c-invs ∧ x
(n−1)
1
> 0 ∧ x 2 > 0 ∧ x
(n−1)
3
> 0
ϕ 2-c-invs
a 2-c-invs
F. Frohn
Theorem 8 (Conditional Acceleration via Monotonic Increase). If
q
ϕ(x) ∧ χ(x) =⇒ χ(a(x)),
then the following conditional acceleration technique is exact:
(χ, a, q
ϕ) → x
= a
n (x) ∧ χ(x)
Example 3. For the canonical acceleration problem of T 2-invs , we obtain:
x
= a
n
2-invs (x)
x 1 > 0 ∧ x 2 > 0
a 2-invs :=
x1+x2
x2−1
T hm. 7
e x
= a
n
2-invs (x) ∧ x 2 − n + 1 > 0 | x 2 > 0 | x 1 > 0 | a 2-invs
T hm. 8
e x
= a
n
2-invs (x) ∧ x 2 − n + 1 > 0 ∧ x 1 > 0 | x 2 > 0 ∧ x 1 > 0 | | | a 2-invs
While we could also use Thm. 1 for the first step, Thm. 2 is inapplicable in the
second step. The reason is that we need the converse invariant x 2 > 0 to prove
invariance of x 1 > 0.
It is not a coincidence that T 2-invs , which could also be accelerated with
acceleration via monotonicity (cf. Thm. 3) directly, can be handled by applying
our novel calculus with Theorems 7 and 8.
Remark 1. If applying acceleration via monotonicity to T loop yields ψ, then
x
= a
n (x) | | | ϕ(x) | a(x)
≤3
e ψ(y) | ϕ(x) | | | a(x)
where either Thm. 7 or Thm. 8 is applied in each e -step.
Thus, there is no need for a conditional variant of acceleration via monotonicity.
Note that combining Theorems 7 and 8 with our calculus is also useful for loops
where acceleration via monotonicity is inapplicable.
Example 4. Consider the following loop, which can be accelerated by splitting
its guard into one invariant and two converse invariants.
while x 1 > 0 ∧ x 2 > 0 ∧ x 3 > 0 do
x1
x2
x3
←
x1−1
x2+x1
x3−x2
(T 2-c-invs )
Let
ϕ 2-c-invs := x 1 > 0 ∧ x 2 > 0 ∧ x 3 > 0,
a 2-c-invs :=
x1−1
x2+x1
x3−x2
,
ψ
init
2-c-invs := x
= a
n
2-c-invs (x),
and let x
(m)
i
be the i
th component of a
m
2-c-invs (x). Starting with the canonical
acceleration problem of T 2-c-invs , we obtain:
ψ
init
2-c-invs
ϕ 2-c-invs
a 2-c-invs
T hm. 7
e
ψ
init
2-c-invs ∧ x
(n−1)
1
> 0
x 1 > 0
x 2 > 0 ∧ x 3 > 0
a 2-c-invs
T hm. 8
e
ψ
init
2-c-invs ∧ x
(n−1)
1
> 0 ∧ x 2 > 0
x 1 > 0 ∧ x 2 > 0
x 3 > 0
a 2-c-invs
T hm. 7
e
ψ
init
2-c-invs ∧ x
(n−1)
1
> 0 ∧ x 2 > 0 ∧ x
(n−1)
3
> 0
ϕ 2-c-invs
a 2-c-invs