Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 786 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 56 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇔, 0 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 73 ms)
        ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇔, 0 ms)
        ↳14 YES

(0) Obligation:

JBC Problem based on JBC Program:
package CyclicAnalysisRec;

public class CyclicAnalysisRec {
	CyclicAnalysisRec field;

	public static void main(String[] args) {
		Random.args = args;
		CyclicAnalysisRec t = new CyclicAnalysisRec();
		t.field = new CyclicAnalysisRec();
		t.field.appendNewCyclicList(Random.random());
		t.appendNewList(Random.random());
		t.length();
	}

	public int length() {
		if (this.field == null) return 1;
		else return 1 + this.field.length();
	}

	public void appendNewCyclicList(int i) {
		CyclicAnalysisRec last = this.appendNewList(i);
		last.field = this;
	}

	/**
 	 * @param i number of elements to append
 	 * @return the last list element appended
 	 */
	private CyclicAnalysisRec appendNewList(int i) {
		this.field = new CyclicAnalysisRec();
		if (i <= 1) {
			return this.field;
		} else {
			return this.field.appendNewList(i-1);
		}
	}
}


package CyclicAnalysisRec;

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:
CyclicAnalysisRec.CyclicAnalysisRec.main([Ljava/lang/String;)V: Graph of 314 nodes with 0 SCCs.

CyclicAnalysisRec.CyclicAnalysisRec.appendNewList(I)LCyclicAnalysisRec/CyclicAnalysisRec;: Graph of 33 nodes with 0 SCCs.

CyclicAnalysisRec.CyclicAnalysisRec.length()I: Graph of 28 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicAnalysisRec.CyclicAnalysisRec.length()I
SCC calls the following helper methods: CyclicAnalysisRec.CyclicAnalysisRec.length()I
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • CyclicAnalysisRec.CyclicAnalysisRec: [field]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 12 IRules

P rules:
f1797_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930))) → f1804_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)))
f1804_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930))) → f1808_0_length_NONNULL(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o930)), o930)
f1808_0_length_NONNULL(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(o941sub)) → f1811_0_length_NONNULL(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(o941sub))
f1811_0_length_NONNULL(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(o941sub)) → f1815_0_length_ConstantStackPush(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))))
f1815_0_length_ConstantStackPush(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub)))) → f1829_0_length_Load(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))))
f1829_0_length_Load(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub)))) → f1837_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))))
f1837_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub)))) → f1851_0_length_InvokeMethod(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(o941sub))
f1851_0_length_InvokeMethod(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(o941sub)) → f1853_0_length_Load(EOS, java.lang.Object(o941sub), java.lang.Object(o941sub))
f1851_0_length_InvokeMethod(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(o941sub)) → f1853_1_length_Load(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o941sub))), java.lang.Object(o941sub), java.lang.Object(o941sub))
f1853_0_length_Load(EOS, java.lang.Object(o941sub), java.lang.Object(o941sub)) → f1855_0_length_Load(EOS, java.lang.Object(o941sub), java.lang.Object(o941sub))
f1855_0_length_Load(EOS, java.lang.Object(o941sub), java.lang.Object(o941sub)) → f1791_0_length_Load(EOS, java.lang.Object(o941sub), java.lang.Object(o941sub))
f1791_0_length_Load(EOS, java.lang.Object(o912sub), java.lang.Object(o912sub)) → f1797_0_length_FieldAccess(EOS, java.lang.Object(o912sub), java.lang.Object(o912sub), java.lang.Object(o912sub))

Combined rules. Obtained 2 IRules

P rules:
f1797_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0)))) → f1853_1_length_Load(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0))), java.lang.Object(x0), java.lang.Object(x0))
f1797_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0)))) → f1797_0_length_FieldAccess(EOS, java.lang.Object(x0), java.lang.Object(x0), java.lang.Object(x0))

Filtered ground terms:


f1797_0_length_FieldAccess(x1, x2, x3, x4) → f1797_0_length_FieldAccess(x2, x3, x4)
f1853_1_length_Load(x1, x2, x3, x4) → f1853_1_length_Load(x2, x3, x4)
CyclicAnalysisRec.CyclicAnalysisRec(x1, x2) → CyclicAnalysisRec.CyclicAnalysisRec(x2)

Filtered duplicate terms:


f1797_0_length_FieldAccess(x1, x2, x3) → f1797_0_length_FieldAccess(x3)
f1853_1_length_Load(x1, x2, x3) → f1853_1_length_Load(x1)

Prepared 2 rules for path length conversion:

P rules:
f1797_0_length_FieldAccess(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0)))) → f1853_1_length_Load(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0))))
f1797_0_length_FieldAccess(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0)))) → f1797_0_length_FieldAccess(java.lang.Object(x0))

Finished conversion. Obtained 1 rules.

P rules:
f1797_0_length_FieldAccess(v3) → f1797_0_length_FieldAccess(v4) | &&(&&(>(+(v4, 1), 1), <=(+(v4, 2), v3)), >(+(v3, 1), 3))

(7) Obligation:

Rules:
f1797_0_length_FieldAccess(v3) → f1797_0_length_FieldAccess(v4) | &&(&&(>(+(v4, 1), 1), <=(+(v4, 2), v3)), >(+(v3, 1), 3))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1797_0_length_FieldAccess(x3)] = x3

Therefore the following rule(s) have been dropped:


