Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

package ArrayObjects;

public class ArrayObjects {
	public static void main(String[] argv) {
		Object obj0 = new Object();
		Object obj1 = new Object();
		Object obj2 = new Object();
		Object[] data = {obj0, obj1, obj2};
		while (data[0] != obj0);
		while (data[1] != obj1);
		while (data[2] != obj2);
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ArrayObjects.ArrayObjects.main([Ljava/lang/String;)V: Graph of 67 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE