(0) Obligation:

JBC Problem based on JBC Program:
public class Sharing {

private Sharing next;

public Sharing(Sharing next) {
this.next = next;
}

public void iter(Sharing other) {
Sharing cursor = this;

while (cursor != null) {
other.next = new Sharing(null);
other = other.next;

cursor = cursor.next;
}
}

public static void main(String[] args) {
Sharing sh1 = new Sharing(new Sharing(new Sharing(null)));
Sharing sh2 = new Sharing(new Sharing(null));
sh2.next.next = sh2;
sh1.iter(sh2);
}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE