Validating LR1 ParsersReportar como inadecuado

Validating LR1 Parsers - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 GALLIUM - Programming languages, types, compilation and proofs Inria Paris-Rocquencourt 2 DI-ENS - Département d-informatique de l-École normale supérieure

Abstract : An LR1 parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser pro-vides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.

Autor: Jacques-Henri Jourdan - François Pottier - Xavier Leroy -



Documentos relacionados