(0) Obligation:
Need to prove time_complexity of the following program:
/**
* A loop whose termination depends on a <tt>break</tt> statement.
*
* All calls terminate.
*
* Julia + BinTerm prove that all calls terminate
*
* @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
*/
public class Break {
public static void main() {
int i = 0;
while (true) {
if (i > 10) break;
i++;
}
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
Break.main()V: Graph of 86 nodes with 0 SCCs.
(3) TerminationGraphToComplexityProof (EQUIVALENT transformation)
Proven constant complexity by absence of SCCs and edges with non-constant weight
(4) BOUNDS(CONSTANT, 77)