[en] FORMALIZATION OF KEY ALGORITHMS FROM LPEGN

[pt] FORMALIZAÇÃO DE ALGORITMOS-CHAVE DE LPEG

[pt] GUILHERME DANTAS DE OLIVEIRA

[pt] GRAMATICA DE ANALISE SINTATICA DE EXPRESSAO

[pt] LPEG

[pt] BOA FORMACAO

[en] PARSING EXPRESSION GRAMMAR

[en] LPEG

[en] WELL FORMEDNESS

[pt] Gramáticas de Análise Sintática de Expressão (PEGs, do inglês Parsing Expression Languages) são uma classe de gramáticas formais determinísticas originalmente descritas por Ford e amplamente utilizadas para descrever e analisar linguagens de programação. PEGs foram implementadas por diversos projetos. Um desses projetos é LPeg, uma biblioteca Lua que compila PEGs para código otimizado que é executado por uma máquina virtual especializada. A implementação de LPeg apresenta dois algoritmos-chave que nunca foram publicados ou verificados formalmente. Primeiramente, LPeg possui sua própria implementação da verificação de boa-formação introduzida por Ford, essencial para garantir que a análise sintática termine. Em segundo lugar, LPeg implementa um algoritmo que computa o conjunto de primeiros caracteres que podem ser aceitos por um padrão, utilizado para gerar código de máquina virtual mais eficiente para certos padrões. Este trabalho formaliza esses algoritmos e prova que estão corretos usando o provador de teoremas Coq. Além disso, provamos que esses algoritmos terminam utilizando uma abordagem baseada em consumo de gás.

[en] Parsing Expression Grammars (PEGs) are a class of deterministic formal grammars originally described by Ford. They are widely used to describe and parse machine-oriented languages and have been implemented by several projects. One such project is LPeg, a Lua library that compiles PEGs into optimized code that is run by a specialized virtual machine. The implementation of LPeg features two key algorithms that have never been published or verified before. First, LPeg has its own implementation of the well-formedness check introduced by Ford, which is crucial for ensuring that parsing terminates. Second, LPeg implements an algorithm that computes the set of first characters that may be accepted by a pattern, which it uses to optimize the virtual-machine code for certain patterns. This work formalizes these algorithms and proves their correctness using the Coq proof assistant. We also prove their termination using a gas-based approach.

ROBERTO IERUSALIMSCHY

ROBERTO IERUSALIMSCHY

SERGIO QUEIROZ DE MEDEIROS

HUGO MUSSO GUALANDI

2025-06-17

2025-04-24

[pt] TEXTO

application/pdf

INGLÊS

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=71084@1

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=71084@2

https://doi.org/10.17771/PUCRio.acad.71084