Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class List1 {
	List1 pred, next;

	List1(List1 pred) {
		if (pred != null) {
			pred.next = this;
		}
		this.pred = pred;
	}

	static int length(List1 l) {
		int r = 1;
		while (null != (l = l.next))
			r++;
		return r;
	}

	public static void main(String[] args) {
		//Create doubly-linked list:
		int length = args.length;
		List1 cur = new List1(null);
		List1 first = cur;
		while (length-- > 0) {
			cur = new List1(cur);
		}

		length(first);		
	}
}



(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
List1.main([Ljava/lang/String;)V: Graph of 140 nodes with 2 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: List1.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • List1: [next]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f1575_0_length_Load(EOS, java.lang.Object(o1038sub), o1037) → f1577_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), o1037)
f1577_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), java.lang.Object(o1045sub)) → f1580_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), java.lang.Object(o1045sub))
f1580_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), java.lang.Object(o1045sub)) → f1588_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), java.lang.Object(o1045sub))
f1580_0_length_FieldAccess(EOS, java.lang.Object(o1048sub), java.lang.Object(o1048sub)) → f1589_0_length_FieldAccess(EOS, java.lang.Object(o1048sub), java.lang.Object(o1048sub))
f1588_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), java.lang.Object(List1(EOC, o1052))) → f1592_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), java.lang.Object(List1(EOC, o1052)))
f1592_0_length_FieldAccess(EOS, java.lang.Object(o1038sub), java.lang.Object(List1(EOC, o1052))) → f1597_0_length_Duplicate(EOS, java.lang.Object(o1038sub), o1052)
f1597_0_length_Duplicate(EOS, java.lang.Object(o1038sub), o1052) → f1602_0_length_Store(EOS, java.lang.Object(o1038sub), o1052, o1052)
f1602_0_length_Store(EOS, java.lang.Object(o1038sub), o1052, o1052) → f1608_0_length_EQ(EOS, java.lang.Object(o1038sub), o1052, o1052)
f1608_0_length_EQ(EOS, java.lang.Object(o1038sub), o1052, o1052) → f1613_0_length_Inc(EOS, java.lang.Object(o1038sub), o1052)
f1613_0_length_Inc(EOS, java.lang.Object(o1038sub), o1052) → f1618_0_length_JMP(EOS, java.lang.Object(o1038sub), o1052)
f1618_0_length_JMP(EOS, java.lang.Object(o1038sub), o1052) → f1627_0_length_ConstantStackPush(EOS, java.lang.Object(o1038sub), o1052)
f1627_0_length_ConstantStackPush(EOS, java.lang.Object(o1038sub), o1052) → f1573_0_length_ConstantStackPush(EOS, java.lang.Object(o1038sub), o1052)
f1573_0_length_ConstantStackPush(EOS, java.lang.Object(o1038sub), o1037) → f1575_0_length_Load(EOS, java.lang.Object(o1038sub), o1037)
f1589_0_length_FieldAccess(EOS, java.lang.Object(List1(EOC, o1055)), java.lang.Object(List1(EOC, o1055))) → f1594_0_length_FieldAccess(EOS, java.lang.Object(List1(EOC, o1055)), java.lang.Object(List1(EOC, o1055)))
f1594_0_length_FieldAccess(EOS, java.lang.Object(List1(EOC, o1055)), java.lang.Object(List1(EOC, o1055))) → f1600_0_length_Duplicate(EOS, java.lang.Object(List1(EOC, o1055)), o1055)
f1600_0_length_Duplicate(EOS, java.lang.Object(List1(EOC, o1055)), o1055) → f1605_0_length_Store(EOS, java.lang.Object(List1(EOC, o1055)), o1055, o1055)
f1605_0_length_Store(EOS, java.lang.Object(List1(EOC, o1055)), o1055, o1055) → f1610_0_length_EQ(EOS, java.lang.Object(List1(EOC, o1055)), o1055, o1055)
f1610_0_length_EQ(EOS, java.lang.Object(List1(EOC, o1055)), o1055, o1055) → f1616_0_length_Inc(EOS, java.lang.Object(List1(EOC, o1055)), o1055)
f1616_0_length_Inc(EOS, java.lang.Object(List1(EOC, o1055)), o1055) → f1620_0_length_JMP(EOS, java.lang.Object(List1(EOC, o1055)), o1055)
f1620_0_length_JMP(EOS, java.lang.Object(List1(EOC, o1055)), o1055) → f1632_0_length_ConstantStackPush(EOS, java.lang.Object(List1(EOC, o1055)), o1055)
f1632_0_length_ConstantStackPush(EOS, java.lang.Object(List1(EOC, o1055)), o1055) → f1573_0_length_ConstantStackPush(EOS, java.lang.Object(List1(EOC, o1055)), o1055)

