Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class ListReverseAcyclicList {
	public static void main(String... args) {
		List x = List.createList(args[0].length(), null);
		List.reverse(x);
	}
}

class List {
	List n;

	public List(List next) {
		this.n = next;
	}

	public static void reverse(List x) {		
		List y = null;
		while (x != null) {
			List z = x;
			x = x.n;
			z.n = y;
			y = z;
		}
	}

	public static List createList(int l, List end) {
		while (--l > 0) {
			end = new List(end);
		}
		return end;
	}

	public static List createCycle(int l) {
		List last = new List(null);
		List first = createList(l - 1, last);
		last.n = first;
		return first;
	}

	public static List createPanhandleList(int pl, int cl) {
		return createList(pl, createCycle(cl));
	}

}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 30 IRules

P rules:
f752_0_reverse_NULL(EOS, o150, java.lang.Object(o160sub), o149, java.lang.Object(o160sub)) → f755_0_reverse_NULL(EOS, o150, java.lang.Object(o160sub), o149, java.lang.Object(o160sub))
f755_0_reverse_NULL(EOS, o150, java.lang.Object(o160sub), o149, java.lang.Object(o160sub)) → f758_0_reverse_Load(EOS, o150, java.lang.Object(o160sub), o149)
f758_0_reverse_Load(EOS, o150, java.lang.Object(o160sub), o149) → f767_0_reverse_Store(EOS, o150, java.lang.Object(o160sub), o149, java.lang.Object(o160sub))
f767_0_reverse_Store(EOS, o150, java.lang.Object(o160sub), o149, java.lang.Object(o160sub)) → f778_0_reverse_Store(EOS, o150, java.lang.Object(o160sub), o149, java.lang.Object(o160sub))
f767_0_reverse_Store(EOS, java.lang.Object(o166sub), java.lang.Object(o166sub), o149, java.lang.Object(o166sub)) → f779_0_reverse_Store(EOS, java.lang.Object(o166sub), java.lang.Object(o166sub), o149, java.lang.Object(o166sub))
f778_0_reverse_Store(EOS, o150, java.lang.Object(List(EOC, o168)), o149, java.lang.Object(List(EOC, o168))) → f783_0_reverse_Store(EOS, o150, java.lang.Object(List(EOC, o168)), o149, java.lang.Object(List(EOC, o168)))
f783_0_reverse_Store(EOS, o150, java.lang.Object(List(EOC, o168)), o149, java.lang.Object(List(EOC, o168))) → f785_0_reverse_Load(EOS, o150, java.lang.Object(List(EOC, o168)), o149, java.lang.Object(List(EOC, o168)))
f785_0_reverse_Load(EOS, o150, java.lang.Object(List(EOC, o168)), o149, java.lang.Object(List(EOC, o168))) → f789_0_reverse_FieldAccess(EOS, o150, o149, java.lang.Object(List(EOC, o168)), java.lang.Object(List(EOC, o168)))
f789_0_reverse_FieldAccess(EOS, o150, o149, java.lang.Object(List(EOC, o168)), java.lang.Object(List(EOC, o168))) → f795_0_reverse_Store(EOS, o150, o149, java.lang.Object(List(EOC, o168)), o168)
f795_0_reverse_Store(EOS, o150, o149, java.lang.Object(List(EOC, o168)), o168) → f800_0_reverse_Load(EOS, o150, o168, o149, java.lang.Object(List(EOC, o168)))
f800_0_reverse_Load(EOS, o150, o168, o149, java.lang.Object(List(EOC, o168))) → f805_0_reverse_Load(EOS, o150, o168, o149, java.lang.Object(List(EOC, o168)), java.lang.Object(List(EOC, o168)))
f805_0_reverse_Load(EOS, o150, o168, o149, java.lang.Object(List(EOC, o168)), java.lang.Object(List(EOC, o168))) → f810_0_reverse_FieldAccess(EOS, o150, o168, java.lang.Object(List(EOC, o168)), java.lang.Object(List(EOC, o168)), o149)
f810_0_reverse_FieldAccess(EOS, o150, o168, java.lang.Object(List(EOC, o168)), java.lang.Object(List(EOC, o168)), o149) → f817_0_reverse_Load(EOS, o150, o168, java.lang.Object(List(EOC, o149)))
f817_0_reverse_Load(EOS, o150, o168, java.lang.Object(List(EOC, o149))) → f822_0_reverse_Store(EOS, o150, o168, java.lang.Object(List(EOC, o149)))
f822_0_reverse_Store(EOS, o150, o168, java.lang.Object(List(EOC, o149))) → f826_0_reverse_JMP(EOS, o150, o168, java.lang.Object(List(EOC, o149)))
f826_0_reverse_JMP(EOS, o150, o168, java.lang.Object(List(EOC, o149))) → f834_0_reverse_Load(EOS, o150, o168, java.lang.Object(List(EOC, o149)))
f834_0_reverse_Load(EOS, o150, o168, java.lang.Object(List(EOC, o149))) → f749_0_reverse_Load(EOS, o150, o168, java.lang.Object(List(EOC, o149)))
f749_0_reverse_Load(EOS, o150, o148, o149) → f752_0_reverse_NULL(EOS, o150, o148, o149, o148)
f779_0_reverse_Store(EOS, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170))) → f784_0_reverse_Store(EOS, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170)))
f784_0_reverse_Store(EOS, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170))) → f787_0_reverse_Load(EOS, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170)))
f787_0_reverse_Load(EOS, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170))) → f792_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)))
f792_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170))) → f798_0_reverse_Store(EOS, java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170)), o170)
f798_0_reverse_Store(EOS, java.lang.Object(List(EOC, o170)), o149, java.lang.Object(List(EOC, o170)), o170) → f803_0_reverse_Load(EOS, java.lang.Object(List(EOC, o170)), o170, o149, java.lang.Object(List(EOC, o170)))
f803_0_reverse_Load(EOS, java.lang.Object(List(EOC, o170)), o170, o149, java.lang.Object(List(EOC, o170))) → f808_0_reverse_Load(EOS, java.lang.Object(List(EOC, o170)), o170, o149, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)))
f808_0_reverse_Load(EOS, java.lang.Object(List(EOC, o170)), o170, o149, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170))) → f813_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o170)), o170, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)), o149)
f813_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o170)), o170, java.lang.Object(List(EOC, o170)), java.lang.Object(List(EOC, o170)), o149) → f821_0_reverse_Load(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149)))
f821_0_reverse_Load(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149))) → f824_0_reverse_Store(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149)))
f824_0_reverse_Store(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149))) → f828_0_reverse_JMP(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149)))
f828_0_reverse_JMP(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149))) → f841_0_reverse_Load(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149)))
f841_0_reverse_Load(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149))) → f749_0_reverse_Load(EOS, java.lang.Object(List(EOC, o149)), o170, java.lang.Object(List(EOC, o149)))

