Foundations of program refinement by calculation

Abstract

Embora não seja prática generalizada, aceita-se hoje o valor da especificação formal de aplicações como ingrediente essencial ao desenvolvimento de software fiável. Isso pressupõe uma noção adicional — a de refinamento — capaz de sistematizar a derivação de implementações correctas a partir de modelos abstractos (ie. especificações). No chamado estilo construtivo de desenvolvimento, faz-se refinamento passo-a-passo, provando que cada passo decorre do anterior por regras que garantem a correcção. Estas provas, que são vulgarmente feitas na lógica de predicados e teoria de conjuntos, têm, porém, problemas de escalabilidade: por um lado, não é prático provar factos envolvendo muitas variáveis e quantificações. Por outro, o nível relativamente pouco ágil em que decorrem as provas impede a sua progressão e pede ferramentas automáticas de prova. Esta tese desenvolve uma técnica alternativa de refinamento baseada na chamada transformada-pointfree. A ideia é desenvolver um cálculo ágil capaz de calcular implementações a partir das suas especificações por transformações algébricas simples. A transformada actua sempre que pretendemos raciocinar, mapeando expressões da lógica de predicados em expressões do cálculo relacional com implosão das quantificações e outras construções baseadas em variáveis. Nesse sentido, esta tese aborda os fundamentos do refinamento de programas por cálculo, através de raciocínios ao nível do cálculo de relações binárias dito pointfree, nos seus dois níveis essenciais: dados e algoritmos. Para esse efeito, desenvolvem-se e generalizam-se algumas construções do cálculo relacional, nomeadamente a transposição funcional, uma técnica que tem por objectivo converter relações em funções, de modo a exprimir a álgebra de relações através da álgebra de funções. É utilizada nesta dissertação como leit-motiv. No sentido de potenciar ao máximo a pretendida algebrização do processo de cálculo de programas, a abordagem proposta capitaliza no conceito de conexão de Galois. Em particular, mostra-se como as principais leis de refinamento de dados podem ser vistas como esse tipo de conexão. No plano do refinamento algorítmico, estuda-se a ordem padrão de refinamento ao nível pointfree e calcula-se a sua factorização em duas subordens com comportamentos opostos: redução de não-determinismo e aumento da definição. Essa factorização torna a ordem original mais tratável matematicamente. Apresenta-se a sua teoria em estilo pointfree, que inclui uma prova simples do refinamento estrutural, para tipos paramétricos arbitrários. Finalmente, mostramos que só precisamos de uma regra completa de refinamento relacional—para provar o refinamento coalgébrico—e utilizámo-la para testemunhar o refinamento por cálculo de relações de transição correspondentes a coalgebras.

Design of trustworthy software calls for technologies which discuss software reliability formally, ie. by writing and reasoning about mathematical models of real-life objects and activities (vulg. specifications). Such technologies involve the additional notion of refinement (or reification), which means the systematic process of ensuring correct implementations for formal specifications. In the well-known constructive style for software development, design is factored in several steps, each intermediate step being first proposed and then proved to follow from its antecedent. However, such an ”invent-and-verify” style is often impractical due to the complexity of the mathematical reasoning involved in real-size software problems. Moreover, program reasoning is normally carried out in predicate/ temporal logic and na¨ıve set theory — notations which don’t scale up to fully detailed models of complex problems. This thesis is concerned with the foundations of an alternative technique for program refinement based on so-called pointfree calculation. The idea is to develop a calculus allowing for programs to be actually calculated from their specifications. Instead of doing proofs from first principles, this strategy leads to implementations which are “correct by construction”. Conventional refinement rules are transformed into simple, elegant equations dispensing with points and involving only binary relation combinators. The pointfree binary relational calculus is therefore at the heart of the proposed refinement theory. This thesis adds to such a mathematical framework in two ways: on the one hand it shows how to apply it to data and algorithimc refinement problems. On the other hand, some constructions are proposed which prove useful not only in refinement but also in general. This includes generic functional transposition, a technique for converting relations into functions aimed at developing relational algebra via the algebra of functions. It is employed in this dissertation as a leit motiv. Our proposed theory of data refinement draws heavily on the Galois connection approach to mathematical reasoning. This includes a simple way to calculate refinement invariants induced by the Galois connected laws. Algorithmic refinement is addressed in the same way. The standard operation refinement ordering is given a pointfree treatmentwhich includes a simple calculation of Groves’ factorization and its direct application in structural refinement involving arbitrary parametric types. Finally, coalgebraic refinement is done using an equivalent single complete rule for data refinement which is used to witness refinement by calculation of transition relations corresponding to coalgebras.