Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 151 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 119 ms)
↳6 intTRS
↳7 TerminationGraphProcessor (⇔, 0 ms)
↳8 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class StupidArray {
  public static void main(String[] args) {
    int i = 0;
    while (true) {
      i = args.length + 1;
      args[i] = new String();
    }
  }
}



(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

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

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 28 IRules

P rules:
f137_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1))) → f139_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1) | >=(i1, 0)
f139_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1) → f141_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1, 1)
f141_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1, matching1) → f143_0_main_Store(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), +(i1, 1)) | &&(>=(i1, 0), =(matching1, 1))
f143_0_main_Store(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f144_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f144_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f146_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5, java.lang.Object(ARRAY(i1)))
f146_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5, java.lang.Object(ARRAY(i1))) → f148_0_main_New(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f148_0_main_New(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f149_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f149_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f150_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f150_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f151_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f151_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f152_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f152_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f155_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f155_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f157_0__init__ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f157_0__init__ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f159_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f159_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f160_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f160_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f162_0__init__ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f162_0__init__ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f164_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f164_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f167_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f167_0__init__Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f169_0__init__ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f169_0__init__ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f171_0__init__ArrayCreate(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f171_0__init__ArrayCreate(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f173_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f173_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f176_0__init__Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f176_0__init__Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f179_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f179_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f180_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f180_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f184_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5)
f184_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i5) → f187_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1))) | <(i5, i1)
f187_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1))) → f210_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)))
f210_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1))) → f132_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)))
f132_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1))) → f137_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)))

Combined rules. Obtained 1 IRules

P rules:
f137_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0))) → f137_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0))) | &&(>(+(x0, 1), 0), <(+(x0, 1), x0))

Filtered ground terms:


f137_0_main_ArrayLength(x1, x2, x3, x4) → f137_0_main_ArrayLength(x2, x3, x4)
Cond_f137_0_main_ArrayLength(x1, x2, x3, x4, x5) → Cond_f137_0_main_ArrayLength(x1, x3, x4, x5)

Filtered duplicate terms:


f137_0_main_ArrayLength(x1, x2, x3) → f137_0_main_ArrayLength(x3)
Cond_f137_0_main_ArrayLength(x1, x2, x3, x4) → Cond_f137_0_main_ArrayLength(x1, x4)

Prepared 1 rules for path length conversion:

P rules:
f137_0_main_ArrayLength(java.lang.Object(ARRAY(x0)), x0) → f137_0_main_ArrayLength(java.lang.Object(ARRAY(x0)), x0) | &&(>(+(x0, 1), 0), <(+(x0, 1), x0))

Finished conversion. Obtained 1 rules.

P rules:
f137_0_main_ArrayLength(v3, x0) → f137_0_main_ArrayLength(v4, x0) | &&(&&(&&(&&(>(x0, -1), <(+(x0, 1), x0)), >(+(v4, 1), 1)), <=(v4, v3)), >(+(v3, 1), 1))

(6) Obligation:

Rules:
f137_0_main_ArrayLength(v3, x0) → f137_0_main_ArrayLength(v4, x0) | &&(&&(&&(&&(>(x0, -1), <(+(x0, 1), x0)), >(+(v4, 1), 1)), <=(v4, v3)), >(+(v3, 1), 1))

(7) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).


(8) YES