(0) Obligation:

JBC Problem based on JBC Program:
public class A {
public boolean hasSuperType() {
return false;
}

public A getSuperType() {
return null;
}
}


public class B extends A {
public boolean hasSuperType() {
return true;
}

public A getSuperType() {
return new A();
}
}


public class C extends B {
public A getSuperType() {
return new B();
}
}


public class TypeSwitch {
public static void main(String[] args) {
A x = null;
switch (args.length) {
case 0: x = new A();
break;
case 1: x = new B();
break;
case 2: x = new C();
break;
}

while (x.hasSuperType()) {
x = x.getSuperType();
}
}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE