(0) Obligation:

JBC Problem based on JBC Program:

class BinarySearchTree{
private LinkedList data;
private BinarySearchTree lc;
private BinarySearchTree rc;
// private int numData;

public BinarySearchTree(){
data = new Null();
lc = null;
rc = null;
}

public BinarySearchTree copy(){
BinarySearchTree aux = new BinarySearchTree();
aux.data=data.copy();
if (lc==null) aux.lc=null;
else aux.lc=lc.copy();
if (rc==null) aux.rc=null;
else aux.rc=rc.copy();
return aux;
}

public static void main(String[] args) {
BinarySearchTree bst = new BinarySearchTree();
bst.lc = new BinarySearchTree();
bst.rc = new BinarySearchTree();
bst.data = new Null(); //Cons();
//((Cons)bst.data).elem = 13;
//((Cons)bst.data).next = new Null();
bst.copy();
}
}


abstract class LinkedList {
abstract LinkedList copy();

}


class Null extends LinkedList {
LinkedList copy() {
return new Null();
}
/*
List add(int e){
Cons aux = new Cons();
aux.elem = e;
aux.next = this;
return aux;
}
*/
/*
String print(){
return "";
}
*/
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE