Verifying the Semantics of Disambiguation Rules

Verifying the Semantics of Disambiguation Rules: Using Parse Tree Repairing for Showing Safety and Completeness of Associativity and Priority Rules

Miljak, Luka (TU Delft Electrical Engineering, Mathematics and Computer Science)

Visser, Eelco (mentor)
Krebbers, Robbert (mentor)
Yorke-Smith, N. (graduation committee)

Delft University of Technology

Computer Science

2021-04-26

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 or YACC allow annotating a grammar with disambiguation rules, such as priority or associativity. Disambiguation rules filter out certain parse trees, making a grammar less ambiguous. Giving a formal semantics for these disambiguation rules is still an ongoing research topic. In this thesis we verify an existing semantics for these rules by Souza Amorim and Visser (2019) for a subset of expression grammars. These grammars may contain infix, prefix, and postfix expressions. 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. We have mechanized the proofs in the Coq Proof Assistant, increasing the confidence in their correctness. As part of the proofs, we also provide a verified implementation for disambiguation rules.

Ambiguity
Declarative Disambiguation Rules
Verification
Semantics
Proof
Proof assistant
Coq

http://resolver.tudelft.nl/uuid:2d831aa4-df6b-4ab6-983e-9776c710b450

https://github.com/metaborg/disamb-verification Repository link Repository containing Coq proofs https://zenodo.org/record/4680987#.YHRVeOgzZjE Archived Coq proofs (please use GitHub link instead for most up to date proofs)

Student theses

master thesis

© 2021 Luka Miljak