Please use this identifier to cite or link to this item:
|Title:||Affine-based size-change termination||Authors:||Anderson, H.
|Issue Date:||2003||Citation:||Anderson, H.,Khoo, S.-C. (2003). Affine-based size-change termination. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2895 : 122-140. ScholarBank@NUS Repository.||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. Termination analysis using the principle involves the classification of functions either into size-change terminating ones, or ones which are not size-change terminating. Size-change graphs are constructed to represent the functions, and decreasing parameter sizes in those graphs that are idempotent are identified. In this paper, we propose a translation of the size-change graphs to affine-based graphs, in which affine relations among parameters are expressed by Presburger formulæ. We show the correctness of our translation by defining the size-change graph composition in terms of affine relation manipulation, and identifying the idempotent size-change graphs with transitive closures in affine relations. We then propose an affine-based termination analysis, in which more refined termination size-change information is admissible by affine relations. Specifically, our affine-related analysis improves the effectiveness of the termination analysis by capturing constant changes in parameter sizes, affine relationships of the sizes of the source parameters, and contextual information pertaining to function calls. We state and reason about the corresponding soundness and termination of this affine-related analysis. Our approach widens the set of size-change terminating functions. © Springer-Verlag Berlin Heidelberg 2003.||Source Title:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)||URI:||http://scholarbank.nus.edu.sg/handle/10635/77813||ISSN:||03029743|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 29, 2019
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.