Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class DivMinus2 {
  public static int div(int x, int y) {
    int res = 0;
    while (x >= y && y > 0) {
      x = minus(x,y);
      res = res + 1;
    }
    return res;
  }

  public static int minus(int x, int y) {
    while (y != 0) {
      if (y > 0)  {
        y--;
        x--;
      } else  {
        y++;
        x++;
      }
    }
    return x;
  }

  public static void main(String[] args) {
    Random.args = args;
    int x = Random.random();
    int y = Random.random();
    div(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:
DivMinus2.main([Ljava/lang/String;)V: Graph of 219 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: DivMinus2.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 38 IRules

P rules:
f7469_0_div_Load(EOS, i1533, i1532, i1533, i1532) → f7471_0_div_LT(EOS, i1533, i1532, i1533, i1532, i1533)
f7471_0_div_LT(EOS, i1533, i1532, i1533, i1532, i1533) → f7475_0_div_LT(EOS, i1533, i1532, i1533, i1532, i1533)
f7475_0_div_LT(EOS, i1533, i1532, i1533, i1532, i1533) → f7478_0_div_Load(EOS, i1533, i1532, i1533) | >=(i1532, i1533)
f7478_0_div_Load(EOS, i1533, i1532, i1533) → f7482_0_div_LE(EOS, i1533, i1532, i1533, i1533)
f7482_0_div_LE(EOS, i1547, i1532, i1547, i1547) → f7487_0_div_LE(EOS, i1547, i1532, i1547, i1547)
f7487_0_div_LE(EOS, i1547, i1532, i1547, i1547) → f7495_0_div_Load(EOS, i1547, i1532, i1547) | >(i1547, 0)
f7495_0_div_Load(EOS, i1547, i1532, i1547) → f7504_0_div_Load(EOS, i1547, i1547, i1532)
f7504_0_div_Load(EOS, i1547, i1547, i1532) → f7510_0_div_InvokeMethod(EOS, i1547, i1547, i1532, i1547)
f7510_0_div_InvokeMethod(EOS, i1547, i1547, i1532, i1547) → f7513_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1532, i1547)
f7513_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1532, i1547) → f7543_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1532, i1547)
f7543_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1557, i1558) → f7545_0_minus_EQ(EOS, i1547, i1547, i1532, i1547, i1557, i1558, i1558)
f7545_0_minus_EQ(EOS, i1547, i1547, i1532, i1547, i1557, i1567, i1567) → f7547_0_minus_EQ(EOS, i1547, i1547, i1532, i1547, i1557, i1567, i1567)
f7545_0_minus_EQ(EOS, i1547, i1547, i1532, i1547, i1557, matching1, matching2) → f7548_0_minus_EQ(EOS, i1547, i1547, i1532, i1547, i1557, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f7547_0_minus_EQ(EOS, i1547, i1547, i1532, i1547, i1557, i1567, i1567) → f7551_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1557, i1567) | !(=(i1567, 0))
f7551_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1557, i1567) → f7554_0_minus_LE(EOS, i1547, i1547, i1532, i1547, i1557, i1567, i1567)
f7554_0_minus_LE(EOS, i1547, i1547, i1532, i1547, i1557, i1571, i1571) → f7558_0_minus_LE(EOS, i1547, i1547, i1532, i1547, i1557, i1571, i1571)
f7554_0_minus_LE(EOS, i1547, i1547, i1532, i1547, i1557, i1573, i1573) → f7559_0_minus_LE(EOS, i1547, i1547, i1532, i1547, i1557, i1573, i1573)
f7558_0_minus_LE(EOS, i1547, i1547, i1532, i1547, i1557, i1571, i1571) → f7564_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, i1571) | <=(i1571, 0)
f7564_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, i1571) → f7570_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, +(i1571, 1)) | <(i1571, 0)
f7570_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, i1575) → f7577_0_minus_JMP(EOS, i1547, i1547, i1532, i1547, +(i1557, 1), i1575)
f7577_0_minus_JMP(EOS, i1547, i1547, i1532, i1547, i1578, i1575) → f7587_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1578, i1575)
f7587_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1578, i1575) → f7543_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1578, i1575)
f7559_0_minus_LE(EOS, i1547, i1547, i1532, i1547, i1557, i1573, i1573) → f7565_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, i1573) | >(i1573, 0)
f7565_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, i1573) → f7572_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, +(i1573, -1)) | >(i1573, 0)
f7572_0_minus_Inc(EOS, i1547, i1547, i1532, i1547, i1557, i1576) → f7578_0_minus_JMP(EOS, i1547, i1547, i1532, i1547, +(i1557, -1), i1576)
f7578_0_minus_JMP(EOS, i1547, i1547, i1532, i1547, i1579, i1576) → f7592_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1579, i1576)
f7592_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1579, i1576) → f7543_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1579, i1576)
f7548_0_minus_EQ(EOS, i1547, i1547, i1532, i1547, i1557, matching1, matching2) → f7552_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1557) | &&(=(matching1, 0), =(matching2, 0))
f7552_0_minus_Load(EOS, i1547, i1547, i1532, i1547, i1557) → f7555_0_minus_Return(EOS, i1547, i1547, i1532, i1547, i1557)
f7555_0_minus_Return(EOS, i1547, i1547, i1532, i1547, i1557) → f7562_0_div_Store(EOS, i1547, i1547, i1557)
f7562_0_div_Store(EOS, i1547, i1547, i1557) → f7568_0_div_Load(EOS, i1547, i1557, i1547)
f7568_0_div_Load(EOS, i1547, i1557, i1547) → f7574_0_div_ConstantStackPush(EOS, i1547, i1557, i1547)
f7574_0_div_ConstantStackPush(EOS, i1547, i1557, i1547) → f7580_0_div_IntArithmetic(EOS, i1547, i1557, i1547)
f7580_0_div_IntArithmetic(EOS, i1547, i1557, i1547) → f7594_0_div_Store(EOS, i1547, i1557, i1547)
f7594_0_div_Store(EOS, i1547, i1557, i1547) → f11318_0_div_JMP(EOS, i1547, i1557, i1547)
f11318_0_div_JMP(EOS, i1547, i1557, i1547) → f11321_0_div_Load(EOS, i1547, i1557, i1547)
f11321_0_div_Load(EOS, i1547, i1557, i1547) → f7464_0_div_Load(EOS, i1547, i1557, i1547)
f7464_0_div_Load(EOS, i1533, i1532, i1533) → f7469_0_div_Load(EOS, i1533, i1532, i1533, i1532)

