Abstract
Termination analysis is often performed over the abstract domains of monotonicity constraints or of size change graphs. First, the transition relation for a given program is approximated by a set of descriptions. Then, this set is closed under a composition operation. Finally, termination is determined if all of the idempotent loop descriptions in this closure have (possibly different) ranking functions. This approach is complete for size change graphs: An idempotent loop description has a ranking function if and only if it has one which indicates that some specific argument decreases in size. In this paper we generalize the size change criteria for size change graphs which are not idempotent. We also illustrate that proving termination with monotonicity constraints is more powerful than with size change graphs and demonstrate that the size change criteria is incomplete for monotonicity constraints. Finally, we provide a complete termination test for monotonicity constraints.
Original language | English |
---|---|
Title of host publication | Logic Programming |
Subtitle of host publication | 21st International Conference, ICLP 2005 Sitges, Spain, October 2-5, 2005 Proceedings |
Editors | Maurizio Gabbrielli, Gopal Gupta |
Place of Publication | Berlin Germany |
Publisher | Springer |
Pages | 326-340 |
Number of pages | 15 |
ISBN (Print) | 354029208X, 9783540292081 |
DOIs | |
Publication status | Published - 31 Oct 2005 |
Externally published | Yes |
Event | International Conference on Logic Programming 2005 - Sitges, Spain Duration: 2 Oct 2005 → 5 Oct 2005 Conference number: 21st https://link.springer.com/book/10.1007/11562931 (Proceedings) |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 3668 |
ISSN (Print) | 0302-9743 |
Conference
Conference | International Conference on Logic Programming 2005 |
---|---|
Abbreviated title | ICLP 2005 |
Country/Territory | Spain |
City | Sitges |
Period | 2/10/05 → 5/10/05 |
Internet address |
|