Conference Proceedings

Testing for termination with monotonicity constraints

M Codish, V Lagoon, PJ Stuckey, M Gabbrielli (ed.), G Gupta (ed.)

LOGIC PROGRAMMING, PROCEEDINGS | SPRINGER-VERLAG BERLIN | Published : 2005

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 idempoten..

View full abstract