(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Diff
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