PONES: A Region-Graph Based Termination Prover for Program Loops
PONES stands for POsitive-NEgative-Standstill, the three types of regions that it constructs for proving termination for program loops. It can check termination for the loops in the so-called "Deterministic multiple-path linear numerical loops with conjunctive conditions" class, which we abbreviate as "G*P*". Intuitively, a loop in this class has the following characteristics: (1) its loop condition can be expressed as a conjunction of linear inequalities; (2) its body consists of several branches such that each branch has an enabling condition as a conjunction of linear inequalities, (3) each branch updates any variable by a linear expression; and (4) there exists one and only one enabled branch to be taken at each iteration of the loop. PONES can prove termination fully automatically.
PONES is written in Java, and uses "lp_solve" as its LP solving engine. Currently, it has no graphic user interface.
The Theory Behind
In the following, we briefly explain the idea of our region-graph based termination proving technique. More details can be found in the paper [LW06].
Given a loop, we assume that each inequality in the loop condition already takes the form "a_1*x_1+...+a_n*x_n>(or >=)a_0". We call the left-hand side of the inequality a guard of the loop. Apparently, the runtime value of the guard is bounded by "a_0" during the loop iteration. A region is a (sub)set of variable valuations that satisfy the loop condition and form geometrically a convex polyhedron. A positive region is where, after one loop iteration, the value of some guard is decreased, i.e., the guard value moves closer to its lower bound as restricted in the loop condition. A negative region is where the value of some guard is increased after one iteration. A standstill region keeps the value of some guard unchanged after one iteration. There is a transition from one region A to another region B if at some point within A it moves to some point in B after one iteration. A region graph consists of a set of disjoint regions with the complete set of transitions between the regions, where all the member regions cover all loop condition satisfying valuations. A sufficient and necessary condition for the termination of a loop is the following: (1) after any region is entered, it will be eventually exited; and (2) no region is visited infinitely often.
We developed a method to construct region graphs for a loop, with respect to the guards in the loop condition. Any region constructed using our method can be described as a set of linear inequalities. Next, we use a series of incomplete tests to check if one of the constructed region graphs satisfies the above mentioned two conditions. These tests can be conducted fully automatically by solving Linear Programming (LP) problems. These tests are incomplete, so not all terminating loops can be proved to be so.
To illustrate our proving technique, the left shows a region graph that PONES constructs for the following loop where "x" is an integer variable:
while (x >= 0){ x := -2x + 10; }
The left region is negative because the value of the guard "x" is always increased after one loop iteration. The right region is positive. There is no standstill region. To validate the first condition that a region will always be exited after it is entered, we can see that there is no self-transition at any of the two regions. The first condition simply holds. To show that the second condition is satisfied, i.e., no region is entered infinitely often, we need to show the following: For the left negative region, every time that it is re-entered, it is entered at a point with a smaller guard value than it was entered at the last time. For instance, x=3 is a point in the left region. After one iteration, it moves to the point x=4 in the right positive region. One more iteration moves back to the negative region at the point x=2, which is smaller than 3, the guard value at the point x=2 when the region was entered at the last time. Because the left region is bounded by the value of x, this region cannot be repeatedly entered forever. This proves that no region can be entered infinitely often.
Usage & Screenshots
Currently, we still count on manual transformations and abstractions to extract loops from a program.
Maintenance Status
PONES has not been maintained and modified since 2006.
Release
There is no public release of PONES right now.
Future Development
We will implement automatic loop extracting methods such that no human assistant is expected. We will also build a graphic user interface. There are still some bugs in PONES that need to be removed.
We will also develop a method to estimate loop iteration counts based on the region-graph termination proving techniques.