62
F. Frohn
Here, ϕ 1 and ϕ 3 are again invariants of the loop. Thus, as in Thm. 2 it suffices
to require that they hold before entering the loop. On the other hand, ϕ 2 needs
to satisfy a similar condition as in Thm. 1 and thus it suffices to require that ϕ 2
holds before the last iteration. We also say that ϕ 2 is a converse invariant (w.r.t.
ϕ 1 ). It is easy to see that Thm. 3 is equivalent to Thm. 1 if ϕ 1 ≡ ϕ 3 ≡ ≡ (where
denotes logical truth) and it is equivalent to Thm. 2 if ϕ 2 ≡ ϕ 3 ≡ ≡.
With this approach, T non-dec can be accelerated to
x
1
x
2
=
x1−n
x2+n
∧ x 2 > 0 ∧ x 1 − n + 1 > 0
( ψ non-dec )
by choosing ϕ 1 := x 2 > 0, ϕ 2 := x 1 > 0, and ϕ 3 := .
Thm. 3 naturally raises the question: Why do we need two invariants? To see
this, consider a restriction of Thm. 3 where ϕ 3 := . It would fail for a loop like
while x 1 > 0 ∧ x 2 > 0 do (
x1
x2 ) ←
x1+x2
x2−1
(T 2-invs )
which can easily be handled by Thm. 3 (by choosing ϕ 1 := , ϕ 2 := x 2 > 0,
and ϕ 3 := x 1 > 0). The problem is that the converse invariant x 2 > 0 is needed
to prove invariance of x 1 > 0. Similarly, a restriction of Thm. 3 where ϕ 1 :=
would fail for the following variant of T 2-invs :
while x 1 > 0 ∧ x 2 > 0 do (
x1
x2 ) ←
x1−x2
x2+1
Here, the problem is that the invariant x 2 > 0 is needed to prove converse
invariance of x 1 > 0.
3.3 Acceleration via Metering Functions
Another approach for loop acceleration uses metering functions, a variation of
classical ranking functions from termination and complexity analysis [17]. While
ranking functions give rise to upper bounds on the runtime of loops, metering
functions provide lower runtime bounds, i.e., the definition of a metering function
mf : Z
d
→ Q ensures that for each x ∈ Z
d , the loop under consideration can be
applied at least mf (x) times.
Theorem 4 (Acceleration via Metering Functions [17]). Let mf be a
metering function for T loop . Then the following acceleration technique is sound:
T loop → x
= a
n (x) ∧ ϕ(x) ∧ n < mf (x) + 1
So using the metering function x, Thm. 4 accelerates T exp to
x
1
x
2
=
x1−n
2
n ·x2
∧ x 1 > 0 ∧ n < x 1 + 1 ≡ ψ exp .
However, synthesizing non-trivial (i.e., non-constant) metering functions is
challenging. Moreover, unless the number of iterations of T loop equals mf (x)
for all x ∈ Z
d , acceleration via metering functions is not exact.
F. Frohn
Here, ϕ 1 and ϕ 3 are again invariants of the loop. Thus, as in Thm. 2 it suffices
to require that they hold before entering the loop. On the other hand, ϕ 2 needs
to satisfy a similar condition as in Thm. 1 and thus it suffices to require that ϕ 2
holds before the last iteration. We also say that ϕ 2 is a converse invariant (w.r.t.
ϕ 1 ). It is easy to see that Thm. 3 is equivalent to Thm. 1 if ϕ 1 ≡ ϕ 3 ≡ ≡ (where
denotes logical truth) and it is equivalent to Thm. 2 if ϕ 2 ≡ ϕ 3 ≡ ≡.
With this approach, T non-dec can be accelerated to
x
1
x
2
=
x1−n
x2+n
∧ x 2 > 0 ∧ x 1 − n + 1 > 0
( ψ non-dec )
by choosing ϕ 1 := x 2 > 0, ϕ 2 := x 1 > 0, and ϕ 3 := .
Thm. 3 naturally raises the question: Why do we need two invariants? To see
this, consider a restriction of Thm. 3 where ϕ 3 := . It would fail for a loop like
while x 1 > 0 ∧ x 2 > 0 do (
x1
x2 ) ←
x1+x2
x2−1
(T 2-invs )
which can easily be handled by Thm. 3 (by choosing ϕ 1 := , ϕ 2 := x 2 > 0,
and ϕ 3 := x 1 > 0). The problem is that the converse invariant x 2 > 0 is needed
to prove invariance of x 1 > 0. Similarly, a restriction of Thm. 3 where ϕ 1 :=
would fail for the following variant of T 2-invs :
while x 1 > 0 ∧ x 2 > 0 do (
x1
x2 ) ←
x1−x2
x2+1
Here, the problem is that the invariant x 2 > 0 is needed to prove converse
invariance of x 1 > 0.
3.3 Acceleration via Metering Functions
Another approach for loop acceleration uses metering functions, a variation of
classical ranking functions from termination and complexity analysis [17]. While
ranking functions give rise to upper bounds on the runtime of loops, metering
functions provide lower runtime bounds, i.e., the definition of a metering function
mf : Z
d
→ Q ensures that for each x ∈ Z
d , the loop under consideration can be
applied at least mf (x) times.
Theorem 4 (Acceleration via Metering Functions [17]). Let mf be a
metering function for T loop . Then the following acceleration technique is sound:
T loop → x
= a
n (x) ∧ ϕ(x) ∧ n < mf (x) + 1
So using the metering function x, Thm. 4 accelerates T exp to
x
1
x
2
=
x1−n
2
n ·x2
∧ x 1 > 0 ∧ n < x 1 + 1 ≡ ψ exp .
However, synthesizing non-trivial (i.e., non-constant) metering functions is
challenging. Moreover, unless the number of iterations of T loop equals mf (x)
for all x ∈ Z
d , acceleration via metering functions is not exact.