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.
|Original language||English (US)|
|Title of host publication||Software Language Engineering - 5th International Conference, SLE 2012, Revised Selected Papers|
|Number of pages||20|
|State||Published - 2013|
|Event||5th International Conference on Software Language Engineering, SLE 2012 - Dresden, Germany|
Duration: Sep 26 2012 → Sep 28 2012
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Other||5th International Conference on Software Language Engineering, SLE 2012|
|Period||9/26/12 → 9/28/12|
Bibliographical noteFunding Information:
This work is partially supported by NSF Awards No. 0905581 and No. 1047961.