Translating alloy specification to the point-free style

Abstract

Every program starts from a model, an abstraction, which is iteratively re ned until we reach the nal result, the implementation. However, at the end, one must ask: does the nal program resemble in anyway the original model? Was the original idea correct to begin with? Formal methods guarantee that those questions are answered positively, resorting to mathematical techniques. In particular, in this thesis we are interested on the second factor: veri cation of formal models. A trend of formal methods defends that they should be lightweight, resulting in a reduced complexity of the speci cation, and automated analysis. Alloy was proposed as a solution for this problem. In Alloy, the structures are described using a simple mathematical notation: relational logic. A tool for model checking, automatic veri cation within a given scope, is also provided. However, sometimes model checking is not enough and the need arises to perform unbounded veri cations. The only way to do this is to mathematically prove that the speci cations are correct. As such, there is the need to nd a mathematical logic expressive enough to be able to represent the speci cations, while still being su ciently understandable. We see the point-free style, a style where there are no variables or quanti cations, as a kind of Laplace transform, where complex problems are made simple. Being Alloy completely relational, we believe that a point-free relational logic is the natural framework to reason about Alloy speci cations. Our goal is to present a translation from Alloy speci cations to a point-free relational calculus, which can then be mathematically proven, either resorting to proof assistants or to manual proving. Since our motivation for the use of point-free is simplicity, we will focus on obtaining expressions that are simple enough for manipulation and proofs about them.

Todos os programas partem de um modelo, uma abstração, que é iterativamente refinada até se atingir o resultado final, a implementação. No entanto, no m, não há garantia de a implementação representar o modelo original. Nem sequer sabemos se o modelo inicial estava correcto. Métodos formais garantem que estas questões são respondidas positivamente. Nesta tese em particular estamos interessados no segundo factor: verificação de modelos formais. Uma linha de pensamento nos métodos formais defende que estes devem ser leves, resultando numa diminuição da complexidade das especificações e na automação da sua análise. O Alloy foi proposto como uma solução para este problema. Em Alloy, as estruturas são definidas usando uma notação matemática simples: lógica relacional. Uma ferramenta para verificação de modelos, dentro de um dado limite, é também disponibilizada. No entanto, às vezes essa verificação não é suficiente, e surge a necessidade de efetuar verificações sem limites. A única maneira de fazer isto é provando matematicamente que as especificações estão correctas. Sendo assim, surge a necessidade de encontrar uma lógica matemática que seja suficientemente expressiva para representar as especificações, mais ainda suficientemente compreensível. Vemos o estilo\point-free", um estilo de programação sem variáveis, como uma espécie de transformada de Laplace, onde problemas complexos se tornam mais simples. Visto o Alloy ser completamente relacional, acreditamos que um ambiente \point-free" relacional é o mais natural para lidar com as suas especificações. O nosso objectivo é apresentar uma tradução de especificações Alloy para lógica relacional\point-free", onde podem ser matematicamente provadas, quer recorrendo a assistentes de prova, quer manualmente. Visto a nossa motivação para o uso de \point-free" ser a simplicidade, vamos focar-nos na obtenção de expressões suficientemente simples para que possam ser manipuladas e verificadas.