On the design of a Galculator

Abstract

The increasing complexity of software systems together with the lack of tools and techniques to support their development has led to the so-called “software crisis”. Different views about the problem originated diverse approaches to a possible solution, although it is now generally accepted that a “silver bullet” does not exist. The formal methods view considers mathematical reasoning as fundamental to fulfill the most important property of software systems: correctness. However, since correctness proofs are generally difficult and expensive, only critical applications are regarded as potential targets for their use. Developments in tool support such as proof assistants, model checkers and abstract interpreters allow for reducing this cost and making proofs affordable to a wider range of applications. Nevertheless, the effectiveness of a tool is highly dependent of the underlying theory. This dissertation follows a calculational proof style in which equality plays the fundamental role. Instead of the traditional logical approach, fork algebras, an extension of relation algebras, are used. In this setting, Galois connections are important because they reinforce the calculational nature of the algebraic approach, bringing additional structure to the calculus. Moreover, Galois connections enjoy several valuable properties and allow for transformations in the domain of problems. In this dissertation, it is shown how fork algebras and Galois connections can be integrated together with the indirect equality principle. This combination offers a very powerful, generic device to tackle the complexity of proofs in program verification. This power is enhanced with the design of an innovative proof assistant prototype, the Galculator.

O aumento da complexidade dos sistemas de software, juntamente com a falta de ferramentas e técnicas de suporte ao seu desenvolvimento, originaram a chamada “crise do software”. Diferentes visões sobre o problema resultaram em várias abordagens a uma possível solução, embora, actualmente, se considere que não existe uma “solução milagrosa”. A visão dos métodos formais encara o raciocínio matemático como fundamental para satisfazer a propriedade mais importante de um sistema de software: a correcção. Todavia, sendo as provas de correcção, geralmente, difíceis e dispendiosas, apenas as aplicações críticas são encaradas como alvos potenciais para a sua utilização. Desenvolvimentos em ferramentas de suporte, como assistentes de prova, model checkers e interpretadores abstractos, permitem reduzir esse custo, tornando as provas acessíveis a um leque mais alargado de aplicações. Apesar disso, a aplicabilidade destas ferramentas é muito dependente da teoria subjacente. Esta dissertação segue um estilo de prova baseado em cálculo, em que a igualdade assume o papel fundamental. Em vez da tradicional abordagem lógica, são utilizadas fork álgebras, uma extensão das álgebras de relações. Neste contexto, as conexões de Galois são importantes pois reforçam a natureza baseada no cálculo conferida pela abordagem algébrica, assim como a sua estrutura. Para mais, as conexões de Galois gozam de várias propriedades interessantes, além de permitirem transformações no domínio dos problemas. Nesta dissertação mostra-se como as fork álgebras e as conexões de Galois podem ser integradas com o princípio da igualdade indirecta. Esta combinação oferece um dispositivo poderoso e genérico na abordagem às complexas provas da verificarão de programas. Este poder é reforçado com a concepção e implementação de um protótipo de um assistente de prova, o Galculator.