Skip to main content
SpringerLink
Log in

Termination Analysis for Higher-Order Attribute Grammars

  • Conference paper
Software Language Engineering (SLE 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7745))

Included in the following conference series:

Abstract

This paper describes a conservative analysis to detect non-termination in higher-order attribute grammar evaluation caused by the creation of an unbounded number of (finite) trees as local tree-valued attributes, which are then themselves decorated with attributes. This type of non-termination is not detected by a circularity analysis for higher-order attribute grammars. The analysis presented here uses term rewrite rules to model the creation of new trees on which attributes will be evaluated. If the rewrite rules terminate then only a finite number of trees will be created. To handle higher-order inherited attributes, the analysis places an ordering on non-terminals to schedule their use and ensure a finite number of passes over the generated trees. When paired with the traditional completeness and circularity analyses and the assumption that each attribute equation defines a terminating computation, this analysis can be used to show that attribute grammar evaluation will terminate normally. This analysis is applicable to a wide range of common attribute grammar idioms and has been used to show that evaluation of our specification of Java 1.4 terminates.

This work is partially supported by NSF Awards No. 0905581 and No. 1047961.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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.

References

  1. Backhouse, K.: A Functional Semantics of Attribute Grammars. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 142–157. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Boyland, J.T.: Remote attribute grammars. J. ACM 52(4), 627–687 (2005)

    Article  MathSciNet  Google Scholar 

  3. Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17, 279–301 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  4. Ekman, T., Hedin, G.: The JastAdd system - modular extensible compiler construction. Science of Computer Programming 69, 14–26 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  5. Giesl, J., Thiemann, R., Schneider-kamp, P., Falke, S.: AProVE: A system for proving termination. In: Extended Abstracts of the 6th International Workshop on Termination, WST 2003, pp. 68–70 (2003)

    Google Scholar 

  6. Hedin, G.: Reference attribute grammars. Informatica 24(3), 301–317 (2000)

    MATH  Google Scholar 

  7. Johnsson, T.: Attribute Grammars as a Functional Programming Paradigm. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 154–173. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  8. Knuth, D.E.: Semantics of context-free languages. Mathematical Systems Theory 2(2), 127–145 (1968), corrections in 5, 95–96 (1971)

    Google Scholar 

  9. Krishnan, L.: Composable Semantics Using Higher-Order Attribute Grammars. Ph.D. thesis, University of Minnesota, Department of Computer Science and Engineering, Minneapolis, Minnesota, USA (to appear, 2012), draft available at http://melt.cs.umn.edu/pubs/krishnan2012PhD/

  10. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. of the 28th ACM Symposium on Principles of Programming Languages, POPL 2001, pp. 81–92. ACM Press (2001)

    Google Scholar 

  11. Sereni, D., Jones, N.D.: Termination Analysis of Higher-Order Functional Programs. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 281–297. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Sloane, A.M.: Lightweight Language Processing in Kiama. In: Fernandes, J.M., Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2009. LNCS, vol. 6491, pp. 408–425. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Van Wyk, E., de Moor, O., Backhouse, K., Kwiatkowski, P.: Forwarding in Attribute Grammars for Modular Language Design. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol. 2304, pp. 128–142. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  14. Van Wyk, E., Bodin, D., Gao, J., Krishnan, L.: Silver: an extensible attribute grammar system. Science of Computer Programming 75(1-2), 39–54 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  15. Van Wyk, E., Krishnan, L., Bodin, D., Schwerdfeger, A.: Attribute Grammar-Based Language Extensions for Java. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 575–599. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Vogt, H.: Higher order attribute grammars. Ph.D. thesis, Department of Computer Science, Utrecht University, The Netherlands (1989)

    Google Scholar 

  17. Vogt, H., Swierstra, S.D., Kuiper, M.F.: Higher-order attribute grammars. In: ACM Conf. on Prog. Lang. Design and Implementation, PLDI 1989, pp. 131–145 (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN, USA

    Lijesh Krishnan & Eric Van Wyk

Authors
  1. Lijesh Krishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eric Van Wyk
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical and Computer Engineering, University of Waterloo, 200 University Ave. West, N2L 3G1, Waterloo, ON, Canada

    Krzysztof Czarnecki

  2. Department of Computer Science, Lund University, Box 118, 221 00, Lund, Sweden

    Görel Hedin

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Krishnan, L., Van Wyk, E. (2013). Termination Analysis for Higher-Order Attribute Grammars. In: Czarnecki, K., Hedin, G. (eds) Software Language Engineering. SLE 2012. Lecture Notes in Computer Science, vol 7745. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36089-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-36089-3_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-36088-6

  • Online ISBN: 978-3-642-36089-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation