(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