Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: example_4/Test

package example_4;

public class Examples {
	
	int f = 10;

	// usual getter and setter methods
	public int getF() {
		return f;
	}

	public void setF(int f) {
		this.f = f;
	}
	
}


package example_4;

/**
 * @costaContext fields/Examples
 *
 */
public class ExamplesCont {

	Examples e;
	
	public ExamplesCont() {
		e = new Examples();
	}
}


package example_4;

/**
 * @costaContext example_4/Examples
 *
 */
public class Test {
	public void exampleMethods(ExamplesCont x, Examples y) {
		int i = 0;

		while (x.e.getF() > 0) {
			i += y.getF();
			x.e.setF(x.e.getF()-1);
		}
	}
	
	public static void main(String[] args) {
		Test o = new Test();
		ExamplesCont x = new ExamplesCont();
		Examples y = new Examples();
		o.exampleMethods(x,y);
	}
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
example_4.Test.main([Ljava/lang/String;)V: Graph of 365 nodes with 0 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

(4) TRUE