(0) Obligation:
JBC Problem based on JBC Program:
package example_3;
public class Test {
int i;
/**
* Same simple arithmetic loop, but the loop counter
* is a numeric field.
*/
public void m(int n) {
while (i < n) {
i++;
}
}
public static void main(String[] args) {
Test o = new Test();
o.m(10);
}
}
(1) JBCToGraph (SOUND transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
example_3.Test.main([Ljava/lang/String;)V: Graph of 150 nodes with 0 SCCs.
(3) TerminationGraphToSCCProof (SOUND transformation)
Proven termination by absence of SCCs
(4) TRUE