Combined rules. Obtained 3 IRules

P rules:
f7545_0_minus_EQ(EOS, x0, x0, x1, x0, x2, x3, x3) → f7545_0_minus_EQ(EOS, x0, x0, x1, x0, +(x2, 1), +(x3, 1), +(x3, 1)) | <(x3, 0)
f7545_0_minus_EQ(EOS, x0, x0, x1, x0, x2, x3, x3) → f7545_0_minus_EQ(EOS, x0, x0, x1, x0, -(x2, 1), -(x3, 1), -(x3, 1)) | >(x3, 0)
f7545_0_minus_EQ(EOS, x0, x0, x1, x0, x2, 0, 0) → f7545_0_minus_EQ(EOS, x0, x0, x2, x0, x2, x0, x0) | &&(>(x0, 0), >=(x2, x0))

Filtered ground terms:


f7545_0_minus_EQ(x1, x2, x3, x4, x5, x6, x7, x8) → f7545_0_minus_EQ(x2, x3, x4, x5, x6, x7, x8)
Cond_f7545_0_minus_EQ(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f7545_0_minus_EQ(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f7545_0_minus_EQ1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f7545_0_minus_EQ1(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f7545_0_minus_EQ2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f7545_0_minus_EQ2(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:


f7545_0_minus_EQ(x1, x2, x3, x4, x5, x6, x7) → f7545_0_minus_EQ(x3, x4, x5, x7)
Cond_f7545_0_minus_EQ(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f7545_0_minus_EQ(x1, x4, x5, x6, x8)
Cond_f7545_0_minus_EQ1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f7545_0_minus_EQ1(x1, x4, x5, x6, x8)
Cond_f7545_0_minus_EQ2(x1, x2, x3, x4, x5, x6) → Cond_f7545_0_minus_EQ2(x1, x4, x5, x6)

Filtered unneeded terms:


Cond_f7545_0_minus_EQ(x1, x2, x3, x4, x5) → Cond_f7545_0_minus_EQ(x1, x3, x4, x5)
Cond_f7545_0_minus_EQ1(x1, x2, x3, x4, x5) → Cond_f7545_0_minus_EQ1(x1, x3, x4, x5)
f7545_0_minus_EQ(x1, x2, x3, x4) → f7545_0_minus_EQ(x2, x3, x4)
Cond_f7545_0_minus_EQ2(x1, x2, x3, x4) → Cond_f7545_0_minus_EQ2(x1, x3, x4)

Prepared 3 rules for path length conversion:

P rules:
f7545_0_minus_EQ(x0, x2, x3) → f7545_0_minus_EQ(x0, +(x2, 1), +(x3, 1)) | <(x3, 0)
f7545_0_minus_EQ(x0, x2, x3) → f7545_0_minus_EQ(x0, -(x2, 1), -(x3, 1)) | >(x3, 0)
f7545_0_minus_EQ(x0, x2, 0) → f7545_0_minus_EQ(x0, x2, x0) | &&(>(x0, 0), >=(x2, x0))

Finished conversion. Obtained 3 rules.

P rules:
f7545_0_minus_EQ(x0, x1, x2) → f7545_0_minus_EQ(x0, +(x1, 1), +(x2, 1)) | <(x2, 0)
f7545_0_minus_EQ(x3, x4, x5) → f7545_0_minus_EQ(x3, -(x4, 1), -(x5, 1)) | >(x5, 0)
f7545_0_minus_EQ(x6, x7, c0) → f7545_0_minus_EQ(x6, x7, x6) | &&(&&(>(x6, 0), >=(x7, x6)), =(0, c0))

(6) Obligation:

Rules:
f7545_0_minus_EQ(x0, x1, x2) → f7545_0_minus_EQ(x0, +(x1, 1), +(x2, 1)) | <(x2, 0)
f7545_0_minus_EQ(x3, x4, x5) → f7545_0_minus_EQ(x3, -(x4, 1), -(x5, 1)) | >(x5, 0)
f7545_0_minus_EQ(x6, x7, c0) → f7545_0_minus_EQ(x6, x7, x6) | &&(&&(>(x6, 0), >=(x7, x6)), =(0, c0))

(7) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained 2 non-trivial SCCs.


(8) Complex Obligation (AND)

(9) Obligation:

Rules:
f7545_0_minus_EQ(x0, x1, x2) → f7545_0_minus_EQ(x0, +(x1, 1), +(x2, 1)) | <(x2, 0)

(10) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f7545_0_minus_EQ(x4, x6, x8)] = -x8

Therefore the following rule(s) have been dropped:


f7545_0_minus_EQ(x0, x1, x2) → f7545_0_minus_EQ(x0, +(x1, 1), +(x2, 1)) | <(x2, 0)

(11) YES

(12) Obligation:

Rules:
f7545_0_minus_EQ(x6, x7, x8) → f7545_0_minus_EQ(x6, x7, x6) | &&(&&(>(x6, 0), >=(x7, x6)), =(0, x8))
f7545_0_minus_EQ(x3, x4, x5) → f7545_0_minus_EQ(x3, -(x4, 1), -(x5, 1)) | >(x5, 0)

(13) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f7545_0_minus_EQ(x7, x9, x11)] = -x11 + x7 + x9

Therefore the following rule(s) have been dropped:


f7545_0_minus_EQ(x0, x1, x2) → f7545_0_minus_EQ(x0, x1, x0) | &&(&&(>(x0, 0), >=(x1, x0)), =(0, x2))

(14) Obligation:

Rules:
f7545_0_minus_EQ(x3, x4, x5) → f7545_0_minus_EQ(x3, -(x4, 1), -(x5, 1)) | >(x5, 0)

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f7545_0_minus_EQ(x4, x6, x8)] = x8

Therefore the following rule(s) have been dropped:


f7545_0_minus_EQ(x0, x1, x2) → f7545_0_minus_EQ(x0, -(x1, 1), -(x2, 1)) | >(x2, 0)

(16) YES