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.