The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 657).

(0) Obligation:

Need to prove time_complexity of the following program:

public class Diff {
    // We assume that A and B have no repetitions.
 static void dif(int[] A, int[] B, int[] D){
    int k=0;
    int i=0;
    int l1=A.length;
    int l2=B.length;
    boolean found;
    while(i<l1){
        int j=0;
        found=false;
	while((j<l2)&&(!found)){
	  if(A[i]==B[j]) found=true;
	  else j++;
         }

	if (!found) {
            D[k]=A[i];
	    k++;
	}
      i++;
    }
 }

    public static void main(String[] args) {
	dif(new int[20],new int[20],new int[20]);
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Diff.main([Ljava/lang/String;)V: Graph of 666 nodes with 0 SCCs.

(3) TerminationGraphToComplexityProof (EQUIVALENT transformation)

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

(4) BOUNDS(CONSTANT, 657)

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

Constructed TerminationGraph.

(6) Obligation:

Termination Graph based on JBC Program:
Diff.main([Ljava/lang/String;)V: Graph of 128 nodes with 1 SCC.

(7) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(27)) transformation)

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

(8) Obligation:

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

(9) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(27)) transformation)

Extracted set of 103 edges for the analysis of TIME complexity. Dropped leaves.

(10) Obligation:

Set of 103 edges based on JBC Program.
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start