(0) Obligation:
Need to prove time_complexity of the following program:
package ArrayObjects;
public class ArrayObjects {
public static void main(String[] argv) {
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([Ljava/lang/String;)V: Graph of 67 nodes with 0 SCCs.
(3) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(4) Obligation:
Termination Graph based on JBC Program:
ArrayObjects.ArrayObjects.main([Ljava/lang/String;)V: Graph of 67 nodes with 0 SCCs.
(5) TerminationGraphToComplexityProof (EQUIVALENT transformation)
Proven constant complexity by absence of SCCs and edges with non-constant weight
(6) BOUNDS(CONSTANT, 58)