(0) Obligation:
Need to prove time_complexity of the following program:
package ArrayPrimitives;
public class ArrayPrimitives {
public static void main(int int0, int int1, int int2) {
int[] data = {int0, int1, int2};
while (data[0] != int0);
while (data[1] != int1);
while (data[2] != int2);
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
ArrayPrimitives.ArrayPrimitives.main(III)V: Graph of 55 nodes with 0 SCCs.
(3) TerminationGraphToComplexityProof (EQUIVALENT transformation)
Proven constant complexity by absence of SCCs and edges with non-constant weight
(4) BOUNDS(CONSTANT, 46)
(5) TerminationGraphToComplexityProof (EQUIVALENT transformation)
Proven constant complexity by absence of SCCs and edges with non-constant weight
(6) BOUNDS(CONSTANT, 46)
(7) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(8) Obligation:
Termination Graph based on JBC Program:
ArrayPrimitives.ArrayPrimitives.main(III)V: Graph of 55 nodes with 0 SCCs.