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 PastaC7 {
    public static void main(String[] args) {
        Random.args = args;
        int i = Random.random();
        int j = Random.random();
        int k = Random.random();

        while (i <= 100 && j <= k) {
            int t = i;
            i = j;
            j = i + 1;
            k--;
        }
    }
}


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:
PastaC7.main([Ljava/lang/String;)V: Graph of 259 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: PastaC7.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 19 IRules

P rules:
f1077_0_main_ConstantStackPush(EOS, i210, i211, i212, i210) → f1081_0_main_GT(EOS, i210, i211, i212, i210, 100)
f1081_0_main_GT(EOS, i224, i211, i212, i224, matching1) → f1084_0_main_GT(EOS, i224, i211, i212, i224, 100) | =(matching1, 100)
f1084_0_main_GT(EOS, i224, i211, i212, i224, matching1) → f1087_0_main_Load(EOS, i224, i211, i212) | &&(<=(i224, 100), =(matching1, 100))
f1087_0_main_Load(EOS, i224, i211, i212) → f1091_0_main_Load(EOS, i224, i211, i212, i211)
f1091_0_main_Load(EOS, i224, i211, i212, i211) → f1094_0_main_GT(EOS, i224, i211, i212, i211, i212)
f1094_0_main_GT(EOS, i224, i211, i212, i211, i212) → f1097_0_main_GT(EOS, i224, i211, i212, i211, i212)
f1097_0_main_GT(EOS, i224, i211, i212, i211, i212) → f1106_0_main_Load(EOS, i224, i211, i212) | <=(i211, i212)
f1106_0_main_Load(EOS, i224, i211, i212) → f1109_0_main_Store(EOS, i211, i212, i224)
f1109_0_main_Store(EOS, i211, i212, i224) → f1110_0_main_Load(EOS, i211, i212)
f1110_0_main_Load(EOS, i211, i212) → f1113_0_main_Store(EOS, i212, i211)
f1113_0_main_Store(EOS, i212, i211) → f1115_0_main_Load(EOS, i211, i212)
f1115_0_main_Load(EOS, i211, i212) → f1116_0_main_ConstantStackPush(EOS, i211, i212, i211)
f1116_0_main_ConstantStackPush(EOS, i211, i212, i211) → f1118_0_main_IntArithmetic(EOS, i211, i212, i211, 1)
f1118_0_main_IntArithmetic(EOS, i211, i212, i211, matching1) → f1120_0_main_Store(EOS, i211, i212, +(i211, 1)) | &&(>=(i211, 0), =(matching1, 1))
f1120_0_main_Store(EOS, i211, i212, i230) → f1122_0_main_Inc(EOS, i211, i230, i212)
f1122_0_main_Inc(EOS, i211, i230, i212) → f1124_0_main_JMP(EOS, i211, i230, +(i212, -1))
f1124_0_main_JMP(EOS, i211, i230, i231) → f1146_0_main_Load(EOS, i211, i230, i231)
f1146_0_main_Load(EOS, i211, i230, i231) → f1073_0_main_Load(EOS, i211, i230, i231)
f1073_0_main_Load(EOS, i210, i211, i212) → f1077_0_main_ConstantStackPush(EOS, i210, i211, i212, i210)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f1077_0_main_ConstantStackPush(x1, x2, x3, x4, x5) → f1077_0_main_ConstantStackPush(x2, x3, x4, x5)
Cond_f1077_0_main_ConstantStackPush(x1, x2, x3, x4, x5, x6) → Cond_f1077_0_main_ConstantStackPush(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f1077_0_main_ConstantStackPush(x1, x2, x3, x4) → f1077_0_main_ConstantStackPush(x2, x3, x4)
Cond_f1077_0_main_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f1077_0_main_ConstantStackPush(x1, x3, x4, x5)

Filtered unneeded terms:

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

Prepared 1 rules for path length conversion:

P rules:
f1077_0_main_ConstantStackPush(x1, x2, x0) → f1077_0_main_ConstantStackPush(+(x1, 1), -(x2, 1), x1) | &&(&&(>=(x2, x1), <=(x0, 100)), >(+(x1, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f1077_0_main_ConstantStackPush(x0, x1, x2) → f1077_0_main_ConstantStackPush(+(x0, 1), -(x1, 1), x0) | &&(&&(<=(x2, 100), >(x0, -1)), >=(x1, x0))

(6) Obligation:

Rules:
f1077_0_main_ConstantStackPush(x0, x1, x2) → f1077_0_main_ConstantStackPush(+(x0, 1), -(x1, 1), x0) | &&(&&(<=(x2, 100), >(x0, -1)), >=(x1, x0))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1077_0_main_ConstantStackPush(x4, x6, x8)] = 100 - x4 + 100·x6 - x8

Therefore the following rule(s) have been dropped:

f1077_0_main_ConstantStackPush(x0, x1, x2) → f1077_0_main_ConstantStackPush(+(x0, 1), -(x1, 1), x0) | &&(&&(<=(x2, 100), >(x0, -1)), >=(x1, x0))

(8) YES