(0) Obligation:

Need to prove time_complexity of the following program:
package ArrayObjects;

public class ArrayObjects {
	public static void main() {
		Object obj0 = new Object();
		Object obj1 = new Object();
		Object obj2 = new Object();
		Object[] data = {obj0, obj1, obj2};
		while (data[0] != obj0);
		while (data[1] != obj1);
		while (data[2] != obj2);
	}
}


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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ArrayObjects.ArrayObjects.main()V: Graph of 67 nodes with 0 SCCs.


(3) TerminationGraphToComplexityProof (EQUIVALENT transformation)

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

(4) BOUNDS(CONSTANT, 58)

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

Constructed TerminationGraph.

(6) Obligation:

Termination Graph based on JBC Program:
ArrayObjects.ArrayObjects.main()V: Graph of 67 nodes with 0 SCCs.