The Size-change Termination Analyzer

Datalogisk Institut Københavns Universitet

1  Background

The size-change analyzer is a prototype termination analyzer for first-order functional programs, based on Lee, Jones and Ben-Amram's paper at the international conference on Principles of Programming Languages in 2001. It is due to Carl C. Frederiksen. Jones, Lee and Frederiksen are participants of the DAEDALUS project at DIKU.

The size-change termination analysis has been developed as part of a wider effort to implement common "progress" reasoning efficiently. DIKU's participation in DAEDALUS is to study termination analysis as a first step towards the long-term goal of liveness analysis for infinite state systems, applied to the accessibility and responsiveness of concurrent and distributed programs (with dynamic migrating processes).

2  Basis of Analysis

A program satisfies size-change termination (SCT) if every infinite function-call sequence that respects program control flow would give rise to some "bad" dataflow, specifically, an infinite sequence of parameter values whose sizes decrease infinitely.

Algorithmically:

1. For each function in the program, the analyzer generates some "size-change graph," a bipartite graph whose arcs safely describe the parameter size changes observable in that function call.

2. It is decided precisely whether every infinite function-call sequence that respects program control flow has infinite size descent, according to the arcs of the size-change graphs.

   If SCT is satisfied, the program is definitely terminating (for all inputs and all functions), else it is not known whether the program is terminating.

2  Web Version of the Analyzer

The web version of the analyzer takes as input a first-order functional program, derives a set of size-change graphs, and outputs whether SCT is satisfied. Additionally:

• The size-change graphs for the program are displayed graphically.

• If SCT is not satisfied, the analyzer displays a function-call cycle that can be repeated infinitely without causing infinite size descent in any value (according to the size-change graph arcs).

Test suites are available on the analyzer webpage. They show the generality of the size-change reasoning. For example, indirect recursion, lexical descent and functions that permute their arguments are handled automatically.