School of Computing

Permanent URI for this community

https://dl.comp.nus.edu.sg/handle/1900.100/1

Browse

Browsing School of Computing by Author "Anderson Hugh"

Now showing 1 - 1 of 1
  • No Thumbnail Available
    Item
    Affine-Based Size-Change Termination
    (2003-09-01T00:00:00Z) Anderson Hugh; Siau Cheng KHOO
    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.