Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class IntRTA {
  // only wrap a primitive int
  private int val;

  // count up to the value
  // in "limit"
  public static void count(
      IntRTA orig, IntRTA limit) {

    if (orig == null
        || limit == null) {
      return;
    }

    // introduce sharing
    IntRTA copy = orig;

    while (orig.val < limit.val) {
      copy.val++;
    }
  }

  public static void main(String[] args) {
    Random.args = args;
    IntRTA x = new IntRTA();
    x.val = Random.random();
    IntRTA y = new IntRTA();
    y.val = Random.random();
    count(x, y);
  }
}


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:
IntRTA.main([Ljava/lang/String;)V: Graph of 207 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: IntRTA.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • IntRTA: [val]
  • Marker field analysis yielded the following relations that could be markers:
    • IntRTA.val < i45 (Introduced counter i114)
    • IntRTA.val > i18 (Introduced counter i115)

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 14 IRules

P rules:
f492_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i114, i115) → f503_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, i114, i115)
f503_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, i114, i115) → f511_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, java.lang.Object(IntRTA(EOC, i45)), i114, i115)
f511_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, java.lang.Object(IntRTA(EOC, i45)), i114, i115) → f519_0_count_GE(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, i45, i114, i115)
f519_0_count_GE(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, i45, i114, i115) → f529_0_count_GE(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, i45, i114, i115)
f529_0_count_GE(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i18, i45, i114, i115) → f536_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i114, i115) | <(i18, i45)
f536_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i114, i115) → f543_0_count_Duplicate(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i114, i115)
f543_0_count_Duplicate(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i114, i115) → f551_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i114, i115)
f551_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i114, i115) → f556_0_count_ConstantStackPush(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i18, i114, i115)
f556_0_count_ConstantStackPush(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i18, i114, i115) → f558_0_count_IntArithmetic(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i18, 1, i114, i115)
f558_0_count_IntArithmetic(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i18, matching1, i114, i115) → f561_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), +(i18, 1), i114, i115) | &&(>=(i18, 0), =(matching1, 1))
f561_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i55, i114, i115) → f564_0_count_JMP(EOS, java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), +(i114, 0), +(i115, 1)) | &&(>=(i114, 0), >=(i115, 0))
f564_0_count_JMP(EOS, java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), i114, i115) → f593_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), i114, i115)
f593_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), i114, i115) → f482_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i55)), i114, i115)
f482_0_count_Load(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), i114, i115) → f492_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i45)), java.lang.Object(IntRTA(EOC, i18)), java.lang.Object(IntRTA(EOC, i18)), i114, i115)

Combined rules. Obtained 1 IRules

P rules:
f492_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, x0)), java.lang.Object(IntRTA(EOC, x1)), java.lang.Object(IntRTA(EOC, x0)), java.lang.Object(IntRTA(EOC, x1)), java.lang.Object(IntRTA(EOC, x0)), java.lang.Object(IntRTA(EOC, x0)), arith, x3) → f492_0_count_FieldAccess(EOS, java.lang.Object(IntRTA(EOC, +(x0, 1))), java.lang.Object(IntRTA(EOC, x1)), java.lang.Object(IntRTA(EOC, +(x0, 1))), java.lang.Object(IntRTA(EOC, x1)), java.lang.Object(IntRTA(EOC, +(x0, 1))), java.lang.Object(IntRTA(EOC, +(x0, 1))), arith, +(x3, 1)) | &&(&&(&&(>(+(x3, 1), 0), >(x1, x0)), >(+(arith, 1), 0)), >(+(x0, 1), 0))

Filtered ground terms:


f492_0_count_FieldAccess(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f492_0_count_FieldAccess(x2, x3, x4, x5, x6, x7, x8, x9)
Cond_f492_0_count_FieldAccess(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f492_0_count_FieldAccess(x1, x3, x4, x5, x6, x7, x8, x9, x10)
IntRTA(x1, x2) → IntRTA(x2)

Filtered duplicate terms:


f492_0_count_FieldAccess(x1, x2, x3, x4, x5, x6, x7, x8) → f492_0_count_FieldAccess(x4, x6, x7, x8)
Cond_f492_0_count_FieldAccess(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f492_0_count_FieldAccess(x1, x5, x7, x8, x9)

Prepared 1 rules for path length conversion:

P rules:
f492_0_count_FieldAccess(java.lang.Object(IntRTA(x1)), java.lang.Object(IntRTA(x0)), arith, x3, x1, x0) → f492_0_count_FieldAccess(java.lang.Object(IntRTA(x1)), java.lang.Object(IntRTA(+(x0, 1))), arith, +(x3, 1), x1, +(x0, 1)) | &&(&&(&&(>(+(x3, 1), 0), >(x1, x0)), >(+(arith, 1), 0)), >(+(x0, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f492_0_count_FieldAccess(v10, v11, x2, x3, x0, x1) → f492_0_count_FieldAccess(v12, v13, x2, +(x3, 1), x0, +(x1, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x3, -1), >(x2, -1)), >(x1, -1)), <(x1, x0)), <=(+(x1, 2), v11)), <=(+(x0, 2), v10)), >(+(v13, 1), 1)), <=(-(v13, 1), v11)), >(+(v12, 1), 1)), <=(v12, v10)), >(+(v11, 1), 1)), >(+(v10, 1), 1))

(6) Obligation:

Rules:
f492_0_count_FieldAccess(v10, v11, x2, x3, x0, x1) → f492_0_count_FieldAccess(v12, v13, x2, +(x3, 1), x0, +(x1, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x3, -1), >(x2, -1)), >(x1, -1)), <(x1, x0)), <=(+(x1, 2), v11)), <=(+(x0, 2), v10)), >(+(v13, 1), 1)), <=(-(v13, 1), v11)), >(+(v12, 1), 1)), <=(v12, v10)), >(+(v11, 1), 1)), >(+(v10, 1), 1))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


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

Therefore the following rule(s) have been dropped:


f492_0_count_FieldAccess(x0, x1, x2, x3, x4, x5) → f492_0_count_FieldAccess(x6, x7, x2, +(x3, 1), x4, +(x5, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x3, -1), >(x2, -1)), >(x5, -1)), <(x5, x4)), <=(+(x5, 2), x1)), <=(+(x4, 2), x0)), >(+(x7, 1), 1)), <=(-(x7, 1), x1)), >(+(x6, 1), 1)), <=(x6, x0)), >(+(x1, 1), 1)), >(+(x0, 1), 1))

(8) YES