inputs 1 and 0 during the two loop
iterations) that neither x nor y went
down, and thus the disjunctive termination argument is not valid for the
program in Figure 3.
argument Validity Checking
While validity checking for disjunctive termination arguments is more
difficult than checking for monolithic arguments, we can adapt the
problem statement such that recently
developed tools for proving the validity of assertions in programs (such as
Slam2).
An assertion statement can be put
in a program to check if a condition
is true. For example, assert(y ≥ 1);
checks that y ≥ 1 after executing the
command. We can use an assertion
checking tool to formally investigate at
compile time whether the conditions
passed to assertion statements always
evaluate to true. For example, most as-
sertion checking tools will be able to
prove the assert statement at line 3
in Figure 4 never fails. Note that com-
pile-time assertion checking is itself
an undecidable problem, although it
is technically in an easier class of dif-
ficulty than termination.d
The reason that assertion checking
is so important to termination is the
validity of disjunctive termination ar-
guments can be encoded as an asser-
tion statement, where the statement
fails only in the case that the termina-
tion argument is not valid. Once we are
given an argument of the form T1 or T2
or … or Tn, to check validity we simply
want to prove the following statement:
Each time an execution passes
through one state and then through
another one, T1 or T2 or … or Tn holds
between these two states. That is, there
does not exist a pair of states, one be-
ing reachable from the other, possibly
via the unrolling of a loop, such that
neither T1 nor T2 nor … nor Tn holds be-
tween this pair of states.
This statement can be verified a
program transformation where we
introduce new variables into the program to record the state before the
unrolling of the loop and then use
here, we give a brief summary of implementation strategies based on disjunctive
termination arguments deployed by the recent termination checkers:
Refinement: 9, 14 In Cook et al., 14 the termination argument begins with ø. We first
attempt to prove that R+ ⊆ ø. When this proof fails, rank function synthesis is applied
to the witness, thus giving a refinement T1 to the argument, which is then rechecked
r+ ⊆ ø ∪ T1. this process is repeated until a valid argument is found or a real
counterexample is found.
In Chawdhary et al., 9 the termination argument T is constructed following the
structure of the transition relation R = R1 ∪ . . . ∪ Rm by using a ranking function
synthesis procedure, which is used to compute a well-founded overapproximation
WF (X) of a binary relation X. the initial candidate T = WF(R1) ∪ . . . ∪ WF (Rm) is extended
with WF (WF (Ri) ° Rj) and so on until the fixpoint is reached.
Variance analysis: 3, 32 as described in some detail in this article, the approach from
Berdine et al. 3 and Podelski et al. 32 uses program transformations and abstract
interpretation for invariants to compute an overapproximation T1; T2, . . . , Tn such that
R+ ⊆ T1 ∪ T2 . . . ∪ Tn. It then uses rank function synthesis to check that each Ti is well-founded.
In contrast to the refinement-based methods, variance analysis always terminates,
but may return “don’t know” in cases when a refinement-based method succeeds.
Implementation Strategies
an assertion statement to check the
termination argument always holds
between the current state and the recorded state. If the assertion checker
can prove the assert cannot fail, it has
proved the validity of the termination
argument. We can use encoding tricks
to force the assertion checker to consider all possible unrollings.
Figure 5 offers such an example,
where we have used the termination
argument “x goes down by at least one
and x is greater than 0” using the en-
coding given in Cook et al. 14 The new
code (introduced as a part of the en-
coding) is given in red, whereas the
original program from Figure 1 is in
black. We make use of an extra call to
input() to decide when the unroll-
ing begins. The new variables oldx
and oldy are used for recording a state.
Note that the assertion checker must
consider all values possibly returned
by input() during its proof, thus the
proof of termination is valid for any
starting position. This has the effect of
figure 6. encoding of termination argument validity using previous program.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
copied := 0;
x := input();
y := input();
while x > 0 and y > 0 do
if copied = 1 then
assert( (oldx ≥ x + 1 and oldx > 0)
or
(oldy ≥ y + 1 and oldy > 0)
);
elsif input() = 1 then
copied := 1;
oldx := x;
oldy := y;
fi
if input() = 1 then
x := x – 1;
y := y + 1;
else
y := y – 1;
fi
done
d Checking validity of an assertion statement is
an undecidable but co-recursively enumerable
problem, whereas termination is neither r.e.
nor co-r.e. problem.
encoding of termination argument validity using the program from Figure 1 and the termination
argument “x goes down by at least one and is larger than 0 or y goes down by at least one
and is larger than 0.” The black code comes directly from Figure 1. The code in red implements
the encoding of validity with an assertion statement.