(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) JBC2FIG (SOUND transformation)
Constructed FIGraph.
(2) Obligation:
FIGraph based on JBC Program:
Graph of 148 nodes with 0 SCCs.
(3) FIGtoITRSProof (SOUND transformation)
Transformed FIGraph to ITRS rules
(4) TRUE