(0) Obligation:

JBC Problem based on JBC Program:
/**
* Java can do infinite data objects, too.
* Here we take the first n elements from an
* ascending infinite list of integer numbers.
*
* @author Carsten Fuhs
*/
public class Take {

public static int[] take(int n, MyIterator f) {
int[] result = new int[n];
for (int i = 0; i < n; ++i) {
if (f.hasNext()) {
result[i] = f.next();
}
else {
break;
}
}
return result;
}

public static void main(String args[]) {
int start = args[0].length();
int howMany = args[1].length();
From f = new From(start);
int[] firstHowMany = take(howMany, f);
}
}

interface MyIterator {
boolean hasNext();
int next();
}

class From implements MyIterator {

private int current;

public From(int start) {
this.current = start;
}

public boolean hasNext() {
return true;
}

public int next() {
return current++;
}
}



(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Take.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: Take.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • From: [current]
  • Marker field analysis yielded the following relations that could be markers:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 26 IRules

P rules:
f812_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90) → f815_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53)
f815_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53) → f818_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53)
f818_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53) → f823_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) | <(i90, i53)
f823_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f827_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90)
f827_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f832_0_hasNext_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90)
f832_0_hasNext_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f838_0_hasNext_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, 1)
f838_0_hasNext_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, matching1) → f840_0_take_EQ(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, 1) | =(matching1, 1)
f840_0_take_EQ(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, matching1) → f842_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) | &&(>(1, 0), =(matching1, 1))
f842_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f844_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)))
f844_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53))) → f846_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f846_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f849_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f849_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f851_0_next_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f851_0_next_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f853_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f853_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f855_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f855_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f856_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f856_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f859_0_next_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f859_0_next_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f861_0_next_IntArithmetic(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f861_0_next_IntArithmetic(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f863_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f863_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f866_0_next_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f866_0_next_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f868_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f868_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f872_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f872_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f875_0_take_Inc(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) | <(i90, i53)
f875_0_take_Inc(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f880_0_take_JMP(EOS, i53, i53, java.lang.Object(ARRAY(i53)), +(i90, 1)) | >=(i90, 0)
f880_0_take_JMP(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99) → f904_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99)
f904_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99) → f808_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99)
f808_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f812_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90)

Combined rules. Obtained 1 IRules

P rules:
f812_0_take_Load(EOS, x0, x0, java.lang.Object(ARRAY(x0)), x1, x1) → f812_0_take_Load(EOS, x0, x0, java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(>(+(x1, 1), 0), <(x1, x0))

Filtered ground terms:


f812_0_take_Load(x1, x2, x3, x4, x5, x6) → f812_0_take_Load(x2, x3, x4, x5, x6)
Cond_f812_0_take_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f812_0_take_Load(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:


f812_0_take_Load(x1, x2, x3, x4, x5) → f812_0_take_Load(x3, x5)
Cond_f812_0_take_Load(x1, x2, x3, x4, x5, x6) → Cond_f812_0_take_Load(x1, x4, x6)

Prepared 1 rules for path length conversion:

P rules:
f812_0_take_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f812_0_take_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(>(+(x1, 1), 0), <(x1, x0))

Finished conversion. Obtained 1 rules.

P rules:
f812_0_take_Load(v5, x1, x0) → f812_0_take_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(6) Obligation:

Rules:
f812_0_take_Load(v5, x1, x0) → f812_0_take_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f812_0_take_Load(x5, x7, x9)] = -x7 + x9

Therefore the following rule(s) have been dropped:


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

(8) YES