(0) Obligation:

Need to prove time_complexity of the following program:
public class A {
	public void method() {
		while (true);
	}
}


public class ArrayClasses {
    public static void main(int i) {
		A[] data = new A[2];
		data[0] = new A();
		data[1] = new B();
		if (i == 1) data[i].method();
	}
}


public class B extends A {
	public void method() {
		return;
	}
}


(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ArrayClasses.main(I)V: Graph of 66 nodes with 0 SCCs.


(3) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(4) Obligation:

Termination Graph based on JBC Program:
ArrayClasses.main(I)V: Graph of 66 nodes with 0 SCCs.


(5) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(11)) transformation)

Extracted set of 54 edges for the analysis of TIME complexity. Kept leaves.

(6) Obligation:

Set of 54 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

(7) TerminationGraphToComplexityProof (EQUIVALENT transformation)

Proven constant complexity by absence of SCCs and edges with non-constant weight

(8) BOUNDS(CONSTANT, 52)