Publicado no Encontro de Saberes 2017
Evento: II Mostra da Pós-Graduação
Área: CIÊNCIAS EXATAS E DA TERRA
Subárea: Ciência da Computação
Órgão de Fomento: Fundação de Amparo à Pesquisa do Estado de Minas Gerais
Título |
Parsing certificado de expressões regulares baseado em derivadas |
Autores |
RAUL FELIPE PIMENTA LOPES (Autor) Rodrigo Geraldo Ribeiro (Orientador) |
Resumo |
Descrevemos a formalização dos algoritmos baseados na derivada de Brzozowski e na derivada parcial de Antimirov para o parsing baseado em expressões regulares, usando a linguagem dependente de tipos Agda. Essa formalização fornece uma prova de que ou a string de entrada casa com a expressão regular dada ou de que tal casamento não existe. Uma ferramenta para a busca baseada em expressões regulares no estilo da conhecida ferramenta GNU grep foi desenvolvida com os algoritmos certificados. Experimentos práticos conduzidos com essa ferramenta são reportados. Expressões regulares são uma forma algébrica e compacta de especificar linguagens regulares e são muito utilizadas em geradores de analisadores léxicos e utilitários de busca de string. Como tais ferramentas são amplamente usadas e o parsing é pervasivo na computação, existe um interesse crescente em algoritmos de parsing certificados. Esse interesse é motivado pelo desenvolvimento recente de linguagens dependentes de tipos. Tais linguagens são poderosas o suficiente para expressar propriedades algorítmicas como tipos, que são automaticamente checados pelo compilador. O uso de derivadas para expressões regulares foi introduzido por Brzozowski como um método alternativo para computar uma máquina de estados finitos que é equivalente a uma expressão regular. |