Combined rules. Obtained 2 IRules

P rules:
f1575_0_length_Load(EOS, java.lang.Object(x0), java.lang.Object(List1(EOC, x1))) → f1575_0_length_Load(EOS, java.lang.Object(x0), x1)
f1575_0_length_Load(EOS, java.lang.Object(List1(EOC, x0)), java.lang.Object(List1(EOC, x0))) → f1575_0_length_Load(EOS, java.lang.Object(List1(EOC, x0)), x0)

Filtered ground terms:


f1575_0_length_Load(x1, x2, x3) → f1575_0_length_Load(x2, x3)
List1(x1, x2) → List1(x2)

Prepared 2 rules for path length conversion:

P rules:
f1575_0_length_Load(java.lang.Object(x0), java.lang.Object(List1(x1))) → f1575_0_length_Load(java.lang.Object(x0), x1)
f1575_0_length_Load(java.lang.Object(List1(x0)), java.lang.Object(List1(x0))) → f1575_0_length_Load(java.lang.Object(List1(x0)), x0)

Finished conversion. Obtained 2 rules.

P rules:
f1575_0_length_Load(v5, v6) → f1575_0_length_Load(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 1)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 1))
f1575_0_length_Load(v9, v10) → f1575_0_length_Load(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(7) Obligation:

Rules:
f1575_0_length_Load(v5, v6) → f1575_0_length_Load(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 1)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 1))
f1575_0_length_Load(v9, v10) → f1575_0_length_Load(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1575_0_length_Load(x9, x11)] = x11

Therefore the following rule(s) have been dropped:


