Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/83231

TitleConversão para Why3 de formalizações em Coq
Author(s)Ferreira, Bárbara Andreia Cardoso
Advisor(s)Pinto, Jorge Sousa
Frade, M. J.
KeywordsAlgoritmos de ordenação
Coq
Indução
Lógica
Provas formais
Why3
WhyML
Induction
Logic
Formal proofs
Sorting algorithms
Issue date2021
Abstract(s)O presente documento consiste no relatório da dissertação que descreve todo o trabalho desenvolvido no âmbito do projeto “Conversão para Why3 de Formalizações em Coq”. Este trabalho tem como objetivo principal a conversão das definições de alguns algoritmos funcionais, bem como as suas provas, desenvolvidas em Coq, para Why3. Ou seja, utilizar as duas linguagens do Why3 para perceber até que ponto é possível formalizar algoritmos definidos em Coq. Estas formalizações pertencem ao livro da “Software Foundations” sobre algoritmos funcionais. Este demonstra como uma variedade de algoritmos fundamentais podem ser especificados e verificados mecanicamente. Através da conversão de três algoritmos diferentes foi possível perceber que o Why3 apresenta uma linguagem bastante versátil. Este revela ser possível sem grandes dificuldades a conversão das formalizações Coq para a sua linguagem, principalmente utilizando a sua linguagem de programas, WhyML. A intenção, para além da definição, é também explorar o tipo de provas que as duas linguagens (lógica e de programas) do Why3 permitem realizar. Na linguagem de programas, as provas são extremamente simples, conseguidas, na sua grande maioria, através apenas dos solvers automáticos. Na linguagem lógica do Why3 é possível realizar algumas provas indutivas recorrendo às transformações de prova. No entanto, estas ficam restritas apenas às provas que utilizem a indução estrutural. O mais natural é utilizar a linguagem de programas, pois nesta a prova indutiva é automática e segue a estrutura da definição da função, não sendo necessário a definição de princípios de indução. Comparando as duas linguagens do Why3, a linguagem de programas é efetivamente mais interessante que a linguagem lógica.
The present document is the dissertation report that describes all the work developed in the scope of the project "Conversion of Coq Formalizations to Why3". This work has as main objective the conversion of the definitions of some functional algorithms, as well as their proofs, developed in Coq, to Why3. That is, to use the two languages of Why3 to realize to what extent it is possible to formalize algorithms defined in Coq. These formalizations belong to the "Software Foundations"book on functional algorithms. This demonstrates how a variety of fundamental algorithms can be specified and verified mechanically. Through the conversion of three different algorithms it was possible to see that Why3 is a very versatile language. It shows that it is possible to convert Coq formalizations to its language without too much difficulty, especially using its program language, WhyML. The intention, beyond the definition, is also to explore the kind of proofs that the two languages (logical and program) of Why3 allow one to perform. In the program language, proofs are extremely simple, achieved, for the most part, through just the automatic solvers. In the Why3 logic language it is possible to perform some inductive proofs using proof transformations. However, these are restricted only to proofs that use structural induction. It is more natural to use the program language, because in this language the inductive proof is automatic and follows the structure of the function definition, without the need to define induction principles. Comparing the two Why3 languages, the program language is actually more interesting than the logical language.
TypeMaster thesis
DescriptionDissertação de mestrado integrado em Informatics Engineering
URIhttps://hdl.handle.net/1822/83231
AccessOpen access
Appears in Collections:BUM - Dissertações de Mestrado
DI/CCTC - Dissertações de Mestrado (master thesis)

Files in This Item:
File Description SizeFormat 
Bárbara-Dissertação.PDF845,8 kBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID