Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class GCD {
  public static int mod(int a, int b) {
    if(a <= 0 || b <= 0)
      return 0;
    if (a == b) {
      return 0;
    }
    while(a>b) {
      a -= b;
    }
    return a;
  }

  public static int gcd(int a, int b) {
    int tmp;
    while(b != 0) {
      tmp = b;
      b = mod(a, b);
      a = tmp;
    }
    return a;
  }

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

P rules:
f3655_0_gcd_EQ(EOS, i388, i393, i393) → f3657_0_gcd_EQ(EOS, i388, i393, i393)
f3657_0_gcd_EQ(EOS, i388, i393, i393) → f3661_0_gcd_Load(EOS, i388, i393) | !(=(i393, 0))
f3661_0_gcd_Load(EOS, i388, i393) → f3666_0_gcd_Store(EOS, i388, i393, i393)
f3666_0_gcd_Store(EOS, i388, i393, i393) → f3669_0_gcd_Load(EOS, i388, i393, i393)
f3669_0_gcd_Load(EOS, i388, i393, i393) → f3672_0_gcd_Load(EOS, i393, i393, i388)
f3672_0_gcd_Load(EOS, i393, i393, i388) → f3675_0_gcd_InvokeMethod(EOS, i393, i388, i393)
f3675_0_gcd_InvokeMethod(EOS, i393, i388, i393) → f3678_0_mod_Load(EOS, i393, i388, i393, i388, i393)
f3678_0_mod_Load(EOS, i393, i388, i393, i388, i393) → f3681_0_mod_LE(EOS, i393, i388, i393, i388, i393, i388)
f3681_0_mod_LE(EOS, i393, i397, i393, i397, i393, i397) → f3683_0_mod_LE(EOS, i393, i397, i393, i397, i393, i397)
f3681_0_mod_LE(EOS, i393, i398, i393, i398, i393, i398) → f3684_0_mod_LE(EOS, i393, i398, i393, i398, i393, i398)
f3683_0_mod_LE(EOS, i393, i397, i393, i397, i393, i397) → f3686_0_mod_ConstantStackPush(EOS, i393, i397, i393, i397, i393) | <=(i397, 0)
f3686_0_mod_ConstantStackPush(EOS, i393, i397, i393, i397, i393) → f3689_0_mod_Return(EOS, i393, i397, i393, i397, i393, 0)
f3689_0_mod_Return(EOS, i393, i397, i393, i397, i393, matching1) → f3693_0_gcd_Store(EOS, i393, 0) | =(matching1, 0)
f3693_0_gcd_Store(EOS, i393, matching1) → f3698_0_gcd_Load(EOS, 0, i393) | =(matching1, 0)
f3698_0_gcd_Load(EOS, matching1, i393) → f3705_0_gcd_Store(EOS, 0, i393) | =(matching1, 0)
f3705_0_gcd_Store(EOS, matching1, i393) → f3711_0_gcd_JMP(EOS, i393, 0) | =(matching1, 0)
f3711_0_gcd_JMP(EOS, i393, matching1) → f3723_0_gcd_Load(EOS, i393, 0) | =(matching1, 0)
f3723_0_gcd_Load(EOS, i393, matching1) → f3651_0_gcd_Load(EOS, i393, 0) | =(matching1, 0)
f3651_0_gcd_Load(EOS, i388, i389) → f3655_0_gcd_EQ(EOS, i388, i389, i389)
f3684_0_mod_LE(EOS, i393, i398, i393, i398, i393, i398) → f3687_0_mod_Load(EOS, i393, i398, i393, i398, i393) | >(i398, 0)
f3687_0_mod_Load(EOS, i393, i398, i393, i398, i393) → f3691_0_mod_GT(EOS, i393, i398, i393, i398, i393, i393)
f3691_0_mod_GT(EOS, i401, i398, i401, i398, i401, i401) → f3695_0_mod_GT(EOS, i401, i398, i401, i398, i401, i401)
f3691_0_mod_GT(EOS, i402, i398, i402, i398, i402, i402) → f3697_0_mod_GT(EOS, i402, i398, i402, i398, i402, i402)
f3695_0_mod_GT(EOS, i401, i398, i401, i398, i401, i401) → f3701_0_mod_ConstantStackPush(EOS, i401, i398, i401, i398, i401) | <=(i401, 0)
f3701_0_mod_ConstantStackPush(EOS, i401, i398, i401, i398, i401) → f3707_0_mod_Return(EOS, i401, i398, i401, i398, i401, 0)
f3707_0_mod_Return(EOS, i401, i398, i401, i398, i401, matching1) → f3714_0_gcd_Store(EOS, i401, 0) | =(matching1, 0)
f3714_0_gcd_Store(EOS, i401, matching1) → f3726_0_gcd_Load(EOS, 0, i401) | =(matching1, 0)
f3726_0_gcd_Load(EOS, matching1, i401) → f4340_0_gcd_Store(EOS, 0, i401) | =(matching1, 0)
f4340_0_gcd_Store(EOS, matching1, i401) → f4346_0_gcd_JMP(EOS, i401, 0) | =(matching1, 0)
f4346_0_gcd_JMP(EOS, i401, matching1) → f4361_0_gcd_Load(EOS, i401, 0) | =(matching1, 0)
f4361_0_gcd_Load(EOS, i401, matching1) → f3651_0_gcd_Load(EOS, i401, 0) | =(matching1, 0)
f3697_0_mod_GT(EOS, i402, i398, i402, i398, i402, i402) → f3703_0_mod_Load(EOS, i402, i398, i402, i398, i402) | >(i402, 0)
f3703_0_mod_Load(EOS, i402, i398, i402, i398, i402) → f3709_0_mod_Load(EOS, i402, i398, i402, i398, i402, i398)
f3709_0_mod_Load(EOS, i402, i398, i402, i398, i402, i398) → f3716_0_mod_NE(EOS, i402, i398, i402, i398, i402, i398, i402)
f3716_0_mod_NE(EOS, i402, i398, i402, i398, i402, i398, i402) → f3728_0_mod_NE(EOS, i402, i398, i402, i398, i402, i398, i402)
f3716_0_mod_NE(EOS, i402, i402, i402, i402, i402, i402, i402) → f3729_0_mod_NE(EOS, i402, i402, i402, i402, i402, i402, i402)
f3728_0_mod_NE(EOS, i402, i398, i402, i398, i402, i398, i402) → f4341_0_mod_Load(EOS, i402, i398, i402, i398, i402) | !(=(i398, i402))
f4341_0_mod_Load(EOS, i402, i398, i402, i398, i402) → f10611_0_mod_Load(EOS, i402, i398, i402, i398, i402)
f10611_0_mod_Load(EOS, i402, i398, i402, i1008, i402) → f10616_0_mod_Load(EOS, i402, i398, i402, i1008, i402, i1008)
f10616_0_mod_Load(EOS, i402, i398, i402, i1008, i402, i1008) → f10618_0_mod_LE(EOS, i402, i398, i402, i1008, i402, i1008, i402)
f10618_0_mod_LE(EOS, i402, i398, i402, i1008, i402, i1008, i402) → f10619_0_mod_LE(EOS, i402, i398, i402, i1008, i402, i1008, i402)
f10618_0_mod_LE(EOS, i402, i398, i402, i1008, i402, i1008, i402) → f10620_0_mod_LE(EOS, i402, i398, i402, i1008, i402, i1008, i402)
f10619_0_mod_LE(EOS, i402, i398, i402, i1008, i402, i1008, i402) → f10622_0_mod_Load(EOS, i402, i398, i402, i1008) | <=(i1008, i402)
f10622_0_mod_Load(EOS, i402, i398, i402, i1008) → f10625_0_mod_Return(EOS, i402, i398, i402, i1008)
f10625_0_mod_Return(EOS, i402, i398, i402, i1008) → f10633_0_gcd_Store(EOS, i402, i1008)
f10633_0_gcd_Store(EOS, i402, i1008) → f10641_0_gcd_Load(EOS, i1008, i402)
f10641_0_gcd_Load(EOS, i1008, i402) → f10647_0_gcd_Store(EOS, i1008, i402)
f10647_0_gcd_Store(EOS, i1008, i402) → f10653_0_gcd_JMP(EOS, i402, i1008)
f10653_0_gcd_JMP(EOS, i402, i1008) → f10661_0_gcd_Load(EOS, i402, i1008)
f10661_0_gcd_Load(EOS, i402, i1008) → f3651_0_gcd_Load(EOS, i402, i1008)
f10620_0_mod_LE(EOS, i402, i398, i402, i1008, i402, i1008, i402) → f10623_0_mod_Load(EOS, i402, i398, i402, i1008, i402) | >(i1008, i402)
f10623_0_mod_Load(EOS, i402, i398, i402, i1008, i402) → f10626_0_mod_Load(EOS, i402, i398, i402, i402, i1008)
f10626_0_mod_Load(EOS, i402, i398, i402, i402, i1008) → f10637_0_mod_IntArithmetic(EOS, i402, i398, i402, i402, i1008, i402)
f10637_0_mod_IntArithmetic(EOS, i402, i398, i402, i402, i1008, i402) → f10643_0_mod_Store(EOS, i402, i398, i402, i402, -(i1008, i402)) | >(i402, 0)
f10643_0_mod_Store(EOS, i402, i398, i402, i402, i1015) → f10648_0_mod_JMP(EOS, i402, i398, i402, i1015, i402)
f10648_0_mod_JMP(EOS, i402, i398, i402, i1015, i402) → f10657_0_mod_Load(EOS, i402, i398, i402, i1015, i402)
f10657_0_mod_Load(EOS, i402, i398, i402, i1015, i402) → f10611_0_mod_Load(EOS, i402, i398, i402, i1015, i402)
f3729_0_mod_NE(EOS, i402, i402, i402, i402, i402, i402, i402) → f4343_0_mod_ConstantStackPush(EOS, i402, i402, i402, i402, i402)
f4343_0_mod_ConstantStackPush(EOS, i402, i402, i402, i402, i402) → f4349_0_mod_Return(EOS, i402, i402, i402, i402, i402, 0)
f4349_0_mod_Return(EOS, i402, i402, i402, i402, i402, matching1) → f4367_0_gcd_Store(EOS, i402, 0) | =(matching1, 0)
f4367_0_gcd_Store(EOS, i402, matching1) → f10633_0_gcd_Store(EOS, i402, 0) | =(matching1, 0)

Combined rules. Obtained 6 IRules

P rules:
f3655_0_gcd_EQ(EOS, x0, x1, x1) → f3655_0_gcd_EQ(EOS, x1, 0, 0) | &&(<=(x0, 0), !(=(x1, 0)))
f3655_0_gcd_EQ(EOS, x0, x1, x1) → f3655_0_gcd_EQ(EOS, x1, 0, 0) | &&(>(x0, 0), <(x1, 0))
f3655_0_gcd_EQ(EOS, x0, x1, x1) → f10618_0_mod_LE(EOS, x1, x0, x1, x0, x1, x0, x1) | &&(&&(>(x1, 0), !(=(x0, x1))), >(x0, 0))
f10618_0_mod_LE(EOS, x0, x1, x0, x2, x0, x2, x0) → f3655_0_gcd_EQ(EOS, x0, x2, x2) | <=(x2, x0)
f10618_0_mod_LE(EOS, x0, x1, x0, x2, x0, x2, x0) → f10618_0_mod_LE(EOS, x0, x1, x0, -(x2, x0), x0, -(x2, x0), x0) | &&(>(x0, 0), >(x2, x0))
f3655_0_gcd_EQ(EOS, x0, x0, x0) → f3655_0_gcd_EQ(EOS, x0, 0, 0) | >(x0, 0)

Filtered ground terms:


f3655_0_gcd_EQ(x1, x2, x3, x4) → f3655_0_gcd_EQ(x2, x3, x4)
Cond_f3655_0_gcd_EQ(x1, x2, x3, x4, x5) → Cond_f3655_0_gcd_EQ(x1, x3, x4, x5)
Cond_f3655_0_gcd_EQ1(x1, x2, x3, x4, x5) → Cond_f3655_0_gcd_EQ1(x1, x3, x4, x5)
Cond_f3655_0_gcd_EQ2(x1, x2, x3, x4, x5) → Cond_f3655_0_gcd_EQ2(x1, x3, x4, x5)
f10618_0_mod_LE(x1, x2, x3, x4, x5, x6, x7, x8) → f10618_0_mod_LE(x2, x3, x4, x5, x6, x7, x8)
Cond_f10618_0_mod_LE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f10618_0_mod_LE(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f10618_0_mod_LE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f10618_0_mod_LE1(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f3655_0_gcd_EQ3(x1, x2, x3, x4, x5) → Cond_f3655_0_gcd_EQ3(x1, x3, x4, x5)

Filtered duplicate terms:


f3655_0_gcd_EQ(x1, x2, x3) → f3655_0_gcd_EQ(x1, x3)
Cond_f3655_0_gcd_EQ(x1, x2, x3, x4) → Cond_f3655_0_gcd_EQ(x1, x2, x4)
Cond_f3655_0_gcd_EQ1(x1, x2, x3, x4) → Cond_f3655_0_gcd_EQ1(x1, x2, x4)
Cond_f3655_0_gcd_EQ2(x1, x2, x3, x4) → Cond_f3655_0_gcd_EQ2(x1, x2, x4)
f10618_0_mod_LE(x1, x2, x3, x4, x5, x6, x7) → f10618_0_mod_LE(x2, x4, x6, x7)
Cond_f10618_0_mod_LE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10618_0_mod_LE(x1, x3, x7, x8)
Cond_f10618_0_mod_LE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10618_0_mod_LE1(x1, x3, x7, x8)
Cond_f3655_0_gcd_EQ3(x1, x2, x3, x4) → Cond_f3655_0_gcd_EQ3(x1, x4)

Filtered unneeded terms:


Cond_f3655_0_gcd_EQ(x1, x2, x3) → Cond_f3655_0_gcd_EQ(x1, x3)
Cond_f3655_0_gcd_EQ1(x1, x2, x3) → Cond_f3655_0_gcd_EQ1(x1, x3)
f10618_0_mod_LE(x1, x2, x3, x4) → f10618_0_mod_LE(x2, x3, x4)
Cond_f10618_0_mod_LE(x1, x2, x3, x4) → Cond_f10618_0_mod_LE(x1, x3, x4)
Cond_f10618_0_mod_LE1(x1, x2, x3, x4) → Cond_f10618_0_mod_LE1(x1, x3, x4)

Prepared 6 rules for path length conversion:

P rules:
f3655_0_gcd_EQ(x0, x1) → f3655_0_gcd_EQ(x1, 0) | &&(<=(x0, 0), !(=(x1, 0)))
f3655_0_gcd_EQ(x0, x1) → f3655_0_gcd_EQ(x1, 0) | &&(>(x0, 0), <(x1, 0))
f3655_0_gcd_EQ(x0, x1) → f10618_0_mod_LE(x0, x0, x1) | &&(&&(>(x1, 0), !(=(x0, x1))), >(x0, 0))
f10618_0_mod_LE(x2, x2, x0) → f3655_0_gcd_EQ(x0, x2) | <=(x2, x0)
f10618_0_mod_LE(x2, x2, x0) → f10618_0_mod_LE(-(x2, x0), -(x2, x0), x0) | &&(>(x0, 0), >(x2, x0))
f3655_0_gcd_EQ(x0, x0) → f3655_0_gcd_EQ(x0, 0) | >(x0, 0)

Finished conversion. Obtained 8 rules.

P rules:
f3655_0_gcd_EQ(x0, x1) → f3655_0_gcd_EQ(x1, 0) | &&(<=(x0, 0), <(x1, 0))
f3655_0_gcd_EQ(x0, x1) → f3655_0_gcd_EQ(x1, 0) | &&(<=(x0, 0), >(x1, 0))
f3655_0_gcd_EQ(x2, x3) → f3655_0_gcd_EQ(x3, 0) | &&(>(x2, 0), <(x3, 0))
f3655_0_gcd_EQ(x4, x5) → f10618_0_mod_LE(x4, x4, x5) | &&(&&(>(x5, x4), >(x4, 0)), >(x5, 0))
f3655_0_gcd_EQ(x4, x5) → f10618_0_mod_LE(x4, x4, x5) | &&(&&(>(x5, 0), >(x4, 0)), <(x5, x4))
f10618_0_mod_LE(x6, x61, x7) → f3655_0_gcd_EQ(x7, x6) | &&(>=(x7, x6), =(x6, x61))
f10618_0_mod_LE(x8, x81, x9) → f10618_0_mod_LE(-(x8, x9), -(x8, x9), x9) | &&(&&(<(x9, x8), >(x9, 0)), =(x8, x81))
f3655_0_gcd_EQ(x10, x101) → f3655_0_gcd_EQ(x10, 0) | &&(>(x10, 0), =(x10, x101))

(6) Obligation:

Rules:
f3655_0_gcd_EQ(x0, x1) → f3655_0_gcd_EQ(x1, 0) | &&(<=(x0, 0), <(x1, 0))
f3655_0_gcd_EQ(x0, x1) → f3655_0_gcd_EQ(x1, 0) | &&(<=(x0, 0), >(x1, 0))
f3655_0_gcd_EQ(x2, x3) → f3655_0_gcd_EQ(x3, 0) | &&(>(x2, 0), <(x3, 0))
f3655_0_gcd_EQ(x4, x5) → f10618_0_mod_LE(x4, x4, x5) | &&(&&(>(x5, x4), >(x4, 0)), >(x5, 0))
f3655_0_gcd_EQ(x4, x5) → f10618_0_mod_LE(x4, x4, x5) | &&(&&(>(x5, 0), >(x4, 0)), <(x5, x4))
f10618_0_mod_LE(x6, x61, x7) → f3655_0_gcd_EQ(x7, x6) | &&(>=(x7, x6), =(x6, x61))
f10618_0_mod_LE(x8, x81, x9) → f10618_0_mod_LE(-(x8, x9), -(x8, x9), x9) | &&(&&(<(x9, x8), >(x9, 0)), =(x8, x81))
f3655_0_gcd_EQ(x10, x101) → f3655_0_gcd_EQ(x10, 0) | &&(>(x10, 0), =(x10, x101))

(7) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained one non-trivial SCC.


(8) Obligation:

Rules:
f10618_0_mod_LE(x10, x11, x12) → f3655_0_gcd_EQ(x12, x10) | &&(>=(x12, x10), =(x10, x11))
f10618_0_mod_LE(x13, x14, x15) → f10618_0_mod_LE(-(x13, x15), -(x13, x15), x15) | &&(&&(<(x15, x13), >(x15, 0)), =(x13, x14))
f3655_0_gcd_EQ(x8, x9) → f10618_0_mod_LE(x8, x8, x9) | &&(&&(>(x9, 0), >(x8, 0)), <(x9, x8))

(9) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f10618_0_mod_LE(x9, x11, x13)] = -2 + x13
[f3655_0_gcd_EQ(x16, x18)] = -2 + x16

Therefore the following rule(s) have been dropped:


f3655_0_gcd_EQ(x6, x7) → f10618_0_mod_LE(x6, x6, x7) | &&(&&(>(x7, 0), >(x6, 0)), <(x7, x6))

(10) Obligation:

Rules:
f10618_0_mod_LE(x0, x1, x2) → f3655_0_gcd_EQ(x2, x0) | &&(>=(x2, x0), =(x0, x1))
f10618_0_mod_LE(x3, x4, x5) → f10618_0_mod_LE(-(x3, x5), -(x3, x5), x5) | &&(&&(<(x5, x3), >(x5, 0)), =(x3, x4))

(11) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained one non-trivial SCC.


(12) Obligation:

Rules:
f10618_0_mod_LE(x3, x4, x5) → f10618_0_mod_LE(-(x3, x5), -(x3, x5), x5) | &&(&&(<(x5, x3), >(x5, 0)), =(x3, x4))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


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

Therefore the following rule(s) have been dropped:


f10618_0_mod_LE(x0, x1, x2) → f10618_0_mod_LE(-(x0, x2), -(x0, x2), x2) | &&(&&(<(x2, x0), >(x2, 0)), =(x0, x1))

(14) YES