Size-change termination with difference constraints

ABSTRACT

This article considers an algorithmic problem related to the termination analysis of programs. More specifically, we are given bounds on differences in sizes of data values before and after every transition in the program's control-flow graph. Our goal is to infer program termination via the following reasoning (“the size-change principle”): if in any infinite (hypothetic) execution of the program, some size must descend unboundedly, the program must always terminate, since infinite descent of a natural number is impossible.

The problem of inferring termination from such abstract information is not the halting problem for programs and may well be decidable. If this is the case, the decision algorithm forms a “back end” of a termination verifier, and it is interesting to find out the computational complexity of the problem.

A restriction of the problem described above, which only uses monotonicity information (but not difference bounds), is already known to be decidable. We prove that the unrestricted problem is undecidable, which gives a theoretical argument for studying restricted cases. We consider a case where the termination proof is allowed to make use of at most one bound per target variable in each transition. For this special case, which we claim is practically significant, we give (for the first time) an algorithm and show that the problem is in PSPACE, in fact that it is PSPACE-complete. The algorithm is based on combinatorial arguments and results from the theory of integer programming not previously used for similar problems.

The algorithm has interesting connections to other work in termination, in particular to methods for generating linear ranking functions or invariants.

REFERENCES

• 1: Anderson, H. and Khoo, S.-C. 2003. Affine-based size-change termination. In Proceedings of the First Asian Symposium on Programming Languages and Systems (APLAS 2003) (Beijing, China), A. Ohori, Ed. Lecture Notes in Computer Science, vol. 2895. Springer-Verlag, New York, 122--140.
• 2: Krzysztof R. Apt , Dino Pedreschi, Modular termination proofs for logic and pure PROLOG programs, Advances in logic programming theory, Oxford University Press, Inc., New York, NY, 1995
• 3: Avery, J. 2006. Size-change termination and bound analysis. In Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS 2006) M. Hagiya and P. Wadler, Eds. Lecture Notes in Computer Science, vol. 3945. Springer-Verlag, New York.
• 4: Amir M. Ben-Amram , Chin Soon Lee, Program termination analysis in polynomial time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.1, p.5-es, January 2007 [doi>10.1145/1180475.1180480]
• 5: Alexander Brodsky , Yehoshua Sagiv, Inference of inequality constraints in logic programs (extended abstracts), Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.227-240, May 29-31, 1991, Denver, Colorado, United States [doi>10.1145/113413.113434]
• 6: F. Bueno , M. García de la Banda , M. Hermenegildo, Effectiveness of global analysis in strict independence-based automatic parallelization, Proceedings of the 1994 International Symposium on Logic programming, p.320-336, November 1994, Symposia, Melbourne
• 7: Codish, M., Lagoon, V., and Stuckey, P. J. 2005. Testing for termination with monotonicity constraints. In Logic Programming, 21st International Conference, ICLP 2005, M. Gabbrielli and G. Gupta, Eds. Lecture Notes in Computer Science, vol. 3668. Springer-Verlag, New York, 326--340.
• 8: Michael Codish , Cohavit Taboch, A Semantic Basis for Termination Analysis of Logic Programs and Its Realization Using Symbolic Norm Constraints, Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming, p.31-45, September 03-05, 1997
• 9: Michael Colón , Henny Sipma, Practical Methods for Proving Program Termination, Proceedings of the 14th International Conference on Computer Aided Verification, p.442-454, July 27-31, 2002
• 10: Cook, B., Podelski, A., and Rybalchenko, A. 2005. Abstraction refinement for termination. In Proceedings of the 12th International Symposium on Static Analysis (SAS'05) (London, UK, Sept. 7--9) Lecture Notes in Computer Science, vol. 3672. Springer-Verlag, New York, 87--101.
• 11: Cook, B., Podelski, A., and Rybalchenko, A. 2006. Terminator: Beyond safety. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), (Seattle, WA, Aug.), T. Ball and R. B. Jones, Eds. Lecture Notes in Computer Science, vol. 4144. Springer-Verlag, New York, 415--418.
• 12: Dershowitz, N., Lindenstrauss, N., Sagiv, Y., and Serebrenik, A. 2001. A general framework for automatic termination analysis of logic programs. Applic. Algebra Eng. Commun. Comput. 12, 1--2, 117--156.
• 13: Rod G. Downey , Michael R. Fellows, Fixed-Parameter Tractability and Completeness I: Basic Results, SIAM Journal on Computing, v.24 n.4, p.873-921, Aug. 1995 [doi>10.1137/S0097539792228228]
• 14: Graham, R. L. 1981. Rudiments of Ramsey Theory. American Mathematical Society.
• 15: Jones, N. D. 1988. Automatic program specialization: A re-examination from basic principles. In Partial Evaluation and Mixed Computation, D. Bjørner, A. P. Ershov, and N. D. Jones, Eds. North-Holland, Amsterdam, The Netherlands, 225--282.
• 16: Neil D. Jones, Computability and complexity: from a programming perspective, MIT Press, Cambridge, MA, 1997
• 17: Jones, N. D. and Bohr, N. 2004. Termination analysis of the untyped lambda calculus. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA'04). Lecture Notes in Computer Science, vol. 3091. Springer-Verlag, New York, 1--23.
• 18: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 19: Jones, N. D., Landweber, L. H., and Lien, Y. E. 1977. Complexity of some problems in Petri nets. Theoret. Comput. Sci. 4, 3 (June), 277--299.
• 20: Lee, C. S. 2002. Program termination analysis and termination of offline partial evaluation. Ph.D. dissertation, University of Western Australia.
• 21: Lee, C. S. 2008. Ranking functions for size-change termination. Submitted for publication in ACM Trans. Prog. Lang. Syst. (Levven, Belgium).
• 22: Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 2001, London, United Kingdom
• 23: Lindenstrauss, N. and Sagiv, Y. 1997a. Automatic termination analysis of logic programs (with detailed experimental results). http://www.cs.huji.ac.il/~naomil/.
• 24: Lindenstrauss, N. and Sagiv, Y. 1997b. Automatic termination analysis of Prolog programs. In Proceedings of the 14th International Conference on Logic Programming (Leuven, Belgium). L. Naish, Ed. MIT Press, Cambridge, MA, 64--77.
• 25: Manolios, P. and Vroon, D. 2006. Termination analysis with calling context graphs. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006) (Seattle, WA Aug.). Lecture Notes in Computer Science, vol. 4144. Springer-Verlag, New York, 401--414.
• 26: Lee Naish, Automating control for logic programs, Journal of Logic Programming, v.2 n.3, p.167-183, Oct. 1985 [doi>10.1016/0743-1066(85)90017-2]
• 27: Christos H. Papadimitriou, On the complexity of integer programming, Journal of the ACM (JACM), v.28 n.4, p.765-768, Oct. 1981 [doi>10.1145/322276.322287]
• 28: Lutz Plümer, Termination proofs for logic programs, Springer-Verlag New York, Inc., New York, NY, 1990
• 29: Andreas Podelski , Andrey Rybalchenko, Transition Invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.32-41, July 13-17, 2004 [doi>10.1109/LICS.2004.50]
• 30: Ramsey, F. P. 1930. On a problem of formal logic. In Proceedings of the London Mathematical Society. The London Mathematical Society, London, UK, 264--286.
• 31: Sagiv, Y. 1991. A termination test for logic programs. In Proceedings of the International Symposium on Logic Programming (San Diego, CA). V. Saraswat and K. Ueda, Eds. MIT Press, Cambridge, MA, 518--532.
• 32: Schreye, D. D. and Decorte, S. 1994. Termination of logic programs: The never-ending story. J. Logic Prog. 19-20, 199--260.
• 33: Kirack Sohn , Allen Van Gelder, Termination detection in logic programs using argument sizes (extended abstract), Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.216-226, May 29-31, 1991, Denver, Colorado, United States [doi>10.1145/113413.113433]
• 34: René Thiemann , Jürgen Giesl, The size-change principle and dependency pairs for termination of term rewriting, Applicable Algebra in Engineering, Communication and Computing, v.16 n.4, p.229-270, September 2005 [doi>10.1007/s00200-005-0179-7]
• 35: Jeffrey D. Ullman , Allen Van Gelder, Efficient tests for top-down termination of logical rules, Journal of the ACM (JACM), v.35 n.2, p.345-373, April 1988 [doi>10.1145/42282.42285]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

General Terms:
Algorithms, Theory, Verification

Keywords:
Abstraction, program analysis, size-change graph, size-change termination, termination analysis