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