Affine-Based Size-Change Termination
| dc.contributor.author | Anderson Hugh | en_US |
| dc.contributor.author | Siau Cheng KHOO | en_US |
| dc.date.accessioned | 2004-10-21T14:28:52Z | en_US |
| dc.date.accessioned | 2017-01-23T06:59:52Z | |
| dc.date.available | 2004-10-21T14:28:52Z | en_US |
| dc.date.available | 2017-01-23T06:59:52Z | |
| dc.date.issued | 2003-09-01T00:00:00Z | en_US |
| dc.description.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 classication 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 identifed. In this paper, we propose a translation of the sizechange graphs to affine-based graphs, in which affine relations among parameters are expressed by Presburger formulae. 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. | en_US |
| dc.format.extent | 428834 bytes | en_US |
| dc.format.mimetype | application/pdf | en_US |
| dc.identifier.uri | https://dl.comp.nus.edu.sg/xmlui/handle/1900.100/1433 | en_US |
| dc.language.iso | en | en_US |
| dc.relation.ispartofseries | TRA9/03 | en_US |
| dc.title | Affine-Based Size-Change Termination | en_US |
| dc.type | Technical Report | en_US |