Ranking functions for size-change termination II
Amir M. Ben-Amram, Chin Soon Lee · 2007
Abstract. The Size-Change Termination technique is based on a program abstraction for which termination is decidable. Termination is verified by a set of local termination proofs that account for all cycles in a control-flow graph. We present algorithms that construct a global ranking function for an SCT instance. Such functions serve as easy-to-check witnesses for termination, and are therefore interesting for purposes of program certification. Their particular form and complexity shed light on the theory of SCT termination proofs. Our constructions are simpler and more transparent than previously known. They improve the upper bound on the size of the ranking expression from triply exponential to singly exponential. Another contribution is a set of lowerbound results, proving that our constructions are optimal in a certain sense. An interesting point that arises from our constructions is the usefulness of multisets of data in ranking expression construction. 1 SCT and Ranking Functions in a Nutshell Let Val be a well-ordered set of data values. A control-flow graph (CFG) is a directed