Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 424 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 144 ms)
↳6 intTRS
↳7 PolynomialOrderProcessor (⇒, 11 ms)
↳8 intTRS
↳9 TerminationGraphProcessor (⇔, 0 ms)
↳10 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class Fractale1 {
    public static void fractale(int i, Point p1, Point p2) {
	if (i > 0) {
	    int x3 = (p1.x + p1.y + p2.x - p2.y) / 2;
	    int y3 = (p2.x + p2.y + p1.y - p1.x) / 2;
	    Point p3 = new Point(x3, y3);
	    fractale(i-1, p1, p3);
	    fractale(i-1, p3, p2);
	}
    }

    public static void main(String args[]) {
	fractale(args.length, new Point(0, 0), new Point(200, 200));
    }
}

public class Point {
    
    public int x;
    public int y;

    public Point(int x, int y) {
	this.x = x;
	this.y = y;
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Fractale1.main([Ljava/lang/String;)V: Graph of 63 nodes with 0 SCCs.

Fractale1.fractale(ILPoint;LPoint;)V: Graph of 73 nodes with 0 SCCs.


(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: Fractale1.fractale(ILPoint;LPoint;)V
SCC calls the following helper methods: Fractale1.fractale(ILPoint;LPoint;)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • Point: [x, y]
  • Marker field analysis yielded the following relations that could be markers:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 69 IRules

P rules:
f1048_0_fractale_LE(EOS, i107, i107, i107) → f1050_0_fractale_LE(EOS, i107, i107, i107)
f1050_0_fractale_LE(EOS, i107, i107, i107) → f1055_0_fractale_Load(EOS, i107, i107) | >(i107, 0)
f1055_0_fractale_Load(EOS, i107, i107) → f1058_0_fractale_FieldAccess(EOS, i107, i107)
f1058_0_fractale_FieldAccess(EOS, i107, i107) → f1074_0_fractale_Load(EOS, i107, i107)
f1074_0_fractale_Load(EOS, i107, i107) → f1081_0_fractale_FieldAccess(EOS, i107, i107)
f1081_0_fractale_FieldAccess(EOS, i107, i107) → f1083_0_fractale_IntArithmetic(EOS, i107, i107)
f1083_0_fractale_IntArithmetic(EOS, i107, i107) → f1085_0_fractale_Load(EOS, i107, i107)
f1085_0_fractale_Load(EOS, i107, i107) → f1086_0_fractale_FieldAccess(EOS, i107, i107)
f1086_0_fractale_FieldAccess(EOS, i107, i107) → f1088_0_fractale_IntArithmetic(EOS, i107, i107)
f1088_0_fractale_IntArithmetic(EOS, i107, i107) → f1090_0_fractale_Load(EOS, i107, i107)
f1090_0_fractale_Load(EOS, i107, i107) → f1092_0_fractale_FieldAccess(EOS, i107, i107)
f1092_0_fractale_FieldAccess(EOS, i107, i107) → f1094_0_fractale_IntArithmetic(EOS, i107, i107)
f1094_0_fractale_IntArithmetic(EOS, i107, i107) → f1096_0_fractale_ConstantStackPush(EOS, i107, i107)
f1096_0_fractale_ConstantStackPush(EOS, i107, i107) → f1097_0_fractale_IntArithmetic(EOS, i107, i107)
f1097_0_fractale_IntArithmetic(EOS, i107, i107) → f1099_0_fractale_Store(EOS, i107, i107)
f1099_0_fractale_Store(EOS, i107, i107) → f1101_0_fractale_Load(EOS, i107, i107)
f1101_0_fractale_Load(EOS, i107, i107) → f1103_0_fractale_FieldAccess(EOS, i107, i107)
f1103_0_fractale_FieldAccess(EOS, i107, i107) → f1105_0_fractale_Load(EOS, i107, i107)
f1105_0_fractale_Load(EOS, i107, i107) → f1107_0_fractale_FieldAccess(EOS, i107, i107)
f1107_0_fractale_FieldAccess(EOS, i107, i107) → f1109_0_fractale_IntArithmetic(EOS, i107, i107)
f1109_0_fractale_IntArithmetic(EOS, i107, i107) → f1110_0_fractale_Load(EOS, i107, i107)
f1110_0_fractale_Load(EOS, i107, i107) → f1112_0_fractale_FieldAccess(EOS, i107, i107)
f1112_0_fractale_FieldAccess(EOS, i107, i107) → f1114_0_fractale_IntArithmetic(EOS, i107, i107)
f1114_0_fractale_IntArithmetic(EOS, i107, i107) → f1116_0_fractale_Load(EOS, i107, i107)
f1116_0_fractale_Load(EOS, i107, i107) → f1118_0_fractale_FieldAccess(EOS, i107, i107)
f1118_0_fractale_FieldAccess(EOS, i107, i107) → f1120_0_fractale_IntArithmetic(EOS, i107, i107)
f1120_0_fractale_IntArithmetic(EOS, i107, i107) → f1121_0_fractale_ConstantStackPush(EOS, i107, i107)
f1121_0_fractale_ConstantStackPush(EOS, i107, i107) → f1123_0_fractale_IntArithmetic(EOS, i107, i107)
f1123_0_fractale_IntArithmetic(EOS, i107, i107) → f1125_0_fractale_Store(EOS, i107, i107)
f1125_0_fractale_Store(EOS, i107, i107) → f1127_0_fractale_New(EOS, i107, i107)
f1127_0_fractale_New(EOS, i107, i107) → f1129_0_fractale_Duplicate(EOS, i107, i107)
f1129_0_fractale_Duplicate(EOS, i107, i107) → f1131_0_fractale_Load(EOS, i107, i107)
f1131_0_fractale_Load(EOS, i107, i107) → f1133_0_fractale_Load(EOS, i107, i107)
f1133_0_fractale_Load(EOS, i107, i107) → f1135_0_fractale_InvokeMethod(EOS, i107, i107)
f1135_0_fractale_InvokeMethod(EOS, i107, i107) → f1137_0__init__Load(EOS, i107, i107)
f1137_0__init__Load(EOS, i107, i107) → f1139_0__init__InvokeMethod(EOS, i107, i107)
f1139_0__init__InvokeMethod(EOS, i107, i107) → f1141_0__init__Load(EOS, i107, i107)
f1141_0__init__Load(EOS, i107, i107) → f1143_0__init__Load(EOS, i107, i107)
f1143_0__init__Load(EOS, i107, i107) → f1145_0__init__FieldAccess(EOS, i107, i107)
f1145_0__init__FieldAccess(EOS, i107, i107) → f1148_0__init__Load(EOS, i107, i107)
f1148_0__init__Load(EOS, i107, i107) → f1150_0__init__Load(EOS, i107, i107)
f1150_0__init__Load(EOS, i107, i107) → f1152_0__init__FieldAccess(EOS, i107, i107)
f1152_0__init__FieldAccess(EOS, i107, i107) → f1155_0__init__Return(EOS, i107, i107)
f1155_0__init__Return(EOS, i107, i107) → f1157_0_fractale_Store(EOS, i107, i107)
f1157_0_fractale_Store(EOS, i107, i107) → f1159_0_fractale_Load(EOS, i107, i107)
f1159_0_fractale_Load(EOS, i107, i107) → f1161_0_fractale_ConstantStackPush(EOS, i107, i107, i107)
f1161_0_fractale_ConstantStackPush(EOS, i107, i107, i107) → f1163_0_fractale_IntArithmetic(EOS, i107, i107, i107, 1)
f1163_0_fractale_IntArithmetic(EOS, i107, i107, i107, matching1) → f1165_0_fractale_Load(EOS, i107, i107, -(i107, 1)) | &&(>(i107, 0), =(matching1, 1))
f1165_0_fractale_Load(EOS, i107, i107, i123) → f1167_0_fractale_Load(EOS, i107, i107, i123)
f1167_0_fractale_Load(EOS, i107, i107, i123) → f1169_0_fractale_InvokeMethod(EOS, i107, i107, i123)
f1169_0_fractale_InvokeMethod(EOS, i107, i107, i123) → f1170_0_fractale_Load(EOS, i123, i123)
f1169_0_fractale_InvokeMethod(EOS, i107, i107, i123) → f1170_1_fractale_Load(EOS, i107, i107, i123, i123)
f1170_0_fractale_Load(EOS, i123, i123) → f1173_0_fractale_Load(EOS, i123, i123)
f1173_0_fractale_Load(EOS, i123, i123) → f1045_0_fractale_Load(EOS, i123, i123)
f1045_0_fractale_Load(EOS, i101, i101) → f1048_0_fractale_LE(EOS, i101, i101, i101)
f1198_0_fractale_Return(EOS, i107, i107, matching1) → f1327_0_fractale_Return(EOS, i107, i107, 0) | =(matching1, 0)
f1327_0_fractale_Return(EOS, i107, i107, i208) → f1331_0_fractale_Load(EOS, i107, i107)
f1331_0_fractale_Load(EOS, i107, i107) → f1333_0_fractale_ConstantStackPush(EOS, i107, i107)
f1333_0_fractale_ConstantStackPush(EOS, i107, i107) → f1335_0_fractale_IntArithmetic(EOS, i107, i107, 1)
f1335_0_fractale_IntArithmetic(EOS, i107, i107, matching1) → f1337_0_fractale_Load(EOS, i107, -(i107, 1)) | &&(>(i107, 0), =(matching1, 1))
f1337_0_fractale_Load(EOS, i107, i213) → f1339_0_fractale_Load(EOS, i107, i213)
f1339_0_fractale_Load(EOS, i107, i213) → f1340_0_fractale_InvokeMethod(EOS, i107, i213)
f1340_0_fractale_InvokeMethod(EOS, i107, i213) → f1342_0_fractale_Load(EOS, i213, i213)
f1340_0_fractale_InvokeMethod(EOS, i107, i213) → f1342_1_fractale_Load(EOS, i107, i213, i213)
f1342_0_fractale_Load(EOS, i213, i213) → f1345_0_fractale_Load(EOS, i213, i213)
f1345_0_fractale_Load(EOS, i213, i213) → f1045_0_fractale_Load(EOS, i213, i213)
f1539_0_fractale_Return(EOS, i107, i107, i302) → f1327_0_fractale_Return(EOS, i107, i107, i302)
f1170_1_fractale_Load(EOS, i107, i107, matching1, matching2) → f1198_0_fractale_Return(EOS, i107, i107, 0) | &&(=(matching1, 0), =(matching2, 0))
f1170_1_fractale_Load(EOS, i107, i107, i302, i302) → f1539_0_fractale_Return(EOS, i107, i107, i302)

Combined rules. Obtained 5 IRules

P rules:
f1340_0_fractale_InvokeMethod(EOS, i107, i213) → f1342_1_fractale_Load(EOS, i107, i213, i213)
f1048_0_fractale_LE(EOS, x0, x0, x0) → f1048_0_fractale_LE(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)
f1340_0_fractale_InvokeMethod(EOS, x0, x1) → f1048_0_fractale_LE(EOS, x1, x1, x1)
f1048_0_fractale_LE(EOS, 1, 1, 1) → f1340_0_fractale_InvokeMethod(EOS, 1, 0)
f1048_0_fractale_LE(EOS, x0, x0, x0) → f1340_0_fractale_InvokeMethod(EOS, x0, -(x0, 1)) | >(x0, 0)

Filtered ground terms:


f1340_0_fractale_InvokeMethod(x1, x2, x3) → f1340_0_fractale_InvokeMethod(x2, x3)
f1342_1_fractale_Load(x1, x2, x3, x4) → f1342_1_fractale_Load(x2, x3, x4)
f1048_0_fractale_LE(x1, x2, x3, x4) → f1048_0_fractale_LE(x2, x3, x4)
Cond_f1048_0_fractale_LE(x1, x2, x3, x4, x5) → Cond_f1048_0_fractale_LE(x1, x3, x4, x5)
Cond_f1048_0_fractale_LE1(x1, x2, x3, x4, x5) → Cond_f1048_0_fractale_LE1(x1, x3, x4, x5)

Filtered duplicate terms:


f1342_1_fractale_Load(x1, x2, x3) → f1342_1_fractale_Load(x1, x3)
f1048_0_fractale_LE(x1, x2, x3) → f1048_0_fractale_LE(x3)
Cond_f1048_0_fractale_LE(x1, x2, x3, x4) → Cond_f1048_0_fractale_LE(x1, x4)
Cond_f1048_0_fractale_LE1(x1, x2, x3, x4) → Cond_f1048_0_fractale_LE1(x1, x4)

Filtered unneeded terms:


f1340_0_fractale_InvokeMethod(x1, x2) → f1340_0_fractale_InvokeMethod(x2)

Prepared 5 rules for path length conversion:

P rules:
f1340_0_fractale_InvokeMethod(i213) → f1342_1_fractale_Load(i107, i213)
f1048_0_fractale_LE(x0) → f1048_0_fractale_LE(-(x0, 1)) | >(x0, 0)
f1340_0_fractale_InvokeMethod(x1) → f1048_0_fractale_LE(x1)
f1048_0_fractale_LE(1) → f1340_0_fractale_InvokeMethod(0)
f1048_0_fractale_LE(x0) → f1340_0_fractale_InvokeMethod(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 4 rules.

P rules:
f1048_0_fractale_LE(x2) → f1048_0_fractale_LE(-(x2, 1)) | >(x2, 0)
f1340_0_fractale_InvokeMethod(x3) → f1048_0_fractale_LE(x3)
f1048_0_fractale_LE(c1) → f1340_0_fractale_InvokeMethod(0) | =(1, c1)
f1048_0_fractale_LE(x4) → f1340_0_fractale_InvokeMethod(-(x4, 1)) | >(x4, 0)

(6) Obligation:

Rules:
f1048_0_fractale_LE(x2) → f1048_0_fractale_LE(-(x2, 1)) | >(x2, 0)
f1340_0_fractale_InvokeMethod(x3) → f1048_0_fractale_LE(x3)
f1048_0_fractale_LE(c1) → f1340_0_fractale_InvokeMethod(0) | =(1, c1)
f1048_0_fractale_LE(x4) → f1340_0_fractale_InvokeMethod(-(x4, 1)) | >(x4, 0)

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f1048_0_fractale_LE(x5)] = -1 + x5
[f1340_0_fractale_InvokeMethod(x8)] = -1 + x8

Therefore the following rule(s) have been dropped:


f1048_0_fractale_LE(x0) → f1048_0_fractale_LE(-(x0, 1)) | >(x0, 0)
f1048_0_fractale_LE(x2) → f1340_0_fractale_InvokeMethod(0) | =(1, x2)
f1048_0_fractale_LE(x3) → f1340_0_fractale_InvokeMethod(-(x3, 1)) | >(x3, 0)

(8) Obligation:

Rules:
f1340_0_fractale_InvokeMethod(x1) → f1048_0_fractale_LE(x1) | TRUE

(9) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).


(10) YES