Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 895 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 43 ms)
↳6 intTRS
↳7 TerminationGraphProcessor (⇒, 12 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 GCD2 {
  public static int mod(int a, int b) {
    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 && a >= 0 && 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:
GCD2.main([Ljava/lang/String;)V: Graph of 218 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: GCD2.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 43 IRules

P rules:
f1347_0_gcd_EQ(EOS, i182, i200, i200) → f1349_0_gcd_EQ(EOS, i182, i200, i200)
f1349_0_gcd_EQ(EOS, i182, i200, i200) → f1352_0_gcd_Load(EOS, i182, i200) | !(=(i200, 0))
f1352_0_gcd_Load(EOS, i182, i200) → f1355_0_gcd_LT(EOS, i182, i200, i182)
f1355_0_gcd_LT(EOS, i182, i200, i182) → f1359_0_gcd_Load(EOS, i182, i200) | >=(i182, 0)
f1359_0_gcd_Load(EOS, i182, i200) → f1364_0_gcd_LT(EOS, i182, i200, i200)
f1364_0_gcd_LT(EOS, i182, i207, i207) → f1369_0_gcd_LT(EOS, i182, i207, i207)
f1369_0_gcd_LT(EOS, i182, i207, i207) → f1378_0_gcd_Load(EOS, i182, i207) | >=(i207, 0)
f1378_0_gcd_Load(EOS, i182, i207) → f1382_0_gcd_Store(EOS, i182, i207, i207)
f1382_0_gcd_Store(EOS, i182, i207, i207) → f1386_0_gcd_Load(EOS, i182, i207, i207)
f1386_0_gcd_Load(EOS, i182, i207, i207) → f1389_0_gcd_Load(EOS, i207, i207, i182)
f1389_0_gcd_Load(EOS, i207, i207, i182) → f1392_0_gcd_InvokeMethod(EOS, i207, i182, i207)
f1392_0_gcd_InvokeMethod(EOS, i207, i182, i207) → f1394_0_mod_Load(EOS, i207, i182, i207, i182, i207)
f1394_0_mod_Load(EOS, i207, i182, i207, i182, i207) → f1396_0_mod_Load(EOS, i207, i182, i207, i182, i207, i182)
f1396_0_mod_Load(EOS, i207, i182, i207, i182, i207, i182) → f1398_0_mod_NE(EOS, i207, i182, i207, i182, i207, i182, i207)
f1398_0_mod_NE(EOS, i207, i182, i207, i182, i207, i182, i207) → f1400_0_mod_NE(EOS, i207, i182, i207, i182, i207, i182, i207)
f1398_0_mod_NE(EOS, i207, i207, i207, i207, i207, i207, i207) → f1401_0_mod_NE(EOS, i207, i207, i207, i207, i207, i207, i207)
f1400_0_mod_NE(EOS, i207, i182, i207, i182, i207, i182, i207) → f1404_0_mod_Load(EOS, i207, i182, i207, i182, i207) | !(=(i182, i207))
f1404_0_mod_Load(EOS, i207, i182, i207, i182, i207) → f1460_0_mod_Load(EOS, i207, i182, i207, i182, i207)
f1460_0_mod_Load(EOS, i207, i182, i207, i214, i207) → f1470_0_mod_Load(EOS, i207, i182, i207, i214, i207, i214)
f1470_0_mod_Load(EOS, i207, i182, i207, i214, i207, i214) → f1970_0_mod_LE(EOS, i207, i182, i207, i214, i207, i214, i207)
f1970_0_mod_LE(EOS, i207, i182, i207, i214, i207, i214, i207) → f1972_0_mod_LE(EOS, i207, i182, i207, i214, i207, i214, i207)
f1970_0_mod_LE(EOS, i207, i182, i207, i214, i207, i214, i207) → f1973_0_mod_LE(EOS, i207, i182, i207, i214, i207, i214, i207)
f1972_0_mod_LE(EOS, i207, i182, i207, i214, i207, i214, i207) → f1975_0_mod_Load(EOS, i207, i182, i207, i214) | <=(i214, i207)
f1975_0_mod_Load(EOS, i207, i182, i207, i214) → f1978_0_mod_Return(EOS, i207, i182, i207, i214)
f1978_0_mod_Return(EOS, i207, i182, i207, i214) → f1984_0_gcd_Store(EOS, i207, i214)
f1984_0_gcd_Store(EOS, i207, i214) → f1988_0_gcd_Load(EOS, i214, i207)
f1988_0_gcd_Load(EOS, i214, i207) → f1991_0_gcd_Store(EOS, i214, i207)
f1991_0_gcd_Store(EOS, i214, i207) → f1994_0_gcd_JMP(EOS, i207, i214)
f1994_0_gcd_JMP(EOS, i207, i214) → f2007_0_gcd_Load(EOS, i207, i214)
f2007_0_gcd_Load(EOS, i207, i214) → f1294_0_gcd_Load(EOS, i207, i214)
f1294_0_gcd_Load(EOS, i182, i183) → f1347_0_gcd_EQ(EOS, i182, i183, i183)
f1973_0_mod_LE(EOS, i207, i182, i207, i214, i207, i214, i207) → f1976_0_mod_Load(EOS, i207, i182, i207, i214, i207) | >(i214, i207)
f1976_0_mod_Load(EOS, i207, i182, i207, i214, i207) → f1979_0_mod_Load(EOS, i207, i182, i207, i207, i214)
f1979_0_mod_Load(EOS, i207, i182, i207, i207, i214) → f1986_0_mod_IntArithmetic(EOS, i207, i182, i207, i207, i214, i207)
f1986_0_mod_IntArithmetic(EOS, i207, i182, i207, i207, i214, i207) → f1989_0_mod_Store(EOS, i207, i182, i207, i207, -(i214, i207)) | >(i207, 0)
f1989_0_mod_Store(EOS, i207, i182, i207, i207, i375) → f1992_0_mod_JMP(EOS, i207, i182, i207, i375, i207)
f1992_0_mod_JMP(EOS, i207, i182, i207, i375, i207) → f2000_0_mod_Load(EOS, i207, i182, i207, i375, i207)
f2000_0_mod_Load(EOS, i207, i182, i207, i375, i207) → f1460_0_mod_Load(EOS, i207, i182, i207, i375, i207)
f1401_0_mod_NE(EOS, i207, i207, i207, i207, i207, i207, i207) → f1406_0_mod_ConstantStackPush(EOS, i207, i207, i207, i207, i207)
f1406_0_mod_ConstantStackPush(EOS, i207, i207, i207, i207, i207) → f1410_0_mod_Return(EOS, i207, i207, i207, i207, i207, 0)
f1410_0_mod_Return(EOS, i207, i207, i207, i207, i207, matching1) → f1414_0_gcd_Store(EOS, i207, 0) | =(matching1, 0)
f1414_0_gcd_Store(EOS, i207, matching1) → f1437_0_gcd_Store(EOS, i207, 0) | =(matching1, 0)
f1437_0_gcd_Store(EOS, i207, i182) → f1984_0_gcd_Store(EOS, i207, i182)

Combined rules. Obtained 4 IRules

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

Filtered ground terms:


f1347_0_gcd_EQ(x1, x2, x3, x4) → f1347_0_gcd_EQ(x2, x3, x4)
Cond_f1347_0_gcd_EQ(x1, x2, x3, x4, x5) → Cond_f1347_0_gcd_EQ(x1, x3, x4, x5)
f1970_0_mod_LE(x1, x2, x3, x4, x5, x6, x7, x8) → f1970_0_mod_LE(x2, x3, x4, x5, x6, x7, x8)
Cond_f1970_0_mod_LE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1970_0_mod_LE(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1970_0_mod_LE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1970_0_mod_LE1(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1347_0_gcd_EQ1(x1, x2, x3, x4, x5) → Cond_f1347_0_gcd_EQ1(x1, x3, x4, x5)

Filtered duplicate terms:


f1347_0_gcd_EQ(x1, x2, x3) → f1347_0_gcd_EQ(x1, x3)
Cond_f1347_0_gcd_EQ(x1, x2, x3, x4) → Cond_f1347_0_gcd_EQ(x1, x2, x4)
f1970_0_mod_LE(x1, x2, x3, x4, x5, x6, x7) → f1970_0_mod_LE(x2, x4, x6, x7)
Cond_f1970_0_mod_LE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1970_0_mod_LE(x1, x3, x7, x8)
Cond_f1970_0_mod_LE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1970_0_mod_LE1(x1, x3, x7, x8)
Cond_f1347_0_gcd_EQ1(x1, x2, x3, x4) → Cond_f1347_0_gcd_EQ1(x1, x4)

Filtered unneeded terms:


f1970_0_mod_LE(x1, x2, x3, x4) → f1970_0_mod_LE(x2, x3, x4)
Cond_f1970_0_mod_LE(x1, x2, x3, x4) → Cond_f1970_0_mod_LE(x1, x3, x4)
Cond_f1970_0_mod_LE1(x1, x2, x3, x4) → Cond_f1970_0_mod_LE1(x1, x3, x4)

Prepared 4 rules for path length conversion:

P rules:
f1347_0_gcd_EQ(x0, x1) → f1970_0_mod_LE(x0, x0, x1) | &&(&&(>(x1, 0), !(=(x0, x1))), >(+(x0, 1), 0))
f1970_0_mod_LE(x2, x2, x0) → f1347_0_gcd_EQ(x0, x2) | <=(x2, x0)
f1970_0_mod_LE(x2, x2, x0) → f1970_0_mod_LE(-(x2, x0), -(x2, x0), x0) | &&(>(x0, 0), >(x2, x0))
f1347_0_gcd_EQ(x0, x0) → f1347_0_gcd_EQ(x0, 0) | >(x0, 0)

Finished conversion. Obtained 5 rules.

P rules:
f1347_0_gcd_EQ(x0, x1) → f1970_0_mod_LE(x0, x0, x1) | &&(&&(>(x1, x0), >(x0, -1)), >(x1, 0))
f1347_0_gcd_EQ(x0, x1) → f1970_0_mod_LE(x0, x0, x1) | &&(&&(>(x1, 0), >(x0, -1)), <(x1, x0))
f1970_0_mod_LE(x2, x21, x3) → f1347_0_gcd_EQ(x3, x2) | &&(>=(x3, x2), =(x2, x21))
f1970_0_mod_LE(x4, x41, x5) → f1970_0_mod_LE(-(x4, x5), -(x4, x5), x5) | &&(&&(<(x5, x4), >(x5, 0)), =(x4, x41))
f1347_0_gcd_EQ(x6, x61) → f1347_0_gcd_EQ(x6, 0) | &&(>(x6, 0), =(x6, x61))

(6) Obligation:

Rules:
f1347_0_gcd_EQ(x0, x1) → f1970_0_mod_LE(x0, x0, x1) | &&(&&(>(x1, x0), >(x0, -1)), >(x1, 0))
f1347_0_gcd_EQ(x0, x1) → f1970_0_mod_LE(x0, x0, x1) | &&(&&(>(x1, 0), >(x0, -1)), <(x1, x0))
f1970_0_mod_LE(x2, x21, x3) → f1347_0_gcd_EQ(x3, x2) | &&(>=(x3, x2), =(x2, x21))
f1970_0_mod_LE(x4, x41, x5) → f1970_0_mod_LE(-(x4, x5), -(x4, x5), x5) | &&(&&(<(x5, x4), >(x5, 0)), =(x4, x41))
f1347_0_gcd_EQ(x6, x61) → f1347_0_gcd_EQ(x6, 0) | &&(>(x6, 0), =(x6, x61))

(7) TerminationGraphProcessor (SOUND transformation)

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


(8) Obligation:

Rules:
f1970_0_mod_LE(x4, x5, x6) → f1347_0_gcd_EQ(x6, x4) | &&(>=(x6, x4), =(x4, x5))
f1970_0_mod_LE(x7, x8, x9) → f1970_0_mod_LE(-(x7, x9), -(x7, x9), x9) | &&(&&(<(x9, x7), >(x9, 0)), =(x7, x8))
f1347_0_gcd_EQ(x2, x3) → f1970_0_mod_LE(x2, x2, x3) | &&(&&(>(x3, 0), >(x2, -1)), <(x3, x2))

(9) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f1970_0_mod_LE(x9, x11, x13)] = -2 + x13
[f1347_0_gcd_EQ(x16, x18)] = -2 + x16

Therefore the following rule(s) have been dropped:


f1347_0_gcd_EQ(x6, x7) → f1970_0_mod_LE(x6, x6, x7) | &&(&&(>(x7, 0), >(x6, -1)), <(x7, x6))

(10) Obligation:

Rules:
f1970_0_mod_LE(x0, x1, x2) → f1347_0_gcd_EQ(x2, x0) | &&(>=(x2, x0), =(x0, x1))
f1970_0_mod_LE(x3, x4, x5) → f1970_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:
f1970_0_mod_LE(x3, x4, x5) → f1970_0_mod_LE(-(x3, x5), -(x3, x5), x5) | &&(&&(<(x5, x3), >(x5, 0)), =(x3, x4))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


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

Therefore the following rule(s) have been dropped:


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

(14) YES