Combined rules. Obtained 2 IRules

P rules:
f752_0_reverse_NULL(EOS, x0, java.lang.Object(List(EOC, x1)), x2, java.lang.Object(List(EOC, x1))) → f752_0_reverse_NULL(EOS, x0, x1, java.lang.Object(List(EOC, x2)), x1)
f752_0_reverse_NULL(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), x1, java.lang.Object(List(EOC, x0))) → f752_0_reverse_NULL(EOS, java.lang.Object(List(EOC, x1)), x0, java.lang.Object(List(EOC, x1)), x0)

Filtered ground terms:


f752_0_reverse_NULL(x1, x2, x3, x4, x5) → f752_0_reverse_NULL(x2, x3, x4, x5)
List(x1, x2) → List(x2)

Filtered duplicate terms:


f752_0_reverse_NULL(x1, x2, x3, x4) → f752_0_reverse_NULL(x1, x3, x4)

Prepared 2 rules for path length conversion:

P rules:
f752_0_reverse_NULL(x0, x2, java.lang.Object(List(x1))) → f752_0_reverse_NULL(x0, java.lang.Object(List(x2)), x1)
f752_0_reverse_NULL(java.lang.Object(List(x0)), x1, java.lang.Object(List(x0))) → f752_0_reverse_NULL(java.lang.Object(List(x1)), java.lang.Object(List(x1)), x0)

Finished conversion. Obtained 2 rules.

P rules:
f752_0_reverse_NULL(v8, v9, v10) → f752_0_reverse_NULL(v11, v12, v13) | &&(&&(&&(&&(&&(&&(&&(&&(>=(v9, -(v12, 2)), >(+(v9, 1), 0)), >=(v8, v11)), >(+(v8, 1), 0)), >(+(v13, 1), 0)), <=(+(v13, 1), v10)), >(+(v12, 1), 1)), >(+(v11, 1), 0)), >(+(v10, 1), 1))
f752_0_reverse_NULL(v14, v15, v16) → f752_0_reverse_NULL(v17, v18, v19) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v19, 1), 0), <=(+(v19, 1), v16)), <=(+(v19, 1), v14)), >(+(v18, 1), 1)), <=(-(v18, 2), v15)), >(+(v17, 1), 1)), <=(-(v17, 2), v15)), >(+(v16, 1), 1)), >(+(v15, 1), 0)), >(+(v14, 1), 1))

