Contents

[Minimize] [Restore] [Maximize]

• Introduction
• Web interface
• Input for analyzer
  • Source language
• Output of analyzer
  • Some terminology
• Other on-line termination analyzers

Introduction

The Size-change Termination Analysis (SCT Analysis for short) is a tool for identifying all potentially non-terminating loops in a given program, as part of the program's verification. It has been jointly developed by Neil D. Jones, Amir Ben-Amram and Chin Soon Lee at TOPPS, DIKU [Jones2001]. This web implementation is due to Carl C. Frederiksen [Fred2001].

Web interface

• The left-hand frame contains links to benchmark programs on which the analyzer has been tested.
  • A program name in black indicates that the program terminates on all inputs.
  • A program name in red indicates that the program does not terminate for some input.
• The top right-hand frame (analyzer frame) contains a text area for entering the subject program, and buttons to run the analysis and reset the text area.

• This frame contains instructions and explanations.

Input for analyzer

Instructions

1. Enter a source program. This may be done by
   • directly entering the program into the text area of the analyzer frame; or
   • selecting a benchmark program in the left-hand frame to insert the code for that program into the text area of the analyzer frame.
2. Click on the button labelled Click here to run analysis below the text area of the analyzer frame to run the analysis.

Source language

1. The source language is a minimal first-order functional language, generated by the following grammar.

   
   

   Prog	::=	Def1...Defn
   Def	::=	fn(x1, ..., xn) = Exprfn
   Expr	::=	x
   	|	con
   	|	con(Expr1, ..., Exprn)
   	|	des(Expr)
   	|	if Expr1 then Expr2 else Expr3
   	|	let x1 = Expr1 ... xn = Exprn in Expr0
   	|	fn(x1, ..., xn)
   	|	op(x1, ..., xn)
   x	:=	identifier beginning with lower case
   fn	:=	identifier beginning with lower case, not in op
   con	:=	capitalized identifier
   des	:=	{1st, 2nd, 3rd, ...}
   op	:=	primitive operator (eq, equal, ...)

   
   

2. Source programs have the obvious semantics. The list ADT can be simulated using: Cons, 1st, and 2nd. The eq operator tests the outermost constructor in a data value: e.g., eq(xs,Cons) returns true just when xs is a pair.

Test suites

The benchmark programs have come mainly from Arne Glenstrup's masters thesis [Glen1999]. They have been adapted from examples found in earlier Prolog and TRS literature.

Output of analyzer

The analyzer may

• declare that the subject program always terminates; or
• report a set of critical multipaths corresponding to potentially non-terminating loops in the program.

In the first case, the subject program definitely terminates on every input. Read on for a sketch of the basis of such deductions, or consult [Jones2001] for details. In the second case, the potentially non-terminating loops reported must be verified to terminate manually.

Instructions

• Click on the link labelled callsites in the analysis output to view the program's size-change graphs.

• Click on a function name to view the size-change graphs corresponding to calls that originate from that function's body.

• Click on a call expression label (also called a callsite) to view the size-change graph corresponding to calls due to that expression.

• For programs that are not declared to terminate, click on any link listed under critical multipath to view the representation of a possibly non-terminating loop in the program.

Some terminology

1. Size-change graph This is a bipartite graph capturing the size relationships among source and target parameters in a function call. It contains decreasing arcs (green in the analyzer output), and non-increasing arcs (black and dashed in the analyzer output).
   1. A decreasing arc asserts that the size of the target parameter after the call is strictly smaller than the size of the source parameter before the call.
   2. A non-increasing arc asserts that the size of the target parameter after the call is no larger than the size of the source parameter before the call.

   For simplicity, the size of a data value is the number of constructors contained in it.

   The first phase of the analysis is to collect a set of size-change graphs such that any potential function call in a program run is represented by some graph in this set.

2. Multipath This is a sequence of size-change graphs representing a call sequence. As such, the target function of each graph in the sequence must match the source function of the next graph.

   A critical multipath corresponds to a loop in the program for which the analyzer is unable to prove termination.

   For programs that are not declared terminating, a set of critical multipaths is listed. They identify the parts of the program that are potentially non-terminating. The call sequences corresponding to these multipaths should be inspected manually as part of the program's verification.

3. Size-change termination condition The basis of the SCT analysis is as follows.
   1. An infinite multipath containing a connected sequence of size-relation arcs, an infinite number of which are decreasing, is impossible to observe in an actual run of the program. This is because the descending parameter values implied by the size-relation arcs would eventually cause a runtime error.

   2. A critical multipath repeated infinitely does not contain infinite descent according to the arcs in its size-change graphs. It represents a potential loop in the program.

   3. The absence of critical multipaths is strong enough to imply that every infinite multipath has infinite descent, and is therefore impossible. The conclusion: the subject program always terminates.

   The condition that ``every infinite multipath has infinite descent'' is referred to as the size-change termination or SCT condition.

   The SCT condition is decidable: the analyzer reports the results of a decision procedure.

Other on-line termination analyzers

The following Prolog termination analyzers are available on the web.

1. Termilog
2. Terminweb

Prolog termination analysis tends to be more involved because typically one traces also groundedness information, as well as size relations among parameters in the same procedure environment.

Bibliography

Fred2001

Carl C. Frederiksen.
A simple implementation of the size-change termination principle.
Technical report, DIKU, Copenhagen University, Denmark, 2001.
TOPPS bibliography reference: D-442.

Glen1999

Arne J. Glenstrup.
Terminator ii: Stopping partial evaluation of fully recursive programs.
Master's thesis, DIKU, Copenhagen University, 1999.

Jones2001

Chin Soon Lee, Neil D. Jones, and Amir Ben-Amram.
The size-change principle for program termination.
In Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, 17-19 January 2001. ACM, 2001.

Wahl2000

David Wahlstedt.
Detecting termination using size-change in parameter values.
Master's thesis, Chalmers University of Technology, 2000.

[Daedalus]

Daedalus project.