(0) Obligation:

JBC Problem based on JBC Program:
public class FactSumList {
static int factorial(int n){
int fact = 1;
for (int i=1; i <= n; i++) fact = fact * i;
return fact;
}

public static int doSum(ListReverse x){
if (x==null) return 0;
else return factorial(x.data) + doSum(x.next);
}

public static void main(String [] args) {
ListReverse l = new ListReverse();
l.next = new ListReverse();
doSum(l);
}
}


class ListReverse {
ListReverse next;
int data;
int length;

public ListReverse listReverse(ListReverse x) {
ListReverse result = null;
ListReverse tmp = null;

while ( x != null ) {
tmp = x.next;
x.next = result;
result = x;
x = tmp;
}

return result;
}

}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE