Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

/**
 * A recursive loop.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate.
 *
 * @author <A HREF="mailto:[e-mail]">Fausto Spoto</A>
 */

public class Double3 {

    private static void test(int n) {
	while (--n > 0) test(n);
    }

    public static void main(String[] args) {
	test(10);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Double3.main([Ljava/lang/String;)V: Graph of 31 nodes with 0 SCCs.

Double3.test(I)V: Graph of 15 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Double3.test(I)V
SCC calls the following helper methods: Double3.test(I)V
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
• Marker field analysis yielded the following relations that could be markers:
  

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 14 IRules

P rules:
f322_0_test_Inc(EOS, i27, i38) → f325_0_test_Load(EOS, i27, +(i38, -1))
f325_0_test_Load(EOS, i27, i41) → f327_0_test_LE(EOS, i27, i41, i41)
f327_0_test_LE(EOS, i27, i45, i45) → f330_0_test_LE(EOS, i27, i45, i45)
f330_0_test_LE(EOS, i27, i45, i45) → f333_0_test_Load(EOS, i27, i45) | >(i45, 0)
f333_0_test_Load(EOS, i27, i45) → f337_0_test_InvokeMethod(EOS, i27, i45, i45)
f337_0_test_InvokeMethod(EOS, i27, i45, i45) → f343_0_test_Inc(EOS, i45, i45)
f337_0_test_InvokeMethod(EOS, i27, i45, i45) → f343_1_test_Inc(EOS, i27, i45, i45, i45)
f343_0_test_Inc(EOS, i45, i45) → f348_0_test_Inc(EOS, i45, i45)
f348_0_test_Inc(EOS, i45, i45) → f269_0_test_Inc(EOS, i45, i45)
f269_0_test_Inc(EOS, i27, i27) → f322_0_test_Inc(EOS, i27, i27)
f355_0_test_Return(EOS, i27, i50, i50) → f357_0_test_JMP(EOS, i27, i50)
f357_0_test_JMP(EOS, i27, i50) → f360_0_test_Inc(EOS, i27, i50)
f360_0_test_Inc(EOS, i27, i50) → f322_0_test_Inc(EOS, i27, i50)
f343_1_test_Inc(EOS, i27, i50, i50, i50) → f355_0_test_Return(EOS, i27, i50, i50)

Combined rules. Obtained 2 IRules

P rules:
f322_0_test_Inc(EOS, x0, x1) → f322_0_test_Inc(EOS, -(x1, 1), -(x1, 1)) | >(x1, 1)
f322_0_test_Inc(EOS, x0, x1) → f322_0_test_Inc(EOS, x0, -(x1, 1)) | >(x1, 1)

Filtered ground terms:

f322_0_test_Inc(x1, x2, x3) → f322_0_test_Inc(x2, x3)
Cond_f322_0_test_Inc(x1, x2, x3, x4) → Cond_f322_0_test_Inc(x1, x3, x4)
Cond_f322_0_test_Inc1(x1, x2, x3, x4) → Cond_f322_0_test_Inc1(x1, x3, x4)

Filtered unneeded terms:

Cond_f322_0_test_Inc(x1, x2, x3) → Cond_f322_0_test_Inc(x1, x3)
Cond_f322_0_test_Inc1(x1, x2, x3) → Cond_f322_0_test_Inc1(x1, x3)
f322_0_test_Inc(x1, x2) → f322_0_test_Inc(x2)

Prepared 1 rules for path length conversion:

P rules:
f322_0_test_Inc(x1) → f322_0_test_Inc(-(x1, 1)) | >(x1, 1)

Finished conversion. Obtained 1 rules.

P rules:
f322_0_test_Inc(x0) → f322_0_test_Inc(-(x0, 1)) | >(x0, 1)

(6) Obligation:

Rules:
f322_0_test_Inc(x0) → f322_0_test_Inc(-(x0, 1)) | >(x0, 1)

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f322_0_test_Inc(x2)] = x2

Therefore the following rule(s) have been dropped:

f322_0_test_Inc(x0) → f322_0_test_Inc(-(x0, 1)) | >(x0, 1)

(8) YES