Bounded Size-change Termination
No Thumbnail Available
Date
2005-08-03T02:49:06Z
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
The size-change principle devised by Lee, Jones and Ben-Amram, provides an effective method of determining program termination for recursive functions over well-founded types. In this paper, we extend size-change termination beyond the original well-founded condition to include arbitrary bounds that are expressed by linear constraints. Our bounded termination condition determines if repeated calls to a function will monotonically move the call arguments toward the boundary of the guard. We also present a technique which allows the analysis of functions in which there turn values are relevant to termination. Our analysis exploits the decidability and expressive power of affine constraints. These techniques significantly extend the set of programs that are size-change terminating.