LL(1) Parser Generator (Q7361330)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry LL1_Parser
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | LL(1) Parser Generator |
AFP entry LL1_Parser |
Statements
2 May 2024
0 references
Sarah Tilscher
0 references
Simon Wimmer
0 references
LL(1) Parser Generator (English)
0 references
In this formalization, we implement an LL(1) parser generator that first pre-computes the NULLABLE set, FIRST map and FOLLOW map, to then build a lookahead table. We prove correctness, soundness and error-free termination for LL(1) grammars. We provide the JSON grammar and show how to parse a tokenized JSON string using a parser created with the verified parser generator. The proof structure is significantly based on Vermillion , an LL(1) parser generator verified in Coq.
0 references
