Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class ListContent{

  public static void main(String[] args) {
    Random.args = args;
    IntList l = IntList.createIntList();

    while (l.value > 0) l.value--;
  }

}

class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }

  public static IntList createIntList() {

    int i = Random.random();
    IntList l = null;

    while (i > 0) {
      l = new IntList(Random.random(), l);
      i--;
    }

    return l;
  }
}


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

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


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ListContent.main([Ljava/lang/String;)V: Graph of 89 nodes with 1 SCC.

IntList.createIntList()LIntList;: Graph of 163 nodes with 1 SCC.


(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: IntList.createIntList()LIntList;
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • java.lang.String: [count]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 38 IRules

P rules:
f1641_0_createIntList_LE(EOS, i426, i426) → f1644_0_createIntList_LE(EOS, i426, i426)
f1644_0_createIntList_LE(EOS, i426, i426) → f1647_0_createIntList_New(EOS, i426) | >(i426, 0)
f1647_0_createIntList_New(EOS, i426) → f1650_0_createIntList_Duplicate(EOS, i426)
f1650_0_createIntList_Duplicate(EOS, i426) → f1653_0_createIntList_InvokeMethod(EOS, i426)
f1653_0_createIntList_InvokeMethod(EOS, i426) → f1660_0_random_FieldAccess(EOS, i426)
f1660_0_random_FieldAccess(EOS, i426) → f1667_0_random_FieldAccess(EOS, i426)
f1667_0_random_FieldAccess(EOS, i426) → f1670_0_random_ArrayAccess(EOS, i426)
f1670_0_random_ArrayAccess(EOS, i426) → f1672_0_random_ArrayAccess(EOS, i426)
f1672_0_random_ArrayAccess(EOS, i426) → f1676_0_random_Store(EOS, i426, o533)
f1676_0_random_Store(EOS, i426, o533) → f1679_0_random_FieldAccess(EOS, i426, o533)
f1679_0_random_FieldAccess(EOS, i426, o533) → f1682_0_random_ConstantStackPush(EOS, i426, o533)
f1682_0_random_ConstantStackPush(EOS, i426, o533) → f1687_0_random_IntArithmetic(EOS, i426, o533)
f1687_0_random_IntArithmetic(EOS, i426, o533) → f1691_0_random_FieldAccess(EOS, i426, o533)
f1691_0_random_FieldAccess(EOS, i426, o533) → f1693_0_random_Load(EOS, i426, o533)
f1693_0_random_Load(EOS, i426, o533) → f1700_0_random_InvokeMethod(EOS, i426, o533)
f1700_0_random_InvokeMethod(EOS, i426, java.lang.Object(o548sub)) → f1703_0_random_InvokeMethod(EOS, i426, java.lang.Object(o548sub))
f1703_0_random_InvokeMethod(EOS, i426, java.lang.Object(o548sub)) → f1707_0_length_Load(EOS, i426, java.lang.Object(o548sub), java.lang.Object(o548sub))
f1707_0_length_Load(EOS, i426, java.lang.Object(o548sub), java.lang.Object(o548sub)) → f1721_0_length_FieldAccess(EOS, i426, java.lang.Object(o548sub), java.lang.Object(o548sub))
f1721_0_length_FieldAccess(EOS, i426, java.lang.Object(java.lang.String(o556sub, i464)), java.lang.Object(java.lang.String(o556sub, i464))) → f1723_0_length_FieldAccess(EOS, i426, java.lang.Object(java.lang.String(o556sub, i464)), java.lang.Object(java.lang.String(o556sub, i464)))
f1723_0_length_FieldAccess(EOS, i426, java.lang.Object(java.lang.String(o556sub, i464)), java.lang.Object(java.lang.String(o556sub, i464))) → f1731_0_length_Return(EOS, i426, java.lang.Object(java.lang.String(o556sub, i464)))
f1731_0_length_Return(EOS, i426, java.lang.Object(java.lang.String(o556sub, i464))) → f1737_0_random_Return(EOS, i426)
f1737_0_random_Return(EOS, i426) → f1739_0_createIntList_Load(EOS, i426)
f1739_0_createIntList_Load(EOS, i426) → f1748_0_createIntList_InvokeMethod(EOS, i426)
f1748_0_createIntList_InvokeMethod(EOS, i426) → f1755_0__init__Load(EOS, i426)
f1755_0__init__Load(EOS, i426) → f1767_0__init__InvokeMethod(EOS, i426)
f1767_0__init__InvokeMethod(EOS, i426) → f1775_0__init__Load(EOS, i426)
f1775_0__init__Load(EOS, i426) → f1781_0__init__Load(EOS, i426)
f1781_0__init__Load(EOS, i426) → f1789_0__init__FieldAccess(EOS, i426)
f1789_0__init__FieldAccess(EOS, i426) → f1798_0__init__Load(EOS, i426)
f1798_0__init__Load(EOS, i426) → f1806_0__init__Load(EOS, i426)
f1806_0__init__Load(EOS, i426) → f1814_0__init__FieldAccess(EOS, i426)
f1814_0__init__FieldAccess(EOS, i426) → f1825_0__init__Return(EOS, i426)
f1825_0__init__Return(EOS, i426) → f1833_0_createIntList_Store(EOS, i426)
f1833_0_createIntList_Store(EOS, i426) → f1842_0_createIntList_Inc(EOS, i426)
f1842_0_createIntList_Inc(EOS, i426) → f1851_0_createIntList_JMP(EOS, +(i426, -1)) | >(i426, 0)
f1851_0_createIntList_JMP(EOS, i512) → f1859_0_createIntList_Load(EOS, i512)
f1859_0_createIntList_Load(EOS, i512) → f1635_0_createIntList_Load(EOS, i512)
f1635_0_createIntList_Load(EOS, i421) → f1641_0_createIntList_LE(EOS, i421, i421)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f1641_0_createIntList_LE(x1, x2, x3) → f1641_0_createIntList_LE(x2, x3)
Cond_f1641_0_createIntList_LE(x1, x2, x3, x4) → Cond_f1641_0_createIntList_LE(x1, x3, x4)

Filtered duplicate terms:


f1641_0_createIntList_LE(x1, x2) → f1641_0_createIntList_LE(x2)
Cond_f1641_0_createIntList_LE(x1, x2, x3) → Cond_f1641_0_createIntList_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(7) Obligation:

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

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1641_0_createIntList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(9) YES

(10) Obligation:

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

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 14 IRules

P rules:
f1381_0_main_FieldAccess(EOS, java.lang.Object(o422sub), java.lang.Object(o422sub), i552) → f1386_0_main_FieldAccess(EOS, java.lang.Object(o422sub), java.lang.Object(o422sub), i552)
f1386_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, i334)), java.lang.Object(IntList(EOC, i334)), i552) → f1390_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, i334)), java.lang.Object(IntList(EOC, i334)), i552)
f1390_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, i334)), java.lang.Object(IntList(EOC, i334)), i552) → f1400_0_main_LE(EOS, java.lang.Object(IntList(EOC, i334)), i334, i552)
f1400_0_main_LE(EOS, java.lang.Object(IntList(EOC, i341)), i341, i552) → f1406_0_main_LE(EOS, java.lang.Object(IntList(EOC, i341)), i341, i552)
f1406_0_main_LE(EOS, java.lang.Object(IntList(EOC, i341)), i341, i552) → f1416_0_main_Load(EOS, java.lang.Object(IntList(EOC, i341)), i552) | >(i341, 0)
f1416_0_main_Load(EOS, java.lang.Object(IntList(EOC, i341)), i552) → f1427_0_main_Duplicate(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i552)
f1427_0_main_Duplicate(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i552) → f1438_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i552)
f1438_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i552) → f1445_0_main_ConstantStackPush(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i341, i552)
f1445_0_main_ConstantStackPush(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i341, i552) → f1450_0_main_IntArithmetic(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i341, 1, i552)
f1450_0_main_IntArithmetic(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i341, matching1, i552) → f1459_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), -(i341, 1), i552) | &&(>(i341, 0), =(matching1, 1))
f1459_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, i341)), java.lang.Object(IntList(EOC, i341)), i360, i552) → f1462_0_main_JMP(EOS, java.lang.Object(IntList(EOC, i360)), +(i552, 0)) | >=(i552, 0)
f1462_0_main_JMP(EOS, java.lang.Object(IntList(EOC, i360)), i552) → f1475_0_main_Load(EOS, java.lang.Object(IntList(EOC, i360)), i552)
f1475_0_main_Load(EOS, java.lang.Object(IntList(EOC, i360)), i552) → f1375_0_main_Load(EOS, java.lang.Object(IntList(EOC, i360)), i552)
f1375_0_main_Load(EOS, o414, i552) → f1381_0_main_FieldAccess(EOS, o414, o414, i552)