f1575_0_length_Load(x0, x1) → f1575_0_length_Load(x2, x3) | &&(&&(&&(&&(&&(>(+(x3, 1), 0), <=(+(x3, 1), x1)), >(+(x2, 1), 1)), <=(x2, x0)), >(+(x1, 1), 1)), >(+(x0, 1), 1))
f1575_0_length_Load(x4, x5) → f1575_0_length_Load(x6, x7) | &&(&&(&&(&&(&&(&&(&&(>=(x4, +(x7, 1)), >=(x4, x6)), >(+(x4, 1), 1)), >(+(x7, 1), 0)), <=(+(x7, 1), x5)), >(+(x6, 1), 1)), <=(x6, x5)), >(+(x5, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: List1.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 44 IRules

P rules:
f1219_0_main_Inc(EOS, i77, i77) → f1221_0_main_LE(EOS, +(i77, -1), i77)
f1221_0_main_LE(EOS, i117, i121) → f1224_0_main_LE(EOS, i117, i121)
f1224_0_main_LE(EOS, i117, i121) → f1227_0_main_New(EOS, i117) | >(i121, 0)
f1227_0_main_New(EOS, i117) → f1231_0_main_Duplicate(EOS, i117)
f1231_0_main_Duplicate(EOS, i117) → f1234_0_main_Load(EOS, i117)
f1234_0_main_Load(EOS, i117) → f1235_0_main_InvokeMethod(EOS, i117)
f1235_0_main_InvokeMethod(EOS, i117) → f1238_0__init__Load(EOS, i117)
f1238_0__init__Load(EOS, i117) → f1244_0__init__InvokeMethod(EOS, i117)
f1244_0__init__InvokeMethod(EOS, i117) → f1248_0__init__Load(EOS, i117)
f1248_0__init__Load(EOS, i117) → f1251_0__init__NULL(EOS, i117)
f1251_0__init__NULL(EOS, i117) → f1255_0__init__Load(EOS, i117)
f1255_0__init__Load(EOS, i117) → f1258_0__init__Load(EOS, i117)
f1258_0__init__Load(EOS, i117) → f1261_0__init__FieldAccess(EOS, i117)
f1261_0__init__FieldAccess(EOS, i117) → f1271_0__init__FieldAccess(EOS, i117)
f1261_0__init__FieldAccess(EOS, i117) → f1272_0__init__FieldAccess(EOS, i117)
f1271_0__init__FieldAccess(EOS, i117) → f1290_0__init__FieldAccess(EOS, i117)
f1271_0__init__FieldAccess(EOS, i117) → f1291_0__init__FieldAccess(EOS, i117)
f1290_0__init__FieldAccess(EOS, i117) → f1296_0__init__FieldAccess(EOS, i117)
f1296_0__init__FieldAccess(EOS, i117) → f1312_0__init__Load(EOS, i117)
f1312_0__init__Load(EOS, i117) → f1323_0__init__Load(EOS, i117)
f1323_0__init__Load(EOS, i117) → f1336_0__init__FieldAccess(EOS, i117)
f1336_0__init__FieldAccess(EOS, i117) → f1353_0__init__Return(EOS, i117)
f1353_0__init__Return(EOS, i117) → f1362_0_main_Store(EOS, i117)
f1362_0_main_Store(EOS, i117) → f1368_0_main_JMP(EOS, i117)
f1368_0_main_JMP(EOS, i117) → f1380_0_main_Load(EOS, i117)
f1380_0_main_Load(EOS, i117) → f1096_0_main_Load(EOS, i117)
f1096_0_main_Load(EOS, i77) → f1219_0_main_Inc(EOS, i77, i77)
f1291_0__init__FieldAccess(EOS, i117) → f1299_0__init__Load(EOS, i117)
f1299_0__init__Load(EOS, i117) → f1314_0__init__Load(EOS, i117)
f1314_0__init__Load(EOS, i117) → f1325_0__init__FieldAccess(EOS, i117)
f1325_0__init__FieldAccess(EOS, i117) → f1337_0__init__Return(EOS, i117)
f1337_0__init__Return(EOS, i117) → f1354_0_main_Store(EOS, i117)
f1354_0_main_Store(EOS, i117) → f1363_0_main_JMP(EOS, i117)
f1363_0_main_JMP(EOS, i117) → f1369_0_main_Load(EOS, i117)
f1369_0_main_Load(EOS, i117) → f1096_0_main_Load(EOS, i117)
f1272_0__init__FieldAccess(EOS, i117) → f1293_0__init__FieldAccess(EOS, i117)
f1293_0__init__FieldAccess(EOS, i117) → f1304_0__init__Load(EOS, i117)
f1304_0__init__Load(EOS, i117) → f1316_0__init__Load(EOS, i117)
f1316_0__init__Load(EOS, i117) → f1328_0__init__FieldAccess(EOS, i117)
f1328_0__init__FieldAccess(EOS, i117) → f1340_0__init__Return(EOS, i117)
f1340_0__init__Return(EOS, i117) → f1356_0_main_Store(EOS, i117)
f1356_0_main_Store(EOS, i117) → f1364_0_main_JMP(EOS, i117)
f1364_0_main_JMP(EOS, i117) → f1370_0_main_Load(EOS, i117)
f1370_0_main_Load(EOS, i117) → f1096_0_main_Load(EOS, i117)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f1219_0_main_Inc(x1, x2, x3) → f1219_0_main_Inc(x2, x3)
Cond_f1219_0_main_Inc(x1, x2, x3, x4) → Cond_f1219_0_main_Inc(x1, x3, x4)

Filtered duplicate terms:


f1219_0_main_Inc(x1, x2) → f1219_0_main_Inc(x2)
Cond_f1219_0_main_Inc(x1, x2, x3) → Cond_f1219_0_main_Inc(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(12) Obligation:

Rules:
f1219_0_main_Inc(x0) → f1219_0_main_Inc(-(x0, 1)) | >(x0, 0)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1219_0_main_Inc(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(14) YES