(7) Obligation:

Rules:
f752_0_reverse_NULL(v8, v9, v10) → f752_0_reverse_NULL(v11, v12, v13) | &&(&&(&&(&&(&&(&&(&&(&&(>=(v9, -(v12, 2)), >(+(v9, 1), 0)), >=(v8, v11)), >(+(v8, 1), 0)), >(+(v13, 1), 0)), <=(+(v13, 1), v10)), >(+(v12, 1), 1)), >(+(v11, 1), 0)), >(+(v10, 1), 1))
f752_0_reverse_NULL(v14, v15, v16) → f752_0_reverse_NULL(v17, v18, v19) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v19, 1), 0), <=(+(v19, 1), v16)), <=(+(v19, 1), v14)), >(+(v18, 1), 1)), <=(-(v18, 2), v15)), >(+(v17, 1), 1)), <=(-(v17, 2), v15)), >(+(v16, 1), 1)), >(+(v15, 1), 0)), >(+(v14, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f752_0_reverse_NULL(x)] = 1·x3

where x = (x1, ... ,xn).



Therefore the following rule(s) have been dropped:


f752_0_reverse_NULL(x0, x1, x2) → f752_0_reverse_NULL(x3, x4, x5) | &&(&&(&&(&&(&&(&&(&&(&&(>=(x1, -(x4, 2)), >(+(x1, 1), 0)), >=(x0, x3)), >(+(x0, 1), 0)), >(+(x5, 1), 0)), <=(+(x5, 1), x2)), >(+(x4, 1), 1)), >(+(x3, 1), 0)), >(+(x2, 1), 1))
f752_0_reverse_NULL(x6, x7, x8) → f752_0_reverse_NULL(x9, x10, x11) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x11, 1), 0), <=(+(x11, 1), x8)), <=(+(x11, 1), x6)), >(+(x10, 1), 1)), <=(-(x10, 2), x7)), >(+(x9, 1), 1)), <=(-(x9, 2), x7)), >(+(x8, 1), 1)), >(+(x7, 1), 0)), >(+(x6, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: ListReverseAcyclicList.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 17 IRules

P rules:
f246_0_createList_Load(EOS, i33) → f248_0_createList_LE(EOS, i33, i33)
f248_0_createList_LE(EOS, i37, i37) → f252_0_createList_LE(EOS, i37, i37)
f252_0_createList_LE(EOS, i37, i37) → f254_0_createList_New(EOS, i37) | >(i37, 0)
f254_0_createList_New(EOS, i37) → f256_0_createList_Duplicate(EOS, i37)
f256_0_createList_Duplicate(EOS, i37) → f260_0_createList_Load(EOS, i37)
f260_0_createList_Load(EOS, i37) → f263_0_createList_InvokeMethod(EOS, i37)
f263_0_createList_InvokeMethod(EOS, i37) → f267_0__init__Load(EOS, i37)
f267_0__init__Load(EOS, i37) → f270_0__init__InvokeMethod(EOS, i37)
f270_0__init__InvokeMethod(EOS, i37) → f274_0__init__Load(EOS, i37)
f274_0__init__Load(EOS, i37) → f278_0__init__Load(EOS, i37)
f278_0__init__Load(EOS, i37) → f282_0__init__FieldAccess(EOS, i37)
f282_0__init__FieldAccess(EOS, i37) → f291_0__init__Return(EOS, i37)
f291_0__init__Return(EOS, i37) → f297_0_createList_Store(EOS, i37)
f297_0_createList_Store(EOS, i37) → f305_0_createList_JMP(EOS, i37)
f305_0_createList_JMP(EOS, i37) → f331_0_createList_Inc(EOS, i37)
f331_0_createList_Inc(EOS, i37) → f242_0_createList_Inc(EOS, i37)
f242_0_createList_Inc(EOS, i30) → f246_0_createList_Load(EOS, +(i30, -1)) | >=(i30, 0)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f246_0_createList_Load(x1, x2) → f246_0_createList_Load(x2)
Cond_f246_0_createList_Load(x1, x2, x3) → Cond_f246_0_createList_Load(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(12) Obligation:

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

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f246_0_createList_Load(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(14) YES