(0) Obligation:
Need to prove time_complexity of the following 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(int i) {
A x = null;
switch (i) {
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 (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
TypeSwitch.main(I)V: Graph of 186 nodes with 0 SCCs.
(3) TerminationGraphToComplexityProof (EQUIVALENT transformation)
Proven constant complexity by absence of SCCs and edges with non-constant weight
(4) BOUNDS(CONSTANT, 166)