Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 627 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 32 ms)
↳6 intTRS
↳7 PolynomialOrderProcessor (⇒, 0 ms)
↳8 intTRS
↳9 LinearRankingProcessor (⇔, 0 ms)
↳10 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 PastaC3 {
    public static void main(String[] args) {
        Random.args = args;
        int x = Random.random();
        int y = Random.random();
        int z = Random.random();

        while (x < y) {
            if (x < z) {
                x++;
            } else {
                z++;
            }
        }
    }
}


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:
PastaC3.main([Ljava/lang/String;)V: Graph of 249 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: PastaC3.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 16 IRules

P rules:
f634_0_main_Load(EOS, i18, i45, i92, i18) → f646_0_main_GE(EOS, i18, i45, i92, i18, i45)
f646_0_main_GE(EOS, i18, i45, i92, i18, i45) → f667_0_main_GE(EOS, i18, i45, i92, i18, i45)
f667_0_main_GE(EOS, i18, i45, i92, i18, i45) → f679_0_main_Load(EOS, i18, i45, i92) | <(i18, i45)
f679_0_main_Load(EOS, i18, i45, i92) → f687_0_main_Load(EOS, i18, i45, i92, i18)
f687_0_main_Load(EOS, i18, i45, i92, i18) → f703_0_main_GE(EOS, i18, i45, i92, i18, i92)
f703_0_main_GE(EOS, i18, i45, i92, i18, i92) → f718_0_main_GE(EOS, i18, i45, i92, i18, i92)
f703_0_main_GE(EOS, i18, i45, i92, i18, i92) → f719_0_main_GE(EOS, i18, i45, i92, i18, i92)
f718_0_main_GE(EOS, i18, i45, i92, i18, i92) → f733_0_main_Inc(EOS, i18, i45, i92) | >=(i18, i92)
f733_0_main_Inc(EOS, i18, i45, i92) → f748_0_main_JMP(EOS, i18, i45, +(i92, 1)) | >=(i92, 0)
f748_0_main_JMP(EOS, i18, i45, i110) → f804_0_main_Load(EOS, i18, i45, i110)
f804_0_main_Load(EOS, i18, i45, i110) → f622_0_main_Load(EOS, i18, i45, i110)
f622_0_main_Load(EOS, i18, i45, i92) → f634_0_main_Load(EOS, i18, i45, i92, i18)
f719_0_main_GE(EOS, i18, i45, i92, i18, i92) → f735_0_main_Inc(EOS, i18, i45, i92) | <(i18, i92)
f735_0_main_Inc(EOS, i18, i45, i92) → f750_0_main_JMP(EOS, +(i18, 1), i45, i92) | >=(i18, 0)
f750_0_main_JMP(EOS, i111, i45, i92) → f812_0_main_Load(EOS, i111, i45, i92)
f812_0_main_Load(EOS, i111, i45, i92) → f622_0_main_Load(EOS, i111, i45, i92)

Combined rules. Obtained 2 IRules

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

Filtered ground terms:


f634_0_main_Load(x1, x2, x3, x4, x5) → f634_0_main_Load(x2, x3, x4, x5)
Cond_f634_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f634_0_main_Load(x1, x3, x4, x5, x6)
Cond_f634_0_main_Load1(x1, x2, x3, x4, x5, x6) → Cond_f634_0_main_Load1(x1, x3, x4, x5, x6)

Filtered duplicate terms:


f634_0_main_Load(x1, x2, x3, x4) → f634_0_main_Load(x2, x3, x4)
Cond_f634_0_main_Load(x1, x2, x3, x4, x5) → Cond_f634_0_main_Load(x1, x3, x4, x5)
Cond_f634_0_main_Load1(x1, x2, x3, x4, x5) → Cond_f634_0_main_Load1(x1, x3, x4, x5)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 2 rules.

P rules:
f634_0_main_Load(x0, x1, x2) → f634_0_main_Load(x0, +(x1, 1), x2) | &&(&&(>=(x2, x1), >(x1, -1)), <(x2, x0))
f634_0_main_Load(x3, x4, x5) → f634_0_main_Load(x3, x4, +(x5, 1)) | &&(&&(>(x5, -1), <(x5, x3)), <(x5, x4))

(6) Obligation:

Rules:
f634_0_main_Load(x0, x1, x2) → f634_0_main_Load(x0, +(x1, 1), x2) | &&(&&(>=(x2, x1), >(x1, -1)), <(x2, x0))
f634_0_main_Load(x3, x4, x5) → f634_0_main_Load(x3, x4, +(x5, 1)) | &&(&&(>(x5, -1), <(x5, x3)), <(x5, x4))

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f634_0_main_Load(x7, x9, x11)] = -x11 + x7

Therefore the following rule(s) have been dropped:


f634_0_main_Load(x3, x4, x5) → f634_0_main_Load(x3, x4, +(x5, 1)) | &&(&&(>(x5, -1), <(x5, x3)), <(x5, x4))

(8) Obligation:

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

(9) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f634_0_main_Load(x)] = (-1)·x2 + 1·x3

where x = (x1, ... ,xn).



Therefore the following rule(s) have been dropped:


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

(10) YES