Use este identificador para citar ou linkar para este item: http://hdl.handle.net/123456789/3952
Título: Implementação e análise de uma engine para expressões regulares em Coq via testes baseados em propriedades
Título(s) alternativo(s): Implementation and analysis of an expression engine in Coq via property-based testing
Autor(es): BENEVIDES, Marcos Vinicius Moreira Serra
Palavras-chave: COQ
Expressões regulares
Programção funcional
Provadores de teoremas
Quickcheck
Testes baseados em propriedades
COQ
Regular expressions
Functional programming
Proofers of theorems
Quickcheck
Property-based testing
Data do documento: 11-Jul-2019
Editor: Universidade Federal do Maranhão
Resumo: Um provador interativo de teoremas (ou assistentes de provas) é uma ferramenta que auxilia o desenvolvimento de provas formais. Este trabalho fez uma revisão bibliográfica dos fundamentos matemáticos destas ferramentas. Além disso apresentou o assistente de provas COQ e como ele implementa alguns destes conceitos. Alternativamente, apresentou-se os testes baseados em propriedades que é uma solução intermediária entre os testes unitários e as provas formais. Este trabalho utilizou então essa metodologia para analisar um algoritmo de expressões regulares que foi publicado como Functional pearl.
Descrição: ABSTRACT An interactive theorem prover (or proof assistant) is a tool that assists the development of formal evidence. This work has reviewed the literature of the mathematical foundations of these tools. He also presented the assistant of COQ evidence and how it implements some of these concepts. Alternatively, it was presented property-based testing which is an intermediate solution between tests unitary and formal evidence. This paper then used this methodology to analyze a regular expression algorithm that was published as Functional pearl.
URI: http://hdl.handle.net/123456789/3952
Aparece nas coleções:TCCs de Graduação em Ciência da Computação do Campus do Bacanga

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
MARCOS-BENEVIDES.pdfTrabalho de Conclusão de Curso787,79 kBAdobe PDFVisualizar/Abrir


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.