(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: example_3/Test
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