(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.