Combined rules. Obtained 1 IRules

P rules:
f1381_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, x0)), java.lang.Object(IntList(EOC, x0)), arith) → f1381_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, -(x0, 1))), java.lang.Object(IntList(EOC, -(x0, 1))), arith) | &&(>(x0, 0), >(+(arith, 1), 0))

Filtered ground terms:


f1381_0_main_FieldAccess(x1, x2, x3, x4) → f1381_0_main_FieldAccess(x2, x3, x4)
Cond_f1381_0_main_FieldAccess(x1, x2, x3, x4, x5) → Cond_f1381_0_main_FieldAccess(x1, x3, x4, x5)
IntList(x1, x2) → IntList(x2)

Filtered duplicate terms:


f1381_0_main_FieldAccess(x1, x2, x3) → f1381_0_main_FieldAccess(x2, x3)
Cond_f1381_0_main_FieldAccess(x1, x2, x3, x4) → Cond_f1381_0_main_FieldAccess(x1, x3, x4)

Prepared 1 rules for path length conversion:

P rules:
f1381_0_main_FieldAccess(java.lang.Object(IntList(x0)), arith, x0) → f1381_0_main_FieldAccess(java.lang.Object(IntList(-(x0, 1))), arith, -(x0, 1)) | &&(>(x0, 0), >(+(arith, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f1381_0_main_FieldAccess(v5, x1, x0) → f1381_0_main_FieldAccess(v6, x1, -(x0, 1)) | &&(&&(&&(&&(&&(>(x1, -1), >(x0, 0)), <=(+(x0, 2), v5)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(12) Obligation:

Rules:
f1381_0_main_FieldAccess(v5, x1, x0) → f1381_0_main_FieldAccess(v6, x1, -(x0, 1)) | &&(&&(&&(&&(&&(>(x1, -1), >(x0, 0)), <=(+(x0, 2), v5)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(13) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f1381_0_main_FieldAccess(x)] = 1·x3

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



Therefore the following rule(s) have been dropped:


f1381_0_main_FieldAccess(x0, x1, x2) → f1381_0_main_FieldAccess(x3, x1, -(x2, 1)) | &&(&&(&&(&&(&&(>(x1, -1), >(x2, 0)), <=(+(x2, 2), x0)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x0, 1), 1))

(14) YES