f1797_0_length_FieldAccess(x0) → f1797_0_length_FieldAccess(x1) | &&(&&(>(+(x1, 1), 1), <=(+(x1, 2), x0)), >(+(x0, 1), 3))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicAnalysisRec.CyclicAnalysisRec.appendNewList(I)LCyclicAnalysisRec/CyclicAnalysisRec;
SCC calls the following helper methods: CyclicAnalysisRec.CyclicAnalysisRec.appendNewList(I)LCyclicAnalysisRec/CyclicAnalysisRec;
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • CyclicAnalysisRec.CyclicAnalysisRec: [field]
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f1027_0_appendNewList_New(EOS, i190, i190) → f1035_0_appendNewList_Duplicate(EOS, i190, i190)
f1035_0_appendNewList_Duplicate(EOS, i190, i190) → f1041_0_appendNewList_InvokeMethod(EOS, i190, i190)
f1041_0_appendNewList_InvokeMethod(EOS, i190, i190) → f1045_0__init__Load(EOS, i190, i190)
f1045_0__init__Load(EOS, i190, i190) → f1049_0__init__InvokeMethod(EOS, i190, i190)
f1049_0__init__InvokeMethod(EOS, i190, i190) → f1061_0__init__Return(EOS, i190, i190)
f1061_0__init__Return(EOS, i190, i190) → f1066_0_appendNewList_FieldAccess(EOS, i190, i190)
f1066_0_appendNewList_FieldAccess(EOS, i190, i190) → f1071_0_appendNewList_Load(EOS, i190, i190)
f1071_0_appendNewList_Load(EOS, i190, i190) → f1073_0_appendNewList_ConstantStackPush(EOS, i190, i190, i190)
f1073_0_appendNewList_ConstantStackPush(EOS, i190, i190, i190) → f1079_0_appendNewList_GT(EOS, i190, i190, i190, 1)
f1079_0_appendNewList_GT(EOS, i205, i205, i205, matching1) → f1086_0_appendNewList_GT(EOS, i205, i205, i205, 1) | =(matching1, 1)
f1086_0_appendNewList_GT(EOS, i205, i205, i205, matching1) → f1096_0_appendNewList_Load(EOS, i205, i205) | &&(>(i205, 1), =(matching1, 1))
f1096_0_appendNewList_Load(EOS, i205, i205) → f1102_0_appendNewList_FieldAccess(EOS, i205, i205)
f1102_0_appendNewList_FieldAccess(EOS, i205, i205) → f1113_0_appendNewList_Load(EOS, i205, i205)
f1113_0_appendNewList_Load(EOS, i205, i205) → f1119_0_appendNewList_ConstantStackPush(EOS, i205, i205)
f1119_0_appendNewList_ConstantStackPush(EOS, i205, i205) → f1160_0_appendNewList_IntArithmetic(EOS, i205, i205, 1)
f1160_0_appendNewList_IntArithmetic(EOS, i205, i205, matching1) → f1162_0_appendNewList_InvokeMethod(EOS, i205, -(i205, 1)) | &&(>(i205, 0), =(matching1, 1))
f1162_0_appendNewList_InvokeMethod(EOS, i205, i224) → f1175_0_appendNewList_Load(EOS, i224, i224)
f1162_0_appendNewList_InvokeMethod(EOS, i205, i224) → f1175_1_appendNewList_Load(EOS, i205, i224, i224)
f1175_0_appendNewList_Load(EOS, i224, i224) → f1177_0_appendNewList_Load(EOS, i224, i224)
f1177_0_appendNewList_Load(EOS, i224, i224) → f1023_0_appendNewList_Load(EOS, i224, i224)
f1023_0_appendNewList_Load(EOS, i190, i190) → f1027_0_appendNewList_New(EOS, i190, i190)

Combined rules. Obtained 2 IRules

P rules:
f1027_0_appendNewList_New(EOS, x0, x0) → f1175_1_appendNewList_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 1)
f1027_0_appendNewList_New(EOS, x0, x0) → f1027_0_appendNewList_New(EOS, -(x0, 1), -(x0, 1)) | >(x0, 1)

Filtered ground terms:


f1027_0_appendNewList_New(x1, x2, x3) → f1027_0_appendNewList_New(x2, x3)
Cond_f1027_0_appendNewList_New(x1, x2, x3, x4) → Cond_f1027_0_appendNewList_New(x1, x3, x4)
f1175_1_appendNewList_Load(x1, x2, x3, x4) → f1175_1_appendNewList_Load(x2, x3, x4)
Cond_f1027_0_appendNewList_New1(x1, x2, x3, x4) → Cond_f1027_0_appendNewList_New1(x1, x3, x4)

Filtered duplicate terms:


f1027_0_appendNewList_New(x1, x2) → f1027_0_appendNewList_New(x2)
Cond_f1027_0_appendNewList_New(x1, x2, x3) → Cond_f1027_0_appendNewList_New(x1, x3)
f1175_1_appendNewList_Load(x1, x2, x3) → f1175_1_appendNewList_Load(x3)
Cond_f1027_0_appendNewList_New1(x1, x2, x3) → Cond_f1027_0_appendNewList_New1(x1, x3)

Filtered unneeded terms:


Cond_f1027_0_appendNewList_New(x1, x2) → Cond_f1027_0_appendNewList_New(x1)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(12) Obligation:

Rules:
f1027_0_appendNewList_New(x1) → f1027_0_appendNewList_New(-(x1, 1)) | >(x1, 1)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1027_0_appendNewList_New(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(14) YES