Program Generation, Termination, and Binding-Time Analysis | SpringerLink
Skip to main content
Springer Nature Link
Log in

Program Generation, Termination, and Binding-Time Analysis

Invited Paper

  • Conference paper
  • First Online:
Generative Programming and Component Engineering (GPCE 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2487))

  • 570 Accesses

Abstract

Recent research suggests that the goal of fully automatic and reliable program generation for a broad range of applications is coming nearer to feasibility. However, several interesting and challenging problems remain to be solved before it becomes a reality. Solving them is also necessary, if we hope ever to elevate software engineering from its current state (a highly-developed handiwork) into a successful branch of engineering, capable of solving a wide range of new problems by systematic, well-automated and well-founded methods.

We first discuss the relations between problem specifications and their solutions in program form, and then narrow the discussion to an important special case: program transformation. Although the goal of fully automatic program generation is still far from fully achieved, there has been some success in a special case: partial evaluation, also known as program specialization.

A key problem in all program generation is termination of the generation process. This paper describes recent progress towards automatically solving the termination problem, first for individual programs, and then for specializers and “generating extensions,” the program generators that most offline partial evaluators produce.

The paper ends with a list of challenging problems whose solution would bring the community closer to the goal of broad-spectrum, fully automatic and reliable program generation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Andreas Abel and Thorsten Altenkirch. A semantical analysis of structural recursion. In Abstracts of the Fourth International Workshop on Termination WST’99, pages 24–25. unpublished, May 1999.

    Google Scholar 

  2. Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, 1986.

    Google Scholar 

  3. Thomas Arts and Jürgen Giesl. Proving innermost termination automatically. In Proceedings Rewriting Techniques and Applications RTA’97, volume 1232 of Lecture Notes in Computer Science, pages 157–171. Springer, 1997.

    Google Scholar 

  4. Andrew Berlin and Daniel Weise. Compiling scientific code using partial evaluation. IEEE Computer, 23(12):25–37, 1990.

    Google Scholar 

  5. Lars Birkedal and Morten Welinder. Hand-writing program generator generators. In M. Hermenegildo and J. Penjam, editors, Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming (PLILP’ 94), pages 198–214. Springer-Verlag, September 1994.

    Google Scholar 

  6. Anders Bondorf. Automatic autoprojection of higher order recursive equations. Science of Computer Programming, 17:3–34, 1991.

    Article  MATH  Google Scholar 

  7. Anders Bondorf and Jesper Jørgensen. Efficient analyses for realistic off-line partial evaluation: extended version. Technical Report 93/4, DIKU, University of Copenhagen, Denmark, 1993.

    Google Scholar 

  8. Rod M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44–67, January 1977.

    Google Scholar 

  9. Jiazhen Cai, P. Facon, Fritz Henglein, Robert Paige, and Edmond Schonberg. Type analysis and data structure selection. In Constructing Programs From Specifications, pages 325–347. North-Holland, 1991.

    Google Scholar 

  10. Wei-Ngan Chin and Siau-Cheng Khoo. Calculating sized types. Higher-Order and Symbolic Computation, 14(2/3):261–300, 2002.

    Article  Google Scholar 

  11. Wei-Ngan Chin, Siau-Cheng Khoo, and Tat-Wee Lee. Synchronisation analysis to stop tupling. In Programming Languages and Systems (ESOP’98), pages 75–89, Lisbon, 1998. Springer LNCS 1381.

    Chapter  Google Scholar 

  12. Niels H. Christensen, Robert Glück, and Søren Laursen. Binding-time analysis in partial evaluation: One size does not fit all. In D. Bjørner, M. Broy, and A. V. Zamulin, editors, Perspectives of System Informatics. Proceedings, volume 1755 of Lecture Notes in Computer Science, pages 80–92. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  13. Michael A. Colón and Henny B. Sipma. Practical methods for proving program termination. In Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science, pages ??-?? Springer-Verlag, 2002.

    Google Scholar 

  14. Charles Consel. A tour of Schism: a partial evaluation system for higher-order applicative languages. In ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 66–77, 1993.

    Google Scholar 

  15. Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In ACM Symposium on Principles of Programming Languages, pages 493–501. ACM Press, 1993.

    Google Scholar 

  16. Charles Consel and François Noël. A general approach for run-time specialization and its application to C. In ACM Symposium on Principles of Programming Languages, pages 145–156, 1996.

    Google Scholar 

  17. Catarina Coquand. The interactive theorem prover Agda. http://www.cs.chalmers.se/~catarina/agda/, 2001.

  18. James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439–448. IEEE Press, 2000.

    Google Scholar 

  19. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In 4th POPL, Los Angeles, CA, pages 238–252, Jan. 1977.

    Google Scholar 

  20. Olivier Danvy, Robert Glück, and Peter Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1996.

    Google Scholar 

  21. Manuvir Das. Partial Evaluation using Dependence Graphs. PhD thesis, University of Wisconsin-Madison, February 1998.

    Google Scholar 

  22. Manuvir Das and Thomas Reps. BTA termination using CFL-reachability. Technical Report 1329, Computer Science Department, University of Wisconsin-Madison, 1996.

    Google Scholar 

  23. Yoshihiko Futamura. Partial evaluation of computation process-an approach to a compiler-compiler. Higher-Order and Symbolic Computation, 12(4):381–391, 1999. Reprinted from Systems · Computers · Controls 2(5), 1971.

    Article  MATH  Google Scholar 

  24. Yoshihiko Futamura. Partial evaluation of computation process, revisited. Higher-Order and Symbolic Computation, 12(4):377–380, 1999.

    Article  Google Scholar 

  25. John Gallagher and Maurice Bruynooghe. Some low-level source transformations for logic programs. In M. Bruynooghe, editor, Proceedings of the Second Workshop on Meta-Programming in Logic, April 1990, Leuven, Belgium, pages 229–246. Department of Computer Science, KU Leuven, Belgium, 1990.

    Google Scholar 

  26. John P. Gallagher. Tutorial on specialisation of logic programs. In Proceedings of PEPM’93, the ACM Sigplan Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 88–98. ACM Press, 1993.

    Google Scholar 

  27. Steve Ganz, Amr Sabry, and Walid Taha. Macros as Multi-Stage computations: Type-Safe, generative, binding macros in MacroML. In Cindy Norris and Jr. James B. Fenwick, editors, Proceedings of the Sith ACM SIGPLAN International Conference on Functional Programming (ICFP-01), volume 36, 10 of ACM SIGPLAN notices, pages 74–85, New York, September 3–5 2001. ACM Press.

    Google Scholar 

  28. Arne Glenstrup, Henning Makholm, and Jens Peter Secher. C-Mix —specialization of C programs. In Torben Mogensen, and Peter Thiemann, editors. Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summerschool, volume 1706. Springer-Verlag, 1999. Hatcliff et al. [35], pages 108–154.

    Google Scholar 

  29. Arne John Glenstrup. Terminator II: Stopping partial evaluation of fully recursive programs. Master’s thesis, DIKU, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen Ø, June 1999.

    Google Scholar 

  30. Arne John Glenstrup. Partial evaluation, termination analysis, and specialisation-point insertion. In preparation, 2002.

    Google Scholar 

  31. Arne John Glenstrup and Neil D. Jones. BTA algorithms to ensure termination of off-line partial evaluation. In Perspectives of System Informatics: Proceedings of the Andrei Ershov Second International Memorial Conference, Lecture Notes in Computer Science. Springer-Verlag, June 1996.

    Google Scholar 

  32. Robert Glück, Ryo Nakashige, and Robert Zöchling. Binding-time analysis applied to mathematical algorithms. In J. Doležal and J. Fidler, editors, System Modelling and Optimization, pages 137–146. Chapman & Hall, 1995.

    Google Scholar 

  33. Robert Glück and Morten Heine Sørensen. A roadmap to metacomputation by supercompilation. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, pages 137–160. Springer-Verlag, 1996.

    Google Scholar 

  34. Brian Grant, Markus Mock, Matthai Philipose, Craig Chambers, and Susan J. Eggers. DyC: An expressive annotation-directed dynamic compiler for C. Theoretical Computer Science, 248(1–2):147–199, 2000.

    Article  MATH  Google Scholar 

  35. John Hatcliff, Torben Mogensen, and Peter Thiemann, editors. Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summerschool, volume 1706. Springer-Verlag, 1999.

    Google Scholar 

  36. Carsten Kehler Holst and John Launchbury. Handwriting cogen to avoid problems with static typing. In Draft Proceedings, Fourth Annual Glasgow Workshop on Functional Programming, Skye, Scotland, pages 210–218. Glasgow University, 1991.

    Google Scholar 

  37. Paul Hudak. Building domain specific embedded languages. ACM Computing Surveys, 28A:(electronic), December 1996.

    Google Scholar 

  38. John Hughes. Type specialisation for the λ-calculus; or a new paradigm for partial evaluation based on type inference. In Robert Glück, and Peter Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Danvy et al. [20], pages 183–215.

    Google Scholar 

  39. John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Olivier Danvy, Robert Glück, and Peter Thiemann, editors, ACM Symposium on Principles of Programming Languages, pages 410–423. ACM Press, 1996.

    Google Scholar 

  40. Neil D. Jones. What Not to do when writing an interpreter for specialisation. In Robert Glück, and Peter Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Danvy et al. [20], pages 216–237.

    Google Scholar 

  41. Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall. Download accessible from http://www.diku.dk/users/neil, 1993.

  42. Neil D. Jones and Flemming Nielson. Abstract interpretation: a semantics-based tool for program analysis. In Handbook of Logic in Computer Science. Oxford University Press, 1994. 527–629.

    Google Scholar 

  43. Richard B. Kieburtz, Laura McKinney, Jeffrey Bell, James Hook, Alex Kotov, Jeffrey Lewis, Dino Oliva, Tim Sheard, Ira Smith, and Lisa Walton. A software engineering experiment in software component generation. In 18th International Conference in Software Engineering, pages 542–553, 1996.

    Google Scholar 

  44. John Launchbury. Projection Factorisations in Partial Evaluation. Distinguished Dissertations in Computer Science. Cambridge University Press, 1991.

    Google Scholar 

  45. Julia L. Lawall and Peter Thiemann. Sound specialization in the presence of computational effects. In M. Abadi and T. Ito, editors, Proceedings of the 3rd International Symposium on Theoretical Aspects of Computer Software (TACS’97), number 1281 in Lecture Notes in Computer Science, pages 165–190, September 1997.

    Chapter  Google Scholar 

  46. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In ACM Symposium on Principles of Programming Languages, volume 28, pages 81–92. ACM Press, January 2001.

    Google Scholar 

  47. Michael Leuschel. On the power of homeomorphic embedding for online termination. In Static Analysis. Proceedings, volume 1503, pages 230–245. Springer-Verlag, September 1998.

    Google Scholar 

  48. Michael Leuschel and Maurice Bruynooghe. Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming, 2002.

    Google Scholar 

  49. Naomi Lindenstrauss, Yehoshua Sagiv, and Alexander Serebrenik. Termilog: A system for checking termination of queries to logic programs. In Orna Grumberg, editor, Computer Aided Verification, 9th International Conference, CAV’ 97, Haifa, Israel, Jun 22–25, 1997, volume 1254 of Lecture Notes in Computer Science, pages 444–447. Springer, 1997.

    Google Scholar 

  50. Y.Ã. Liu. Efficiency by incrementalization: an introduction. Journal of Higher-Order and Symbolic Computation, 13(4):289–313, 2000.

    Article  MATH  Google Scholar 

  51. John W. Lloyd and John C. Shepherdson. Partial evaluation in logic programming. Journal of Logic Programming, 11:217–242, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  52. Dylan McNamee, Jonathan Walpole, Calton Pu, Crispin Cowan, Charles Krasic, Ashvin Goel, Perry Wagle, Charles Consel, Gilles Muller, and Renaud Marlet. Specialization tools and techniques for systematic optimization of system software. A CM Transactions on Computer Systems, 19(2):217–251, 2001.

    Article  Google Scholar 

  53. Torben Mogensen. Partially static structures in a self-applicable partial evaluator. In D. Bjørner, A.P. Ershov, and N.D. Jones, editors, Partial Evaluation and Mixed Computation, pages 325–347. North-Holland, 1988.

    Google Scholar 

  54. Eugenio Moggi, Walid Taha, Zine-El-Abidine Benaissa, and Tim Sheard. An idealized MetaML: Simpler, and more expressive. In European Symposium on Programming, volume 1576, pages 193–207, 1999.

    Google Scholar 

  55. Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000, USA. Available online from ftp://cse.ogi.edu/pub/tech-reports/README.html.

  56. Rosza Péter. Rekursive Funktionen (Recursive Functions). Académiai Kiadó, Budapest (Academic Press, New York), 1951 (1976).

    Google Scholar 

  57. Massimiliano Poletto, Wilson C. Hsieh, Dawson R. Engler, and M. Frans Kaashoek. ‘C and tcc: A language and compiler for dynamic code generation. ACM Transactions on Programming Languages and Systems, 21(2):324–369, March 1999.

    Google Scholar 

  58. Aravinda Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  59. Konstantinos F. Sagonas, Terrance Swift, and David Scott Warren. XSB as an efficient deductive database engine. In Richard T. Snodgrass and Marianne Winslett, editors, Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data, Minneapolis, Minnesota, May 24–27, 1994, pages 442–453. ACM Press, 1994.

    Google Scholar 

  60. Danny De Schreye, Robert Glück, Jesper Jørgensen, Michael Leuschel, Bern Martens, and Morten H. B. Sørensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(2&3):231–277, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  61. Ulrik Schultz. Partial evaluation for class-based object-oriented languages. In PADO, pages 173–197, 2001.

    Google Scholar 

  62. Peter Sestoft. Bibliography on partial evaluation and mixed computation (bibtex format, online ftp://ftp.diku.dk/diku/semantics/partial-evaluation/). Technical report, DIKU (Computer Science, University of Copenhagen), 2001.

  63. Tim Sheard. Using MetaML: A staged programming language. Lecture Notes in Computer Science, 1608:207--??, 1999.

    Chapter  Google Scholar 

  64. Litong Song and Yoshihiko Futamura. A new termination approach for specialization. In [70], pages 72–91, 2000.

    Chapter  Google Scholar 

  65. Morten Heine Sørensen and Robert Glück. An algorithm of generalization in positive supercompilation. In J.W. Lloyd, editor, Logic Programming: Proceedings of the 1995 International Symposium, pages 465–479. MIT Press, 1995.

    Google Scholar 

  66. Chris Speirs, Zoltan Somogyi, and Harald Søndergaard. Termination analysis for Mercury. In Pascal Van Hentenryck, editor, Static Analysis, Proceedings of the 4th International Symposium, SAS’ 97, Paris, France, Sep 8–19, 1997, volume 1302 of Lecture Notes in Computer Science, pages 160–171. Springer, 1997.

    Google Scholar 

  67. Michael Sperber and Peter Thiemann. Generation of LR parsers by partial evaluation. ACM Transactions on Programming Languages and Systems, 22(2):224–264, March 2000.

    Google Scholar 

  68. Walid Taha. A sound reduction semantics for untyped CBN multi-stage computation. or, the theory of MetaML is non-trival. ACM SIGPLAN Notices, 34(11):34–43, November 1999. Extended abstract.

    Google Scholar 

  69. Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1999. Available from [55].

    Google Scholar 

  70. Walid Taha, editor. Semantics, Applications, and Implementation of Program Generation, volume 1924 of Lecture Notes in Computer Science, Montréal, 2000. Springer-Verlag.

    MATH  Google Scholar 

  71. Walid Taha, Paul Hudak, and Zhanyong Wan. Directions in functional program-ming for real(-time) applications. In the International Workshop on Embedded Software (ES’ 01), volume 221 of Lecture Notes in Computer Science, pages 185–203, Lake Tahoe, 2001. Springer-Verlag.

    Google Scholar 

  72. Walid Taha, Henning Makholm, and John Hughes. Tag elimination and Jones-optimality. In PADO, pages 257–275, 2001. http://cs-www.cs.yale.edu/homes/taha/publications/preprints/pado00.dvi.

  73. Walid Taha and Tim Sheard. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1–2):211–242, October 2000.

    Google Scholar 

  74. Peter Thiemann. A unified framework for binding-time analysis. In M. Bidoit and M. Dauchet, editors, TAPSOFT’ 97: Theory and Practice of Software Development, Lille, France, April 1997. (Lecture Notes in Computer Science, vol. 1214), pages 742–756. Springer-Verlag, 19

    Chapter  Google Scholar 

  75. Peter Thiemann. Aspects of the pgg system: Specialization for standard scheme. In Hatcliff et al. Torben Mogensen, and Peter Thiemann, editors. Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summerschool, volume 1706. Springer-Verlag, 1999. [35], pages 412–432.

    Google Scholar 

  76. Valentin F. Turchin. A supercompiler system based on the language Refal. SIGPLAN Notices, 14(2):46–54, February 1979.

    Google Scholar 

  77. Philip Wadler. Deforestation: Transforming programs to eliminate trees. In H. Ganzinger, editor, ESOP’88. 2nd European Symposium on Programming, Nancy, France, March 1988. (Lecture Notes in Computer Science, vol. 300), pages 344–358. Springer-Verlag, 19

    Google Scholar 

  78. Hongwei Xi. Dependent types for program termination verification. volume 15, pages 91–132, 2002.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DIKU, University of Copenhagen, Denmark

    Neil D. Jones & Arne J. Glenstrup

Authors
  1. Neil D. Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arne J. Glenstrup
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Sciences, University of Texas at Austin, 2.124 Taylor Hall, TX, 78712, Austin, USA

    Don Batory

  2. Department of Telecommunications, ENSEIRB, University of Paris IV, 1, Ave. du Docteur Albert Schweitzer, 33402, Talence, France

    Charles Consel

  3. Department of Computer Science, Rice University, Mail Stop 132, 6100 S. Main Street, 77005-1892, Houston, Texas, USA

    Walid Taha

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jones, N.D., Glenstrup, A.J. (2002). Program Generation, Termination, and Binding-Time Analysis. In: Batory, D., Consel, C., Taha, W. (eds) Generative Programming and Component Engineering. GPCE 2002. Lecture Notes in Computer Science, vol 2487. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45821-2_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-45821-2_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44284-4

  • Online ISBN: 978-3-540-45821-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation