Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 410 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 45 ms)
        ↳7 intTRS
        ↳8 TerminationGraphProcessor (⇒, 18 ms)
        ↳9 intTRS
        ↳10 PolynomialOrderProcessor (⇔, 0 ms)
        ↳11 YES
    ↳12 JBCTerminationSCC
        ↳13 SCCToIntTRSProof (⇒, 26 ms)
        ↳14 intTRS
        ↳15 PolynomialOrderProcessor (⇔, 6 ms)
        ↳16 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class List3 {
	private List3 next;

	void iterate() {
		List3 current = this.next;
	        while (current != this) {
	                current = current.next;
	        }
	}

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

		cur.iterate();
	}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
List3.main([Ljava/lang/String;)V: Graph of 105 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: List3.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • List3: [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 17 IRules

P rules:
f1085_0_iterate_Load(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) → f1098_0_iterate_EQ(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351)
f1098_0_iterate_EQ(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) → f1106_0_iterate_EQ(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) | &&(>(o351[List3.next]o349, 0), >(o351[List3.next]o351, 0))
f1106_0_iterate_EQ(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) → f1109_0_iterate_Load(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351)
f1109_0_iterate_Load(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) → f1112_0_iterate_FieldAccess(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351)
f1112_0_iterate_FieldAccess(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) → f1124_0_iterate_FieldAccess(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) | &&(&&(&&(>(o350[List3.next]o351, 0), >(o350[List3.next]o350, 0)), >(o351[List3.next]o350, 0)), >(o351[List3.next]o351, 0))
f1112_0_iterate_FieldAccess(EOS, o389[List3.next]o349, o389[List3.next]o349, o350[List3.next]o351, o389[List3.next]o389, o351[List3.next]o350, o389[List3.next]o389) → f1125_0_iterate_FieldAccess(EOS, o389[List3.next]o349, o389[List3.next]o389)
f1124_0_iterate_FieldAccess(EOS, o350[List3.next]o349, o390[List3.next]o349, o350[List3.next]o390, o350[List3.next]o350, o390[List3.next]o350, o390[List3.next]o390) → f1129_0_iterate_FieldAccess(EOS, o350[List3.next]o349, o350[List3.next]o350, o350[List3.next]o390, o391[List3.next]o349, o391[List3.next]o350, o391[List3.next]o390) | &&(&&(=(o391[List3.next]o349, +(o390[List3.next]o349, -1)), =(o391[List3.next]o350, +(o390[List3.next]o350, -1))), =(o391[List3.next]o390, +(o390[List3.next]o390, -1)))
f1129_0_iterate_FieldAccess(EOS, o350[List3.next]o349, o350[List3.next]o350, o350[List3.next]o390, o391[List3.next]o349, o391[List3.next]o350, o391[List3.next]o390) → f1132_0_iterate_Store(EOS, o350[List3.next]o349, o350[List3.next]o350, o391[List3.next]o349, o391[List3.next]o350, o350[List3.next]o391, o391[List3.next]o391)
f1132_0_iterate_Store(EOS, o350[List3.next]o349, o350[List3.next]o350, o391[List3.next]o349, o391[List3.next]o350, o350[List3.next]o391, o391[List3.next]o391) → f1136_0_iterate_JMP(EOS, o350[List3.next]o349, o350[List3.next]o350, o391[List3.next]o349, o391[List3.next]o350, o350[List3.next]o391, o391[List3.next]o391)
f1136_0_iterate_JMP(EOS, o350[List3.next]o349, o350[List3.next]o350, o391[List3.next]o349, o391[List3.next]o350, o350[List3.next]o391, o391[List3.next]o391) → f1156_0_iterate_Load(EOS, o350[List3.next]o349, o350[List3.next]o350, o391[List3.next]o349, o391[List3.next]o350, o350[List3.next]o391, o391[List3.next]o391)
f1156_0_iterate_Load(EOS, o350[List3.next]o349, o350[List3.next]o350, o391[List3.next]o349, o391[List3.next]o350, o350[List3.next]o391, o391[List3.next]o391) → f1082_0_iterate_Load(EOS, o350[List3.next]o349, o391[List3.next]o349, o350[List3.next]o391, o350[List3.next]o350, o391[List3.next]o350, o391[List3.next]o391)
f1082_0_iterate_Load(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351) → f1085_0_iterate_Load(EOS, o350[List3.next]o349, o351[List3.next]o349, o350[List3.next]o351, o350[List3.next]o350, o351[List3.next]o350, o351[List3.next]o351)
f1125_0_iterate_FieldAccess(EOS, o392[List3.next]o349, o392[List3.next]o392) → f1130_0_iterate_FieldAccess(EOS, o393[List3.next]o349, o393[List3.next]o392) | &&(=(o393[List3.next]o349, +(o392[List3.next]o349, -1)), =(o393[List3.next]o392, +(o392[List3.next]o392, -1)))
f1130_0_iterate_FieldAccess(EOS, o393[List3.next]o349, o393[List3.next]o392) → f1134_0_iterate_Store(EOS, o393[List3.next]o349, o393[List3.next]o392)
f1134_0_iterate_Store(EOS, o393[List3.next]o349, o393[List3.next]o392) → f1138_0_iterate_JMP(EOS, o393[List3.next]o349, o393[List3.next]o392)
f1138_0_iterate_JMP(EOS, o393[List3.next]o349, o393[List3.next]o392) → f1174_0_iterate_Load(EOS, o393[List3.next]o349, o393[List3.next]o392)
f1174_0_iterate_Load(EOS, o393[List3.next]o349, o393[List3.next]o392) → f1082_0_iterate_Load(EOS, o392[List3.next]o349, o393[List3.next]o349, o392[List3.next]o393, o392[List3.next]o392, o393[List3.next]o392, o393[List3.next]o393) | &&(&&(=(o392[List3.next]o393, 1), =(o392[List3.next]o392, 0)), =(o393[List3.next]o393, 0))

Combined rules. Obtained 2 IRules

P rules:
f1085_0_iterate_Load(EOS, x0, x1, x2, x3, x4, x5) → f1085_0_iterate_Load(EOS, x0, -(x1, 1), x7, x3, -(x4, 1), x9) | &&(&&(&&(&&(>(x5, 0), >(x4, 0)), >(x3, 0)), >(x1, 0)), >(x2, 0))
f1085_0_iterate_Load(EOS, x0, x0, x1, x2, x3, x2) → f1085_0_iterate_Load(EOS, x4, -(x0, 1), 1, 0, -(x2, 1), 0) | &&(>(x0, 0), >(x2, 0))

Filtered ground terms:


f1085_0_iterate_Load(x1, x2, x3, x4, x5, x6, x7) → f1085_0_iterate_Load(x2, x3, x4, x5, x6, x7)
Cond_f1085_0_iterate_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f1085_0_iterate_Load(x1, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f1085_0_iterate_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1085_0_iterate_Load1(x1, x3, x4, x5, x6, x7, x8, x9)

Filtered duplicate terms:


Cond_f1085_0_iterate_Load1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1085_0_iterate_Load1(x1, x3, x4, x6, x7, x8)

Filtered unneeded terms:


Cond_f1085_0_iterate_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1085_0_iterate_Load(x1, x2, x3, x5, x6, x8, x9)
Cond_f1085_0_iterate_Load1(x1, x2, x3, x4, x5, x6) → Cond_f1085_0_iterate_Load1(x1, x2, x5, x6)

Prepared 2 rules for path length conversion:

P rules:
f1085_0_iterate_Load(x0, x1, x2, x3, x4, x5) → f1085_0_iterate_Load(x0, -(x1, 1), x7, x3, -(x4, 1), x9) | &&(&&(&&(&&(>(x5, 0), >(x4, 0)), >(x3, 0)), >(x1, 0)), >(x2, 0))
f1085_0_iterate_Load(x0, x0, x1, x2, x3, x2) → f1085_0_iterate_Load(x4, -(x0, 1), 1, 0, -(x2, 1), 0) | &&(>(x0, 0), >(x2, 0))

Finished conversion. Obtained 2 rules.

P rules:
f1085_0_iterate_Load(x0, x1, x2, x3, x4, x5) → f1085_0_iterate_Load(x0, -(x1, 1), x6, x3, -(x4, 1), x7) | &&(&&(&&(&&(>(x5, 0), >(x4, 0)), >(x3, 0)), >(x1, 0)), >(x2, 0))
f1085_0_iterate_Load(x8, x81, x9, x10, x11, x101) → f1085_0_iterate_Load(x12, -(x8, 1), 1, 0, -(x10, 1), 0) | &&(&&(&&(>(x10, 0), >(x8, 0)), =(x8, x81)), =(x10, x101))

(7) Obligation:

Rules:
f1085_0_iterate_Load(x0, x1, x2, x3, x4, x5) → f1085_0_iterate_Load(x0, -(x1, 1), x6, x3, -(x4, 1), x7) | &&(&&(&&(&&(>(x5, 0), >(x4, 0)), >(x3, 0)), >(x1, 0)), >(x2, 0))
f1085_0_iterate_Load(x8, x81, x9, x10, x11, x101) → f1085_0_iterate_Load(x12, -(x8, 1), 1, 0, -(x10, 1), 0) | &&(&&(&&(>(x10, 0), >(x8, 0)), =(x8, x81)), =(x10, x101))

(8) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained one non-trivial SCC.


(9) Obligation:

Rules:
f1085_0_iterate_Load(x0, x1, x2, x3, x4, x5) → f1085_0_iterate_Load(x0, -(x1, 1), x6, x3, -(x4, 1), x7) | &&(&&(&&(&&(>(x5, 0), >(x4, 0)), >(x3, 0)), >(x1, 0)), >(x2, 0))

(10) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1085_0_iterate_Load(x9, x11, x13, x15, x17, x19)] = x11

Therefore the following rule(s) have been dropped:


f1085_0_iterate_Load(x0, x1, x2, x3, x4, x5) → f1085_0_iterate_Load(x0, -(x1, 1), x6, x3, -(x4, 1), x7) | &&(&&(&&(&&(>(x5, 0), >(x4, 0)), >(x3, 0)), >(x1, 0)), >(x2, 0))

(11) YES

(12) Obligation:

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

(13) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 25 IRules

P rules:
f636_0_main_Inc(EOS, i52, i52, o163[List3.next]o162) → f639_0_main_LE(EOS, +(i52, -1), i52, o163[List3.next]o162)
f639_0_main_LE(EOS, i57, i61, o163[List3.next]o162) → f642_0_main_LE(EOS, i57, i61, o163[List3.next]o162)
f642_0_main_LE(EOS, i57, i61, o163[List3.next]o162) → f646_0_main_Load(EOS, i57, o163[List3.next]o162) | >(i61, 0)
f646_0_main_Load(EOS, i57, o163[List3.next]o162) → f650_0_main_New(EOS, i57, o163[List3.next]o162)
f650_0_main_New(EOS, i57, o163[List3.next]o162) → f652_0_main_Duplicate(EOS, i57, o163[List3.next]o162)
f652_0_main_Duplicate(EOS, i57, o163[List3.next]o162) → f662_0_main_InvokeMethod(EOS, i57, o163[List3.next]o162)
f662_0_main_InvokeMethod(EOS, i57, o163[List3.next]o162) → f671_0__init__Load(EOS, i57, o163[List3.next]o162)
f671_0__init__Load(EOS, i57, o163[List3.next]o162) → f683_0__init__InvokeMethod(EOS, i57, o163[List3.next]o162)
f683_0__init__InvokeMethod(EOS, i57, o163[List3.next]o162) → f686_0__init__Return(EOS, i57, o163[List3.next]o162)
f686_0__init__Return(EOS, i57, o163[List3.next]o162) → f690_0_main_FieldAccess(EOS, i57, o163[List3.next]o162)
f690_0_main_FieldAccess(EOS, i57, o163[List3.next]o162) → f705_0_main_FieldAccess(EOS, i57, o163[List3.next]o162) | >(o163[List3.next]o162, 0)
f690_0_main_FieldAccess(EOS, i57, o163[List3.next]o162) → f706_0_main_FieldAccess(EOS, i57)
f705_0_main_FieldAccess(EOS, i57, o163[List3.next]o162) → f715_0_main_Load(EOS, i57, o163[List3.next]o162)
f715_0_main_Load(EOS, i57, o163[List3.next]o162) → f727_0_main_FieldAccess(EOS, i57, o163[List3.next]o162)
f727_0_main_FieldAccess(EOS, i57, o163[List3.next]o162) → f737_0_main_Store(EOS, i57, o163[List3.next]o169)
f737_0_main_Store(EOS, i57, o163[List3.next]o169) → f745_0_main_JMP(EOS, i57, o163[List3.next]o169)
f745_0_main_JMP(EOS, i57, o163[List3.next]o169) → f770_0_main_Load(EOS, i57, o163[List3.next]o169)
f770_0_main_Load(EOS, i57, o163[List3.next]o169) → f631_0_main_Load(EOS, i57, o163[List3.next]o169)
f631_0_main_Load(EOS, i52, o163[List3.next]o162) → f636_0_main_Inc(EOS, i52, i52, o163[List3.next]o162)
f706_0_main_FieldAccess(EOS, i57) → f720_0_main_Load(EOS, i57)
f720_0_main_Load(EOS, i57) → f729_0_main_FieldAccess(EOS, i57)
f729_0_main_FieldAccess(EOS, i57) → f739_0_main_Store(EOS, i57)
f739_0_main_Store(EOS, i57) → f748_0_main_JMP(EOS, i57)
f748_0_main_JMP(EOS, i57) → f776_0_main_Load(EOS, i57)
f776_0_main_Load(EOS, i57) → f631_0_main_Load(EOS, i57, o190[List3.next]o169) | =(o190[List3.next]o169, 1)

Combined rules. Obtained 2 IRules

P rules:
f636_0_main_Inc(EOS, x0, x0, x1) → f636_0_main_Inc(EOS, -(x0, 1), -(x0, 1), x2) | &&(>(x0, 0), >(x1, 0))
f636_0_main_Inc(EOS, x0, x0, x1) → f636_0_main_Inc(EOS, -(x0, 1), -(x0, 1), 1) | >(x0, 0)

Filtered ground terms:


f636_0_main_Inc(x1, x2, x3, x4) → f636_0_main_Inc(x2, x3, x4)
Cond_f636_0_main_Inc(x1, x2, x3, x4, x5, x6) → Cond_f636_0_main_Inc(x1, x3, x4, x5, x6)
Cond_f636_0_main_Inc1(x1, x2, x3, x4, x5) → Cond_f636_0_main_Inc1(x1, x3, x4, x5)

Filtered duplicate terms:


f636_0_main_Inc(x1, x2, x3) → f636_0_main_Inc(x2, x3)
Cond_f636_0_main_Inc(x1, x2, x3, x4, x5) → Cond_f636_0_main_Inc(x1, x3, x4, x5)
Cond_f636_0_main_Inc1(x1, x2, x3, x4) → Cond_f636_0_main_Inc1(x1, x3, x4)

Filtered unneeded terms:


Cond_f636_0_main_Inc(x1, x2, x3, x4) → Cond_f636_0_main_Inc(x1, x2, x4)
Cond_f636_0_main_Inc1(x1, x2, x3) → Cond_f636_0_main_Inc1(x1, x2)

Prepared 2 rules for path length conversion:

P rules:
f636_0_main_Inc(x0, x1) → f636_0_main_Inc(-(x0, 1), x2) | &&(>(x0, 0), >(x1, 0))
f636_0_main_Inc(x0, x1) → f636_0_main_Inc(-(x0, 1), 1) | >(x0, 0)

Finished conversion. Obtained 2 rules.

P rules:
f636_0_main_Inc(x0, x1) → f636_0_main_Inc(-(x0, 1), x2) | &&(>(x0, 0), >(x1, 0))
f636_0_main_Inc(x3, x4) → f636_0_main_Inc(-(x3, 1), 1) | >(x3, 0)

(14) Obligation:

Rules:
f636_0_main_Inc(x0, x1) → f636_0_main_Inc(-(x0, 1), x2) | &&(>(x0, 0), >(x1, 0))
f636_0_main_Inc(x3, x4) → f636_0_main_Inc(-(x3, 1), 1) | >(x3, 0)

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f636_0_main_Inc(x6, x8)] = x6

Therefore the following rule(s) have been dropped:


f636_0_main_Inc(x0, x1) → f636_0_main_Inc(-(x0, 1), x2) | &&(>(x0, 0), >(x1, 0))
f636_0_main_Inc(x3, x4) → f636_0_main_Inc(-(x3, 1), 1) | >(x3, 0)

(16) YES