(0) Obligation:

JBC Problem based on JBC Program:
public class Node1 implements Node {
private Node next;
private int value;

public Node1(int value, Node next) {
this.value = value;
this.next = next;
}

public Node getNext() {
return next;
}

public void setNext(Node next) {
this.next = next;
}

public int getValue() {
return value;
}

public void setValue(int value) {
this.value = value;
}
}

public class Node2 implements Node {
private Node next;
private int value;

public Node2(int value, Node next) {
this.value = value;
this.next = next;
}

public Node getNext() {
return next;
}

public void setNext(Node next) {
this.next = next;
}

public int getValue() {
return value;
}

public void setValue(int value) {
this.value = value;
}
}

public class Node3 implements Node {
private Node next;
private int value;

public Node3(int value, Node next) {
this.value = value;
this.next = next;
}

public Node getNext() {
return next;
}

public void setNext(Node next) {
this.next = next;
}

public int getValue() {
return value;
}

public void setValue(int value) {
this.value = value;
}
}

public interface Node {
public Node getNext();
public void setNext(Node next);
public int getValue();
public void setValue(int value);
}

/**
* Method main() terminates.
*/

public class TestJulia5 {
public static void main(String[] args) {
Node last = new Node1(1,null);
Node n = new Node2(2,last);
int counter = 0;

n = new Node1(3,n);
n = new Node3(4,n);
n = new Node1(5,n);
n = new Node2(6,n);
n = new Node3(7,n);
last.setNext(n);

while (n != null && counter++ < last.getValue()) {
if (n instanceof Node2)
n.setValue(n.getValue() + 1);
n = n.getNext();
}
}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE