Termination of the given JBC could be proven:

(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 PastaC11 {
    public static void main(String[] args) {
        Random.args = args;
        int x = Random.random();
        int y = Random.random();

        while (true) {
			if (x >= 0) {
				x--;
				y = Random.random();
			} else if (y >= 0) {
				y--;
			} else {
				break;
			}
        }
    } 
}


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:
PastaC11.main([Ljava/lang/String;)V: Graph of 252 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: PastaC11.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 33 IRules

P rules:
f2155_0_main_LT(EOS, matching1, i779, matching2) → f2156_0_main_LT(EOS, -1, i779, -1) | &&(=(matching1, -1), =(matching2, -1))
f2155_0_main_LT(EOS, i789, i779, i789) → f2157_0_main_LT(EOS, i789, i779, i789)
f2156_0_main_LT(EOS, matching1, i779, matching2) → f2159_0_main_Load(EOS, -1, i779) | &&(&&(<(-1, 0), =(matching1, -1)), =(matching2, -1))
f2159_0_main_Load(EOS, matching1, i779) → f2163_0_main_LT(EOS, -1, i779, i779) | =(matching1, -1)
f2163_0_main_LT(EOS, matching1, i795, i795) → f2169_0_main_LT(EOS, -1, i795, i795) | =(matching1, -1)
f2169_0_main_LT(EOS, matching1, i795, i795) → f2174_0_main_Inc(EOS, -1, i795) | &&(>=(i795, 0), =(matching1, -1))
f2174_0_main_Inc(EOS, matching1, i795) → f2179_0_main_JMP(EOS, -1, +(i795, -1)) | &&(>=(i795, 0), =(matching1, -1))
f2179_0_main_JMP(EOS, matching1, i797) → f2193_0_main_Load(EOS, -1, i797) | =(matching1, -1)
f2193_0_main_Load(EOS, matching1, i797) → f2147_0_main_Load(EOS, -1, i797) | =(matching1, -1)
f2147_0_main_Load(EOS, i778, i779) → f2155_0_main_LT(EOS, i778, i779, i778)
f2157_0_main_LT(EOS, i789, i779, i789) → f2161_0_main_Inc(EOS, i789) | >=(i789, 0)
f2161_0_main_Inc(EOS, i789) → f2165_0_main_InvokeMethod(EOS, +(i789, -1)) | >=(i789, 0)
f2165_0_main_InvokeMethod(EOS, i793) → f2170_0_random_FieldAccess(EOS, i793)
f2170_0_random_FieldAccess(EOS, i793) → f2183_0_random_FieldAccess(EOS, i793)
f2183_0_random_FieldAccess(EOS, i793) → f2200_0_random_ArrayAccess(EOS, i793)
f2200_0_random_ArrayAccess(EOS, i793) → f2712_0_random_ArrayAccess(EOS, i793)
f2712_0_random_ArrayAccess(EOS, i793) → f2718_0_random_Store(EOS, i793, o754)
f2718_0_random_Store(EOS, i793, o754) → f2724_0_random_FieldAccess(EOS, i793, o754)
f2724_0_random_FieldAccess(EOS, i793, o754) → f2728_0_random_ConstantStackPush(EOS, i793, o754)
f2728_0_random_ConstantStackPush(EOS, i793, o754) → f2736_0_random_IntArithmetic(EOS, i793, o754)
f2736_0_random_IntArithmetic(EOS, i793, o754) → f2741_0_random_FieldAccess(EOS, i793, o754)
f2741_0_random_FieldAccess(EOS, i793, o754) → f2745_0_random_Load(EOS, i793, o754)
f2745_0_random_Load(EOS, i793, o754) → f2760_0_random_InvokeMethod(EOS, i793, o754)
f2760_0_random_InvokeMethod(EOS, i793, java.lang.Object(o782sub)) → f2765_0_random_InvokeMethod(EOS, i793, java.lang.Object(o782sub))
f2765_0_random_InvokeMethod(EOS, i793, java.lang.Object(o782sub)) → f2770_0_length_Load(EOS, i793, java.lang.Object(o782sub), java.lang.Object(o782sub))
f2770_0_length_Load(EOS, i793, java.lang.Object(o782sub), java.lang.Object(o782sub)) → f2789_0_length_FieldAccess(EOS, i793, java.lang.Object(o782sub), java.lang.Object(o782sub))
f2789_0_length_FieldAccess(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), java.lang.Object(java.lang.String(o795sub, i1032))) → f2791_0_length_FieldAccess(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), java.lang.Object(java.lang.String(o795sub, i1032))) | >=(i1032, 0)
f2791_0_length_FieldAccess(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), java.lang.Object(java.lang.String(o795sub, i1032))) → f2805_0_length_Return(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), i1032)
f2805_0_length_Return(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), i1032) → f2813_0_random_Return(EOS, i793, i1032)
f2813_0_random_Return(EOS, i793, i1032) → f2816_0_main_Store(EOS, i793, i1032)
f2816_0_main_Store(EOS, i793, i1032) → f2831_0_main_JMP(EOS, i793, i1032)
f2831_0_main_JMP(EOS, i793, i1032) → f2847_0_main_Load(EOS, i793, i1032)
f2847_0_main_Load(EOS, i793, i1032) → f2147_0_main_Load(EOS, i793, i1032)

Combined rules. Obtained 2 IRules

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

Filtered ground terms:

f2155_0_main_LT(x1, x2, x3, x4) → f2155_0_main_LT(x2, x3, x4)
Cond_f2155_0_main_LT(x1, x2, x3, x4, x5) → Cond_f2155_0_main_LT(x1, x4)
Cond_f2155_0_main_LT1(x1, x2, x3, x4, x5, x6) → Cond_f2155_0_main_LT1(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f2155_0_main_LT(x1, x2, x3) → f2155_0_main_LT(x2, x3)
Cond_f2155_0_main_LT1(x1, x2, x3, x4, x5) → Cond_f2155_0_main_LT1(x1, x3, x4, x5)

Filtered unneeded terms:

Cond_f2155_0_main_LT1(x1, x2, x3, x4) → Cond_f2155_0_main_LT1(x1, x3, x4)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 2 rules.

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

(6) Obligation:

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

(7) TerminationGraphProcessor (SOUND transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

Rules:
f2155_0_main_LT(x2, x3) → f2155_0_main_LT(x4, -(x3, 1)) | &&(>(x3, -1), >(x4, -1))

(10) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2155_0_main_LT(x4, x6)] = x6

Therefore the following rule(s) have been dropped:

f2155_0_main_LT(x0, x1) → f2155_0_main_LT(x2, -(x1, 1)) | &&(>(x1, -1), >(x2, -1))

(11) YES

(12) Obligation:

Rules:
f2155_0_main_LT(x0, x1) → f2155_0_main_LT(-(x0, 1), -1) | &&(>(x0, -1), =(-1, x1))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2155_0_main_LT(x3, x5)] = x3

Therefore the following rule(s) have been dropped:

f2155_0_main_LT(x0, x1) → f2155_0_main_LT(-(x0, 1), -1) | &&(>(x0, -1), =(-1, x1))

(14) YES