Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaC10 {
    public static void main(String[] args) {
        Random.args = args;
        int i = Random.random();
        int j = Random.random();

        while (i - j >= 1) {
			i = i - Random.random();
			int r = Random.random() + 1;
			j = j + r;
        }
    } 
}


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:
PastaC10.main([Ljava/lang/String;)V: Graph of 321 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: PastaC10.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • java.lang.String: [count]
  • Marker field analysis yielded the following relations that could be markers:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 54 IRules

P rules:
f2262_0_main_Load(EOS, i717, i718, i717) → f2264_0_main_IntArithmetic(EOS, i717, i718, i717, i718)
f2264_0_main_IntArithmetic(EOS, i717, i718, i717, i718) → f2265_0_main_ConstantStackPush(EOS, i717, i718, -(i717, i718)) | >=(i718, 0)
f2265_0_main_ConstantStackPush(EOS, i717, i718, i723) → f2268_0_main_LT(EOS, i717, i718, i723, 1)
f2268_0_main_LT(EOS, i717, i718, i727, matching1) → f2271_0_main_LT(EOS, i717, i718, i727, 1) | =(matching1, 1)
f2271_0_main_LT(EOS, i717, i718, i727, matching1) → f2274_0_main_Load(EOS, i717, i718) | &&(>=(i727, 1), =(matching1, 1))
f2274_0_main_Load(EOS, i717, i718) → f2278_0_main_InvokeMethod(EOS, i718, i717)
f2278_0_main_InvokeMethod(EOS, i718, i717) → f2279_0_random_FieldAccess(EOS, i718, i717)
f2279_0_random_FieldAccess(EOS, i718, i717) → f2282_0_random_FieldAccess(EOS, i718, i717)
f2282_0_random_FieldAccess(EOS, i718, i717) → f2287_0_random_ArrayAccess(EOS, i718, i717)
f2287_0_random_ArrayAccess(EOS, i718, i717) → f2288_0_random_ArrayAccess(EOS, i718, i717)
f2288_0_random_ArrayAccess(EOS, i718, i717) → f2293_0_random_Store(EOS, i718, i717, o1614)
f2293_0_random_Store(EOS, i718, i717, o1614) → f2297_0_random_FieldAccess(EOS, i718, i717, o1614)
f2297_0_random_FieldAccess(EOS, i718, i717, o1614) → f2299_0_random_ConstantStackPush(EOS, i718, i717, o1614)
f2299_0_random_ConstantStackPush(EOS, i718, i717, o1614) → f2304_0_random_IntArithmetic(EOS, i718, i717, o1614)
f2304_0_random_IntArithmetic(EOS, i718, i717, o1614) → f2308_0_random_FieldAccess(EOS, i718, i717, o1614)
f2308_0_random_FieldAccess(EOS, i718, i717, o1614) → f2311_0_random_Load(EOS, i718, i717, o1614)
f2311_0_random_Load(EOS, i718, i717, o1614) → f2318_0_random_InvokeMethod(EOS, i718, i717, o1614)
f2318_0_random_InvokeMethod(EOS, i718, i717, java.lang.Object(o1641sub)) → f2321_0_random_InvokeMethod(EOS, i718, i717, java.lang.Object(o1641sub))
f2321_0_random_InvokeMethod(EOS, i718, i717, java.lang.Object(o1641sub)) → f2324_0_length_Load(EOS, i718, i717, java.lang.Object(o1641sub), java.lang.Object(o1641sub))
f2324_0_length_Load(EOS, i718, i717, java.lang.Object(o1641sub), java.lang.Object(o1641sub)) → f2338_0_length_FieldAccess(EOS, i718, i717, java.lang.Object(o1641sub), java.lang.Object(o1641sub))
f2338_0_length_FieldAccess(EOS, i718, i717, java.lang.Object(java.lang.String(o1655sub, i763)), java.lang.Object(java.lang.String(o1655sub, i763))) → f2340_0_length_FieldAccess(EOS, i718, i717, java.lang.Object(java.lang.String(o1655sub, i763)), java.lang.Object(java.lang.String(o1655sub, i763))) | >=(i763, 0)
f2340_0_length_FieldAccess(EOS, i718, i717, java.lang.Object(java.lang.String(o1655sub, i763)), java.lang.Object(java.lang.String(o1655sub, i763))) → f2348_0_length_Return(EOS, i718, i717, java.lang.Object(java.lang.String(o1655sub, i763)), i763)
f2348_0_length_Return(EOS, i718, i717, java.lang.Object(java.lang.String(o1655sub, i763)), i763) → f2352_0_random_Return(EOS, i718, i717, i763)
f2352_0_random_Return(EOS, i718, i717, i763) → f2355_0_main_IntArithmetic(EOS, i718, i717, i763)
f2355_0_main_IntArithmetic(EOS, i718, i717, i763) → f2364_0_main_Store(EOS, i718, -(i717, i763)) | >=(i763, 0)
f2364_0_main_Store(EOS, i718, i773) → f2372_0_main_InvokeMethod(EOS, i773, i718)
f2372_0_main_InvokeMethod(EOS, i773, i718) → f2378_0_random_FieldAccess(EOS, i773, i718)
f2378_0_random_FieldAccess(EOS, i773, i718) → f2399_0_random_FieldAccess(EOS, i773, i718)
f2399_0_random_FieldAccess(EOS, i773, i718) → f2409_0_random_ArrayAccess(EOS, i773, i718)
f2409_0_random_ArrayAccess(EOS, i773, i718) → f2417_0_random_ArrayAccess(EOS, i773, i718)
f2417_0_random_ArrayAccess(EOS, i773, i718) → f2429_0_random_Store(EOS, i773, i718, o1731)
f2429_0_random_Store(EOS, i773, i718, o1731) → f2441_0_random_FieldAccess(EOS, i773, i718, o1731)
f2441_0_random_FieldAccess(EOS, i773, i718, o1731) → f2451_0_random_ConstantStackPush(EOS, i773, i718, o1731)
f2451_0_random_ConstantStackPush(EOS, i773, i718, o1731) → f2474_0_random_IntArithmetic(EOS, i773, i718, o1731)
f2474_0_random_IntArithmetic(EOS, i773, i718, o1731) → f2492_0_random_FieldAccess(EOS, i773, i718, o1731)
f2492_0_random_FieldAccess(EOS, i773, i718, o1731) → f2510_0_random_Load(EOS, i773, i718, o1731)
f2510_0_random_Load(EOS, i773, i718, o1731) → f2533_0_random_InvokeMethod(EOS, i773, i718, o1731)
f2533_0_random_InvokeMethod(EOS, i773, i718, java.lang.Object(o1831sub)) → f2545_0_random_InvokeMethod(EOS, i773, i718, java.lang.Object(o1831sub))
f2545_0_random_InvokeMethod(EOS, i773, i718, java.lang.Object(o1831sub)) → f2555_0_length_Load(EOS, i773, i718, java.lang.Object(o1831sub), java.lang.Object(o1831sub))
f2555_0_length_Load(EOS, i773, i718, java.lang.Object(o1831sub), java.lang.Object(o1831sub)) → f2584_0_length_FieldAccess(EOS, i773, i718, java.lang.Object(o1831sub), java.lang.Object(o1831sub))
f2584_0_length_FieldAccess(EOS, i773, i718, java.lang.Object(java.lang.String(o1861sub, i856)), java.lang.Object(java.lang.String(o1861sub, i856))) → f2590_0_length_FieldAccess(EOS, i773, i718, java.lang.Object(java.lang.String(o1861sub, i856)), java.lang.Object(java.lang.String(o1861sub, i856))) | >=(i856, 0)
f2590_0_length_FieldAccess(EOS, i773, i718, java.lang.Object(java.lang.String(o1861sub, i856)), java.lang.Object(java.lang.String(o1861sub, i856))) → f2608_0_length_Return(EOS, i773, i718, java.lang.Object(java.lang.String(o1861sub, i856)), i856)
f2608_0_length_Return(EOS, i773, i718, java.lang.Object(java.lang.String(o1861sub, i856)), i856) → f2617_0_random_Return(EOS, i773, i718, i856)
f2617_0_random_Return(EOS, i773, i718, i856) → f2619_0_main_ConstantStackPush(EOS, i773, i718, i856)
f2619_0_main_ConstantStackPush(EOS, i773, i718, i856) → f2632_0_main_IntArithmetic(EOS, i773, i718, i856, 1)
f2632_0_main_IntArithmetic(EOS, i773, i718, i856, matching1) → f2644_0_main_Store(EOS, i773, i718, +(i856, 1)) | &&(>=(i856, 0), =(matching1, 1))
f2644_0_main_Store(EOS, i773, i718, i872) → f2651_0_main_Load(EOS, i773, i718, i872)
f2651_0_main_Load(EOS, i773, i718, i872) → f2670_0_main_Load(EOS, i773, i872, i718)
f2670_0_main_Load(EOS, i773, i872, i718) → f2687_0_main_IntArithmetic(EOS, i773, i718, i872)
f2687_0_main_IntArithmetic(EOS, i773, i718, i872) → f2697_0_main_Store(EOS, i773, +(i718, i872)) | &&(>=(i718, 0), >(i872, 0))
f2697_0_main_Store(EOS, i773, i882) → f2714_0_main_JMP(EOS, i773, i882)
f2714_0_main_JMP(EOS, i773, i882) → f2748_0_main_Load(EOS, i773, i882)
f2748_0_main_Load(EOS, i773, i882) → f2255_0_main_Load(EOS, i773, i882)
f2255_0_main_Load(EOS, i717, i718) → f2262_0_main_Load(EOS, i717, i718, i717)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f2262_0_main_Load(x1, x2, x3, x4) → f2262_0_main_Load(x2, x3, x4)
Cond_f2262_0_main_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f2262_0_main_Load(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:


f2262_0_main_Load(x1, x2, x3) → f2262_0_main_Load(x2, x3)
Cond_f2262_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f2262_0_main_Load(x1, x3, x4, x5, x6)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

P rules:
f2262_0_main_Load(x0, x1) → f2262_0_main_Load(+(x0, +(x2, 1)), -(x1, x3)) | &&(&&(&&(>(x3, -1), >(x2, -1)), >(x0, -1)), >=(-(x1, x0), 1))

(6) Obligation:

Rules:
f2262_0_main_Load(x0, x1) → f2262_0_main_Load(+(x0, +(x2, 1)), -(x1, x3)) | &&(&&(&&(>(x3, -1), >(x2, -1)), >(x0, -1)), >=(-(x1, x0), 1))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f2262_0_main_Load(x5, x7)] = -x5 + x7

Therefore the following rule(s) have been dropped:


f2262_0_main_Load(x0, x1) → f2262_0_main_Load(+(x0, +(x2, 1)), -(x1, x3)) | &&(&&(&&(>(x3, -1), >(x2, -1)), >(x0, -1)), >=(-(x1, x0), 1))

(8) YES