(0) Obligation:
Need to prove time_complexity of the following 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 PastaA7 {
public static void main(int x, int y, int z) {
while (x > y && x > z) {
y++;
z++;
}
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
PastaA7.main(III)V: Graph of 57 nodes with 1 SCC.
(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(7)) transformation)
Extracted set of 50 edges for the analysis of TIME complexity. Kept leaves.
(4) Obligation:
Set of 50 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: nonterm paths and paths from start to sinks
(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 50 jbc graph edges to a weighted ITS with 50 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.
(6) Obligation:
IntTrs with 50 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_5(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_5(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, i5, env, static) -{1,1}> main_Load_46(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_46(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{0,0}> main_Load_48(i2, i3, i5, env, static) :|: 0 <= static
main_Load_48(i2, i3, i5, env, static) -{0,0}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{0,0}> main_Load_50(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_50(i2, i3, i5, env, static) -{1,1}> main_Load_51(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_51(i2, i3, i5, env, static) -{1,1}> main_LE_55(i2, i3, i5, env, static) :|: 0 >= 0
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_57(i2, i3, i5, env, static) :|: i3 < i2
main_LE_57(i2, i3, i5, env, static) -{1,1}> main_Load_63(i2, i3, i5, env, static) :|: i3 < i2
main_Load_63(i2, i3, i5, env, static) -{1,1}> main_Load_65(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_65(i2, i3, i5, env, static) -{1,1}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_78(i2, i3, i5, env, static) :|: i5 < i2
main_LE_78(i2, i3, i5, env, static) -{1,1}> main_Inc_83(i2, i3, i5, env, static) :|: i5 < i2
main_Inc_83(i2, i3, i5, env, static) -{1,1}> main_Inc_85(i2, i3, i5, i9, env, static) :|: i3 + 1 = i9
main_Inc_85(i2, i3, i5, i9, env, static) -{1,1}> main_JMP_86(i2, i3, i5, i9, i10, env, static) :|: i5 + 1 = i10
main_JMP_86(i2, i3, i5, i9, i10, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i9, i10, env, static) :|: 0 >= 0
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_186(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_186(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_187(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_187(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_199(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_LE_199(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_209(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_Load_209(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_230(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_230(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_255(i2, i3, i5, i44, i41, env, static) :|: i44 < i2
main_LE_255(i2, i3, i5, i44, i41, env, static) -{1,1}> main_Inc_277(i2, i3, i5, i41, i44, env, static) :|: i44 < i2
main_Inc_277(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Inc_286(i2, i3, i5, i79, i44, env, static) :|: i41 + 1 = i79
main_Inc_286(i2, i3, i5, i79, i44, env, static) -{1,1}> main_JMP_291(i2, i3, i5, i79, i84, env, static) :|: i44 + 1 = i84
main_JMP_291(i2, i3, i5, i79, i84, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i79, i84, env, static) :|: 0 >= 0
(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_1(
i2,
i3,
i5,
env,
static) -{17,17}>
main_LE_55(
i2,
i3,
i5,
env,
static'1) :|: 0 >= 0 &&
0 <
2 &&
0 <=
static'1 &&
0 <=
static &&
0 <=
1 &&
0 <
1 &&
static''' <=
static +
2 &&
0 <=
static''' &&
0 <=
2 &&
static'1 <=
static''' +
1by chaining
main_Load_1(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_5(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_5(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i2,
i3,
i5,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_14(
a2,
i2,
i3,
i5,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_14(
a2,
i2,
i3,
i5,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_17(
i2,
i3,
i5,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_17(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_18(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_New_19(
i2,
i3,
i5,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_19(
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_21(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_22(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_22(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i2,
i3,
i5,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Load_26(
o2,
i2,
i3,
i5,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_26(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_28(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_28(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Load_30(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Load_30(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_32(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_32(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Return_35(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Return_38(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Return_38(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_39(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_39(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
i2,
i3,
i5,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_40(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_46(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_46(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_47(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_47(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_48(
i2,
i3,
i5,
env,
static) :|:
0 <=
staticmain_Load_48(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_49(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_49(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_50(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_50(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_51(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_51(
i2,
i3,
i5,
env,
static) -{1,1}>
main_LE_55(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
obtained
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
by chaining
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_57(i2, i3, i5, env, static) :|: i3 < i2
main_LE_57(i2, i3, i5, env, static) -{1,1}> main_Load_63(i2, i3, i5, env, static) :|: i3 < i2
main_Load_63(i2, i3, i5, env, static) -{1,1}> main_Load_65(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_65(i2, i3, i5, env, static) -{1,1}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0
obtained
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i9', i10', env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
by chaining
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_78(i2, i3, i5, env, static) :|: i5 < i2
main_LE_78(i2, i3, i5, env, static) -{1,1}> main_Inc_83(i2, i3, i5, env, static) :|: i5 < i2
main_Inc_83(i2, i3, i5, env, static) -{1,1}> main_Inc_85(i2, i3, i5, i9, env, static) :|: i3 + 1 = i9
main_Inc_85(i2, i3, i5, i9, env, static) -{1,1}> main_JMP_86(i2, i3, i5, i9, i10, env, static) :|: i5 + 1 = i10
main_JMP_86(i2, i3, i5, i9, i10, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i9, i10, env, static) :|: 0 >= 0
obtained
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
by chaining
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_186(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_186(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_187(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_187(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
obtained
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
by chaining
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_199(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_LE_199(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_209(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_Load_209(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_230(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_230(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0
obtained
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
by chaining
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_255(i2, i3, i5, i44, i41, env, static) :|: i44 < i2
main_LE_255(i2, i3, i5, i44, i41, env, static) -{1,1}> main_Inc_277(i2, i3, i5, i41, i44, env, static) :|: i44 < i2
main_Inc_277(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Inc_286(i2, i3, i5, i79, i44, env, static) :|: i41 + 1 = i79
main_Inc_286(i2, i3, i5, i79, i44, env, static) -{1,1}> main_JMP_291(i2, i3, i5, i79, i84, env, static) :|: i44 + 1 = i84
main_JMP_291(i2, i3, i5, i79, i84, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i79, i84, env, static) :|: 0 >= 0
(8) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i9', i10', env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
(9) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i9', i10', env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
was transformed to
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
was transformed to
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
(10) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
(11) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
was transformed to
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
was transformed to
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
was transformed to
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: i3 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
was transformed to
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: i41 < i2
(12) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: i3 < i2
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: i41 < i2
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
(13) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 50 jbc graph edges to a weighted ITS with 50 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.
(14) Obligation:
IntTrs with 50 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_5(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_5(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, i5, env, static) -{1,1}> main_Load_46(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_46(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{0,0}> main_Load_48(i2, i3, i5, env, static) :|: 0 <= static
main_Load_48(i2, i3, i5, env, static) -{0,0}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{0,0}> main_Load_50(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_50(i2, i3, i5, env, static) -{1,1}> main_Load_51(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_51(i2, i3, i5, env, static) -{1,1}> main_LE_55(i2, i3, i5, env, static) :|: 0 >= 0
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_57(i2, i3, i5, env, static) :|: i3 < i2
main_LE_57(i2, i3, i5, env, static) -{1,1}> main_Load_63(i2, i3, i5, env, static) :|: i3 < i2
main_Load_63(i2, i3, i5, env, static) -{1,1}> main_Load_65(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_65(i2, i3, i5, env, static) -{1,1}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_78(i2, i3, i5, env, static) :|: i5 < i2
main_LE_78(i2, i3, i5, env, static) -{1,1}> main_Inc_83(i2, i3, i5, env, static) :|: i5 < i2
main_Inc_83(i2, i3, i5, env, static) -{1,1}> main_Inc_85(i2, i3, i5, i9, env, static) :|: i3 + 1 = i9
main_Inc_85(i2, i3, i5, i9, env, static) -{1,1}> main_JMP_86(i2, i3, i5, i9, i10, env, static) :|: i5 + 1 = i10
main_JMP_86(i2, i3, i5, i9, i10, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i9, i10, env, static) :|: 0 >= 0
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_186(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_186(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_187(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_187(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_199(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_LE_199(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_209(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_Load_209(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_230(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_230(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_255(i2, i3, i5, i44, i41, env, static) :|: i44 < i2
main_LE_255(i2, i3, i5, i44, i41, env, static) -{1,1}> main_Inc_277(i2, i3, i5, i41, i44, env, static) :|: i44 < i2
main_Inc_277(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Inc_286(i2, i3, i5, i79, i44, env, static) :|: i41 + 1 = i79
main_Inc_286(i2, i3, i5, i79, i44, env, static) -{1,1}> main_JMP_291(i2, i3, i5, i79, i84, env, static) :|: i44 + 1 = i84
main_JMP_291(i2, i3, i5, i79, i84, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i79, i84, env, static) :|: 0 >= 0
(15) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_1(
i2,
i3,
i5,
env,
static) -{17,17}>
main_LE_55(
i2,
i3,
i5,
env,
static'1) :|: 0 >= 0 &&
0 <
2 &&
0 <=
static'1 &&
0 <=
static &&
0 <=
1 &&
0 <
1 &&
static''' <=
static +
2 &&
0 <=
static''' &&
0 <=
2 &&
static'1 <=
static''' +
1by chaining
main_Load_1(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_5(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_5(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i2,
i3,
i5,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_14(
a2,
i2,
i3,
i5,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_14(
a2,
i2,
i3,
i5,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_17(
i2,
i3,
i5,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_17(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_18(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_New_19(
i2,
i3,
i5,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_19(
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_21(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_22(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_22(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i2,
i3,
i5,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Load_26(
o2,
i2,
i3,
i5,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_26(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_28(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_28(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Load_30(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Load_30(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_32(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_32(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Return_35(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Return_38(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Return_38(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_39(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_39(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
i2,
i3,
i5,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_40(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_46(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_46(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_47(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_47(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_48(
i2,
i3,
i5,
env,
static) :|:
0 <=
staticmain_Load_48(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_49(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_49(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_50(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_50(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_51(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_51(
i2,
i3,
i5,
env,
static) -{1,1}>
main_LE_55(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
obtained
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
by chaining
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_57(i2, i3, i5, env, static) :|: i3 < i2
main_LE_57(i2, i3, i5, env, static) -{1,1}> main_Load_63(i2, i3, i5, env, static) :|: i3 < i2
main_Load_63(i2, i3, i5, env, static) -{1,1}> main_Load_65(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_65(i2, i3, i5, env, static) -{1,1}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0
obtained
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i9', i10', env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
by chaining
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_78(i2, i3, i5, env, static) :|: i5 < i2
main_LE_78(i2, i3, i5, env, static) -{1,1}> main_Inc_83(i2, i3, i5, env, static) :|: i5 < i2
main_Inc_83(i2, i3, i5, env, static) -{1,1}> main_Inc_85(i2, i3, i5, i9, env, static) :|: i3 + 1 = i9
main_Inc_85(i2, i3, i5, i9, env, static) -{1,1}> main_JMP_86(i2, i3, i5, i9, i10, env, static) :|: i5 + 1 = i10
main_JMP_86(i2, i3, i5, i9, i10, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i9, i10, env, static) :|: 0 >= 0
obtained
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
by chaining
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_186(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_186(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_187(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_187(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
obtained
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
by chaining
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_199(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_LE_199(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_209(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_Load_209(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_230(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_230(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0
obtained
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
by chaining
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_255(i2, i3, i5, i44, i41, env, static) :|: i44 < i2
main_LE_255(i2, i3, i5, i44, i41, env, static) -{1,1}> main_Inc_277(i2, i3, i5, i41, i44, env, static) :|: i44 < i2
main_Inc_277(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Inc_286(i2, i3, i5, i79, i44, env, static) :|: i41 + 1 = i79
main_Inc_286(i2, i3, i5, i79, i44, env, static) -{1,1}> main_JMP_291(i2, i3, i5, i79, i84, env, static) :|: i44 + 1 = i84
main_JMP_291(i2, i3, i5, i79, i84, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i79, i84, env, static) :|: 0 >= 0
(16) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i9', i10', env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
(17) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i9', i10', env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
was transformed to
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
was transformed to
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
(18) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
(19) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: 0 >= 0 && i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
was transformed to
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
was transformed to
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0 && i3 < i2
was transformed to
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: i3 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0 && i41 < i2
was transformed to
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: i41 < i2
(20) Obligation:
IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_254(i2, i3, i5, i44, i41, env, static) :|: i2 <= i44
main_LE_240(i2, i3, i5, i44, i41, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i41 + 1, i44 + 1, env, static) :|: i41 + 1 = i79' && i44 + 1 = i84' && i44 < i2
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_56(i2, i3, i5, env, static) :|: i2 <= i3
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_LE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_77(i2, i3, i5, env, static) :|: i2 <= i5
main_LE_55(i2, i3, i5, env, static) -{3,3}> main_LE_72(i2, i3, i5, env, static) :|: i3 < i2
main_LE_72(i2, i3, i5, env, static) -{3,3}> main_JMP_183(i2, i3, i5, i3 + 1, i5 + 1, env, static) :|: i3 + 1 = i9' && i5 + 1 = i10' && i5 < i2
main_LE_195(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: i41 < i2
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{3,3}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_198(i2, i3, i5, i41, i44, env, static) :|: i2 <= i41
(21) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(7)) transformation)
Extracted set of 46 edges for the analysis of TIME complexity. Dropped leaves.
(22) Obligation:
Set of 46 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: all paths from start
(23) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 46 jbc graph edges to a weighted ITS with 46 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.
(24) Obligation:
IntTrs with 46 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_5(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_5(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, i5, env, static) -{1,1}> main_Load_46(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_46(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{0,0}> main_Load_48(i2, i3, i5, env, static) :|: 0 <= static
main_Load_48(i2, i3, i5, env, static) -{0,0}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{0,0}> main_Load_50(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_50(i2, i3, i5, env, static) -{1,1}> main_Load_51(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_51(i2, i3, i5, env, static) -{1,1}> main_LE_55(i2, i3, i5, env, static) :|: 0 >= 0
main_LE_55(i2, i3, i5, env, static) -{0,0}> main_LE_57(i2, i3, i5, env, static) :|: i3 < i2
main_LE_57(i2, i3, i5, env, static) -{1,1}> main_Load_63(i2, i3, i5, env, static) :|: i3 < i2
main_Load_63(i2, i3, i5, env, static) -{1,1}> main_Load_65(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_65(i2, i3, i5, env, static) -{1,1}> main_LE_72(i2, i3, i5, env, static) :|: 0 >= 0
main_LE_72(i2, i3, i5, env, static) -{0,0}> main_LE_78(i2, i3, i5, env, static) :|: i5 < i2
main_LE_78(i2, i3, i5, env, static) -{1,1}> main_Inc_83(i2, i3, i5, env, static) :|: i5 < i2
main_Inc_83(i2, i3, i5, env, static) -{1,1}> main_Inc_85(i2, i3, i5, i9, env, static) :|: i3 + 1 = i9
main_Inc_85(i2, i3, i5, i9, env, static) -{1,1}> main_JMP_86(i2, i3, i5, i9, i10, env, static) :|: i5 + 1 = i10
main_JMP_86(i2, i3, i5, i9, i10, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i9, i10, env, static) :|: 0 >= 0
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_186(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_186(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_187(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_187(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_199(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_LE_199(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_209(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_Load_209(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_230(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_230(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_255(i2, i3, i5, i44, i41, env, static) :|: i44 < i2
main_LE_255(i2, i3, i5, i44, i41, env, static) -{1,1}> main_Inc_277(i2, i3, i5, i41, i44, env, static) :|: i44 < i2
main_Inc_277(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Inc_286(i2, i3, i5, i79, i44, env, static) :|: i41 + 1 = i79
main_Inc_286(i2, i3, i5, i79, i44, env, static) -{1,1}> main_JMP_291(i2, i3, i5, i79, i84, env, static) :|: i44 + 1 = i84
main_JMP_291(i2, i3, i5, i79, i84, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i79, i84, env, static) :|: 0 >= 0
(25) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_1(
i2,
i3,
i5,
env,
static) -{23,23}>
main_JMP_183(
i2,
i3,
i5,
i9',
i10',
env,
static'1) :|: 0 >= 0 &&
static'1 <=
static''' +
1 &&
i3 +
1 =
i9' &&
0 <=
2 &&
0 <=
static''' &&
static''' <=
static +
2 &&
0 <
1 &&
0 <=
1 &&
0 <=
static &&
0 <=
static'1 &&
i3 <
i2 &&
i5 <
i2 &&
i5 +
1 =
i10' &&
0 <
2by chaining
main_Load_1(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_5(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_5(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i2,
i3,
i5,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_14(
a2,
i2,
i3,
i5,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_14(
a2,
i2,
i3,
i5,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_17(
i2,
i3,
i5,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_17(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_New_18(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_18(
i2,
i3,
i5,
env,
static) -{0,0}>
langle_clinit_rangle_New_19(
i2,
i3,
i5,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_19(
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_21(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_21(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_22(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_22(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i2,
i3,
i5,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_24(
o2,
NULL,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Load_26(
o2,
i2,
i3,
i5,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_26(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_28(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_28(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Load_30(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Load_30(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_32(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_32(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Return_35(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Return_35(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_init_rangle_Return_38(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_init_rangle_Return_38(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_39(
o2,
i2,
i3,
i5,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_39(
o2,
i2,
i3,
i5,
env,
static) -{1,1}>
langle_clinit_rangle_Return_40(
i2,
i3,
i5,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_40(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_46(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_46(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_47(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_47(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_48(
i2,
i3,
i5,
env,
static) :|:
0 <=
staticmain_Load_48(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_49(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_49(
i2,
i3,
i5,
env,
static) -{0,0}>
main_Load_50(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_50(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_51(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_51(
i2,
i3,
i5,
env,
static) -{1,1}>
main_LE_55(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_LE_55(
i2,
i3,
i5,
env,
static) -{0,0}>
main_LE_57(
i2,
i3,
i5,
env,
static) :|:
i3 <
i2main_LE_57(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_63(
i2,
i3,
i5,
env,
static) :|:
i3 <
i2main_Load_63(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Load_65(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_Load_65(
i2,
i3,
i5,
env,
static) -{1,1}>
main_LE_72(
i2,
i3,
i5,
env,
static) :|: 0 >= 0
main_LE_72(
i2,
i3,
i5,
env,
static) -{0,0}>
main_LE_78(
i2,
i3,
i5,
env,
static) :|:
i5 <
i2main_LE_78(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Inc_83(
i2,
i3,
i5,
env,
static) :|:
i5 <
i2main_Inc_83(
i2,
i3,
i5,
env,
static) -{1,1}>
main_Inc_85(
i2,
i3,
i5,
i9,
env,
static) :|:
i3 +
1 =
i9main_Inc_85(
i2,
i3,
i5,
i9,
env,
static) -{1,1}>
main_JMP_86(
i2,
i3,
i5,
i9,
i10,
env,
static) :|:
i5 +
1 =
i10main_JMP_86(
i2,
i3,
i5,
i9,
i10,
env,
static) -{0,0}>
main_JMP_183(
i2,
i3,
i5,
i9,
i10,
env,
static) :|: 0 >= 0
obtained
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{9,9}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
by chaining
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_186(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_186(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_187(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_187(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_195(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_LE_195(i2, i3, i5, i41, i44, env, static) -{0,0}> main_LE_199(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_LE_199(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_209(i2, i3, i5, i41, i44, env, static) :|: i41 < i2
main_Load_209(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Load_230(i2, i3, i5, i41, i44, env, static) :|: 0 >= 0
main_Load_230(i2, i3, i5, i41, i44, env, static) -{1,1}> main_LE_240(i2, i3, i5, i44, i41, env, static) :|: 0 >= 0
main_LE_240(i2, i3, i5, i44, i41, env, static) -{0,0}> main_LE_255(i2, i3, i5, i44, i41, env, static) :|: i44 < i2
main_LE_255(i2, i3, i5, i44, i41, env, static) -{1,1}> main_Inc_277(i2, i3, i5, i41, i44, env, static) :|: i44 < i2
main_Inc_277(i2, i3, i5, i41, i44, env, static) -{1,1}> main_Inc_286(i2, i3, i5, i79, i44, env, static) :|: i41 + 1 = i79
main_Inc_286(i2, i3, i5, i79, i44, env, static) -{1,1}> main_JMP_291(i2, i3, i5, i79, i84, env, static) :|: i44 + 1 = i84
main_JMP_291(i2, i3, i5, i79, i84, env, static) -{0,0}> main_JMP_183(i2, i3, i5, i79, i84, env, static) :|: 0 >= 0
(26) Obligation:
IntTrs with 2 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, env, static) -{23,23}> main_JMP_183(i2, i3, i5, i9', i10', env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10' && 0 < 2
main_JMP_183(i2, i3, i5, i41, i44, env, static) -{9,9}> main_JMP_183(i2, i3, i5, i79', i84', env, static) :|: 0 >= 0 && i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
(27) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)
Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:
main_Load_1(x1, x2, x3, x4, x5) → main_Load_1(x1, x2, x3, x5)
main_JMP_183(x1, x2, x3, x4, x5, x6, x7) → main_JMP_183(x1, x4, x5)
(28) Obligation:
IntTrs with 2 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, static) -{23,23}> main_JMP_183(i2, i9', i10') :|: 0 >= 0 && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10' && 0 < 2
main_JMP_183(i2, i41, i44) -{9,9}> main_JMP_183(i2, i79', i84') :|: 0 >= 0 && i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
(29) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_Load_1(i2, i3, i5, static) -{23,23}> main_JMP_183(i2, i9', i10') :|: 0 >= 0 && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10' && 0 < 2
was transformed to
main_Load_1(i2, i3, i5, static) -{23,23}> main_JMP_183(i2, i3 + 1, i5 + 1) :|: 0 >= 0 && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10' && 0 < 2
main_JMP_183(i2, i41, i44) -{9,9}> main_JMP_183(i2, i79', i84') :|: 0 >= 0 && i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
was transformed to
main_JMP_183(i2, i41, i44) -{9,9}> main_JMP_183(i2, i41 + 1, i44 + 1) :|: 0 >= 0 && i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
(30) Obligation:
IntTrs with 2 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, static) -{23,23}> main_JMP_183(i2, i3 + 1, i5 + 1) :|: 0 >= 0 && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10' && 0 < 2
main_JMP_183(i2, i41, i44) -{9,9}> main_JMP_183(i2, i41 + 1, i44 + 1) :|: 0 >= 0 && i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
(31) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_1(i2, i3, i5, static) -{23,23}> main_JMP_183(i2, i3 + 1, i5 + 1) :|: 0 >= 0 && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10' && 0 < 2
was transformed to
main_Load_1(i2, i3, i5, static) -{23,23}> main_JMP_183(i2, i3 + 1, i5 + 1) :|: static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10'
main_JMP_183(i2, i41, i44) -{9,9}> main_JMP_183(i2, i41 + 1, i44 + 1) :|: 0 >= 0 && i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
was transformed to
main_JMP_183(i2, i41, i44) -{9,9}> main_JMP_183(i2, i41 + 1, i44 + 1) :|: i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
(32) Obligation:
IntTrs with 2 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, static) -{23,23}> main_JMP_183(i2, i3 + 1, i5 + 1) :|: static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i3 < i2 && i5 < i2 && i5 + 1 = i10'
main_JMP_183(i2, i41, i44) -{9,9}> main_JMP_183(i2, i41 + 1, i44 + 1) :|: i41 + 1 = i79' && i44 < i2 && i44 + 1 = i84' && i41 < i2
(33) koat Proof (EQUIVALENT transformation)
YES(?, 9*ar_0 + 9*ar_1 + 23)
Initial complexity problem:
1: T:
(Comp: ?, Cost: 23) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_183(ar_0, ar_1 + 1, ar_2 + 1, arityPad)) [ static'1 <= static''' + 1 /\ ar_1 + 1 = i9' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_2 < ar_0 /\ ar_2 + 1 = i10' ]
(Comp: ?, Cost: 9) main_JMP_183(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_183(ar_0, ar_1 + 1, ar_2 + 1, arityPad)) [ ar_1 + 1 = i79' /\ ar_2 < ar_0 /\ ar_2 + 1 = i84' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_183(ar_0, ar_1 + 1, ar_2 + 1, arityPad)) [ static'1 <= static''' + 1 /\ ar_1 + 1 = i9' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_2 < ar_0 /\ ar_2 + 1 = i10' ]
(Comp: ?, Cost: 9) main_JMP_183(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_183(ar_0, ar_1 + 1, ar_2 + 1, arityPad)) [ ar_1 + 1 = i79' /\ ar_2 < ar_0 /\ ar_2 + 1 = i84' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
A polynomial rank function with
Pol(main_Load_1) = V_1 - V_2
Pol(main_JMP_183) = V_1 - V_2
Pol(koat_start) = V_1 - V_2
orients all transitions weakly and the transition
main_JMP_183(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_183(ar_0, ar_1 + 1, ar_2 + 1, arityPad)) [ ar_1 + 1 = i79' /\ ar_2 < ar_0 /\ ar_2 + 1 = i84' /\ ar_1 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_183(ar_0, ar_1 + 1, ar_2 + 1, arityPad)) [ static'1 <= static''' + 1 /\ ar_1 + 1 = i9' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_2 < ar_0 /\ ar_2 + 1 = i10' ]
(Comp: ar_0 + ar_1, Cost: 9) main_JMP_183(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_183(ar_0, ar_1 + 1, ar_2 + 1, arityPad)) [ ar_1 + 1 = i79' /\ ar_2 < ar_0 /\ ar_2 + 1 = i84' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Complexity upper bound 9*ar_0 + 9*ar_1 + 23
Time: 0.145 sec (SMT: 0.135 sec)
(34) BOUNDS(CONSTANT, 23 + 9 * |#0| + 9 * |#1|)