Monolithic and modular termination analyses for higher-order attribute grammars

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.