Verifying the Semantics of Disambiguation Rules

Luka Miljak

Context-free grammars (CFGs) provide a well-known formalism for the specification of programming languages. They describe the structure of a program in terms of parse trees. One major issue of CFGs is ambiguity, where one sentence can sometimes have multiple different parse trees. Some formalisms like SDF3 allow annotating a grammar with disambiguation rules, such as priority or associativity rules. Disambiguation rules filter out certain invalid parse trees, making a grammar less ambiguous.

While the semantics of plain CFGs is not something new, formal semantics for these disambiguation rules is still an ongoing research topic. In this thesis we verify an existing semantics for these rules by Amorim et al. for a small subset of expression grammars. We verify the semantics by proving that it is both safe and complete. Safety states adding disambiguation rules will not change the underlying language of the grammar, meaning each sentence in the language will have at least one valid parse tree that does not get filtered out. Completeness guarantees that a grammar is unambiguous, meaning that each sentence in the language will have at most one valid parse tree that does not get filtered out.

---

Previous: | Verifying the Semantics of Disambiguation Rules: Using Parse Tree Repairing for Showing Safety and Completeness of Associativity and Priority Rules
Next: | Software Restructuring