Conversão para Why3 de formalizações em Coq

Abstract

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.