Semantic equivalence of covering attribute grammars

This paper investigates some methods for proving the equivalence of different language specifications that are given in terms of attribute grammars. Different specifications of the same language may be used for different purposes, such as language definition, program verification, or language implementation. The concept of syntactic coverings is extended to the semantic part of attribute grammars. Given two attribute grammars, the paper discusses several propositions that give sufficient conditions for one attribute grammar to be semantically covered by the other one. These tools are used for a comparison of two attribute grammars that specify syntax and semantics of mixed-type expressions. This example shows a trade-off between the complexity of syntactic and semantic specifications. Another example discussed is the equivalence of different attribute grammars for the translation of the while-statement, as used in compilers for top-down and bottom-up syntax analysis.This work was in part supported by the National Research Council of Canada.