(0) Obligation:

JBC Problem based on JBC Program:
package ClassAnalysisRec;

public class ClassAnalysisRec {
A field;

public static void main(String[] args) {
Random.args = args;
ClassAnalysisRec t = new ClassAnalysisRec();
t.field = new A();
t.field = new B();
t.eval();
}

public void eval() {
int x = Random.random() % 100;
this.field.test(x);
}
}

class A {
public boolean test(int x) {
return this.test(x-1);
}
}

class B extends A {
public boolean test(int x) {
if (x <= 0) return true;
return test(x - 1);
}
}


package ClassAnalysisRec;

public class Random {
static String[] args;
static int index = 0;

public static int random() {
final String string = args[index];
index++;
return string.length();
}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

ClassAnalysisRec.ClassAnalysisRec.eval()V: Graph of 82 nodes with 0 SCCs.

ClassAnalysisRec.B.test(I)Z: Graph of 20 nodes with 0 SCCs.


(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: ClassAnalysisRec.B.test(I)Z
SCC calls the following helper methods: ClassAnalysisRec.B.test(I)Z
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 11 IRules

P rules:
f247_0_test_GT(EOS, i24, i24, i24) → f252_0_test_GT(EOS, i24, i24, i24)
f252_0_test_GT(EOS, i24, i24, i24) → f256_0_test_Load(EOS, i24, i24) | >(i24, 0)
f256_0_test_Load(EOS, i24, i24) → f264_0_test_Load(EOS, i24, i24)
f264_0_test_Load(EOS, i24, i24) → f272_0_test_ConstantStackPush(EOS, i24, i24)
f272_0_test_ConstantStackPush(EOS, i24, i24) → f327_0_test_IntArithmetic(EOS, i24, i24, 1)
f327_0_test_IntArithmetic(EOS, i24, i24, matching1) → f334_0_test_InvokeMethod(EOS, i24, -(i24, 1)) | &&(>(i24, 0), =(matching1, 1))
f334_0_test_InvokeMethod(EOS, i24, i34) → f340_0_test_Load(EOS, i34, i34)
f334_0_test_InvokeMethod(EOS, i24, i34) → f340_1_test_Load(EOS, i24, i34, i34)
f340_0_test_Load(EOS, i34, i34) → f346_0_test_Load(EOS, i34, i34)
f346_0_test_Load(EOS, i34, i34) → f241_0_test_Load(EOS, i34, i34)
f241_0_test_Load(EOS, i21, i21) → f247_0_test_GT(EOS, i21, i21, i21)

Combined rules. Obtained 2 IRules

P rules:
f247_0_test_GT(EOS, x0, x0, x0) → f340_1_test_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f247_0_test_GT(EOS, x0, x0, x0) → f247_0_test_GT(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:


f247_0_test_GT(x1, x2, x3, x4) → f247_0_test_GT(x2, x3, x4)
Cond_f247_0_test_GT(x1, x2, x3, x4, x5) → Cond_f247_0_test_GT(x1, x3, x4, x5)
f340_1_test_Load(x1, x2, x3, x4) → f340_1_test_Load(x2, x3, x4)
Cond_f247_0_test_GT1(x1, x2, x3, x4, x5) → Cond_f247_0_test_GT1(x1, x3, x4, x5)

Filtered duplicate terms:


f247_0_test_GT(x1, x2, x3) → f247_0_test_GT(x3)
Cond_f247_0_test_GT(x1, x2, x3, x4) → Cond_f247_0_test_GT(x1, x4)
f340_1_test_Load(x1, x2, x3) → f340_1_test_Load(x3)
Cond_f247_0_test_GT1(x1, x2, x3, x4) → Cond_f247_0_test_GT1(x1, x4)

Filtered unneeded terms:


Cond_f247_0_test_GT(x1, x2) → Cond_f247_0_test_GT(x1)

Prepared 2 rules for path length conversion:

P rules:
f247_0_test_GT(x0) → f340_1_test_Load(-(x0, 1)) | >(x0, 0)
f247_0_test_GT(x0) → f247_0_test_GT(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

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

(6) Obligation:

Rules:
f247_0_test_GT(x1) → f247_0_test_GT(-(x1, 1)) | >(x1, 0)

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f247_0_test_GT(x2)] = x2

Therefore the following rule(s) have been dropped:


f247_0_test_GT(x0) → f247_0_test_GT(-(x0, 1)) | >(x0, 0)

(8) YES