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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aiken, A.: Introduction to Set Constraint-Based Program Analysis. Science of Computer Programming 35(1999), 79–111 (1999)
Anderson, H., Khoo, S.C.: Affine-Based Size-Change Termination. Technical Report TRA9/03, National University of Singapore (September 2003)
Chin, W.N., Khoo, S.C.: Calculating Sized Types. In: Partial Evaluation and Semantic- Based Program Manipulation, pp. 62–72 (2000)
Colón, M., Sipma, H.: Practical Methods for Proving Program Termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002)
Consel, C.: Polyvariant Binding-Time Analysis For Applicative Languages. In: Partial Evaluation and Semantic-Based Program Manipulation, pp. 66–77 (1993)
Coquand, T., Paulin, C.: Inductively Defined Types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990)
Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Tucson, Arizona, pp. 84–97. ACM Press, NewYork (1978)
Heintze, N.: Set Based Program Analysis. PhD thesis, CMU (1992)
Kelly, P., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega Library Version 1.1.0 Interface Guide. Technical report, University of Maryland, College Park (November 1996)
Khoo, S.C., Shi, K.: Output Constraint Specialization. In: ACM SIGPLAN ASIA Symposium on Partial Evaluation and Semantics-Based Program Manipulation, September 2002, pp. 106–116 (2002)
Lee, C.S.: Program Termination Analysis in Polynomial Time. In: Batory, D., Consel, C., Taha, W. (eds.) GPCE 2002. LNCS, vol. 2487, pp. 218–235. Springer, Heidelberg (2002)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The Size-Change Principle for Program Termination. In: Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol. 28, pp. 81–92. ACM Press, New York (2001)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Shivers, O.: Control Flow Analysis in Scheme. ACM SIGPLAN Notices 7(1), 164–174 (1988)
Speirs, C., Somogyi, Z., Sondergaard, H.: Termination Analysis for Mercury. In: Static Analysis Symposium, pp. 160–171 (1997)
Vanhoof, W., Bruynooghe, M.: Binding-time Analysis for Mercury. In: International Conference on Logic Programming, pp. 500–514 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Anderson, H., Khoo, SC. (2003). Affine-Based Size-Change Termination. In: Ohori, A. (eds) Programming Languages and Systems. APLAS 2003. Lecture Notes in Computer Science, vol 2895. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40018-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-40018-9_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20536-4
Online ISBN: 978-3-540-40018-9
eBook Packages: Springer Book Archive