Checker Termination   as of Julia version 2.4 (built on 23 Oct 2017)

belongs to group Advanced

Prove termination of methods and constructors


This checker looks for methods or constructors that might not terminate, that is, they might have an infinite execution and consequently hang the program. It is well known that termination is an undecidable property of computer programs. Hence, this checker can only approximate the set of non-terminating methods and constructors, by allowing that some actually terminating method or constructor is not recognized as such by the analyzer (false positive). However, all possibly non-terminating methods and constructors are identified by Julia.

Action: check if the method or constructor might actually diverge and debug it accordingly if that is the case. If, instead, the message is the result of the imprecision of the static analyzer, annotate the method or constructor with the @Terminates annotation (see below) and rerun the analysis to verify that all warnings have disappeared.

Manually-provided Annotations

In order to reduce the number of false positives, you can instruct the analyzer with termination annotations, placed in the code that you analyze. Usually, one performs a first termination analysis and gets many fake warnings (false positives). One can use this first analysis to place annotations in the code and then start the analysis again. In particular, Julia can be helped by putting the annotation @Terminates for methods and constructors: states that the given method or constructor always terminates, for all possible call context and parameters.

Dumping Numerical Constraints

Although this checker is meant for debugging non-terminating code, it also allows one to print numerical invariants about program variables, that can useful, for instance, for researchers. For that, just put dummy calls to com.juliasoft.julia.checkers.Watchpoint.analyzeHere() where you want the invariants to be computed and select the dumpNumericalInvariants option. Julia will then generate a text output file with the numerical invariants at the selected program points.


Examples


Consider the following program:

public class Continue {
  public static void main(String[] args) {
    int i = 0;
    while (i < 20) {
      if (i <= 10) continue;
      i++;
    }
  }
}

It is actually the case that the value of variable i is constantly 0. Hence this checker (if the binTerm option is used) issues the following warning:

Continue.java:2: [Termination: DefiniteDivergenceWarning] Continue.main may actually diverge

Note that only the BinTerm termination checker is able to prove non-termination. The default termination checker would instead just conclude that the method has not been proved to terminate, without an actual proof of non-termination.

Consider the following program now:

public class Exc4 {
  public static void main(String[] args) {
    int i = 0;
    while (i < 20) {
      i--;
      try {
        if (i > 10) throw null;
        i += 2;
      }
      catch (NullPointerException e) {
        i++;
      }
    }
  }
}

In this example, variable i increases up to 11. At that point, a null-pointer exception is systematically thrown and the exception handler increases i by 1; since i is also decreased by 1 at the beginning of the loop, the conclusion is that variable i stabilizes on the value 11 and the loop never terminates. Julia, in this case, cannot find neither a proof of termination (which is fine) nor a proof of non-termination (the program is too complex for the non-termination prover) and issues a warning, that should be verified by the programmer:

Exc4.java:2: [Termination: PossibleDivergenceWarning] are you sure that Exc4.main always terminates?

This warning must be seen as the sign of a potentially non-terminating method. In this case, it is actually the case that the method is non-terminating but, in other cases, this might be a false positive.

Below we report a simple modification of the previous program, where variable i is increased by 2 in the exception handler:

public class Exc5 {
  public static void main(String[] args) {
    int i = 0;
    while (i < 20) {
      i--;
      try {
        if (i > 10) throw null;
        i += 2;
      }
      catch (NullPointerException e) {
        i += 2;
      }
    }
  }
}

For the program above, this checker issues no warning, since Julia is able to prove that method main terminates, definitely.

Julia is also able to reason on computations over data structures, not just over integral variables as the previous examples have shown. Consider for instance the following classes:

public class Virtual {
  public static void main(String[] args) {
    Node d = new Div();
    Node n = new Nil();
    int l = Integer.parseInt(args[0]);
    while (l-- > 0)
      n = new Internal(n);
    n.length();
  }
}
public abstract class Node {
    public abstract int length();
}
public class Internal extends Node {
  private Node next;
  public Internal(Node next) {
    this.next = next;
  }
  public int length() {
    return 1 + next.length();
  }
}
public class Div extends Node {
  public int length() {
    return length();
  }
}
public class Nil extends Node {
  public int length() {
    return 0;
  }
}

Julia proves that method main of class Virtual always terminates. Consequently, this checker issues no warning. This conclusion is far from trivial. In particular, Julia is able to conclude that no Div node is reachable from variable n of main. Hence the call n.length() must terminate since the (diverging) redefinition of length inside class Div is never called.