Monolithic and modular termination analyses for higher-order attribute grammars

Lijesh Krishnan, Eric Van Wyk

Research output: Contribution to journalArticlepeer-review


In this paper we describe a sound, but not complete, analysis to prove the termination of 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. The analysis extracts a set of term-rewriting rules from the grammar that model creation of new syntax trees during the evaluation of higher-order attributes. If this term rewriting system terminates, then only a finite number of trees will be created during attribute grammar evaluation. The analysis places an ordering on nonterminals to handle the cases in which higher-order inherited attributes are used to ensure that a finite number of trees are created using such attributes. When paired with the traditional completeness and circularity analyses for attribute grammars 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 can be applied 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. We also describe a modular version of the analysis that is performed on independently developed language extension grammars and the host language being extended. If the extensions individually pass the modular analysis then their composition is also guaranteed to terminate.

Original languageEnglish (US)
Pages (from-to)511-526
Number of pages16
JournalScience of Computer Programming
Issue numberP4
StatePublished - Dec 15 2014

Bibliographical note

Publisher Copyright:
© 2014 Elsevier B.V.


  • Attribute grammar analysis
  • Higher-order attribute grammars
  • Termination analysis


Dive into the research topics of 'Monolithic and modular termination analyses for higher-order attribute grammars'. Together they form a unique fingerprint.

Cite this