(0) Obligation:
Need to prove time_complexity of the following program:
public class CyclicPair2 {
CyclicPair2 next;
public static void main(int rand) {
CyclicPair2 one = new CyclicPair2();
CyclicPair2 two = new CyclicPair2();
if (rand != 0) {
one.next = two;
two.next = one;
} else {
one.next = two;
}
if (rand == 0) {
one.run();
}
}
public void run() {
CyclicPair2 current = this;
while (current != null)
current = current.next;
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
CyclicPair2.main(I)V: Graph of 78 nodes with 0 SCCs.
(3) TerminationGraphToComplexityProof (EQUIVALENT transformation)
Proven constant complexity by absence of SCCs and edges with non-constant weight
(4) BOUNDS(CONSTANT, 67)