Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC 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 (SOUND 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) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE