Back to programming from Galois connections

Abstract

It is clear that the trend towards higher levels of abstraction in programming methods, as well as the effort to make software design more of a scientific, engineering discipline, has led to the development of various programming paradigms and the use of rigorous proof methods to ensure the reliability and safety of critical software systems. However, the implementation of these formal methods can be challenging due to their reliance on inductive proofs following the invent-and-verify method. Despite this, some in the field continue to seek out and use these theoretical foundations in an attempt to produce high-quality software. Therefore, this study presents the potential for the correct-by-construction method, using Galois Connections and theoretical concepts from computer science to develop a methodology for constructing practically applicable software systems whose correctness is guaranteed from the outset.

É clara a tendência em direção a níveis mais elevados de abstração nos métodos de programação, bem como o esforço para tornar o design de software mais uma disciplina científica e de engenharia, levando ao desenvolvimento de vários paradigmas de programação e ao uso de métodos rigorosos de prova para garantir a confiabilidade e segurança de sistemas de software críticos. No entanto, a implementação desses métodos formais pode ser desafiadora devido à sua dependência de provas indutivas uma vez seguido o método de “inventar-e-verificar”. Apesar disso, alguns na área continuam a procurar e a utilizar tais fundamentos teóricos numa tentativa de produzir software de alta qualidade. Assim, este estudo apresenta o potencial do método “correção-por-construção”, utilizando conexões de Galois e conceitos teóricos das ciências da computação para desenvolver uma metodologia para construção de sistemas de software praticamente aplicáveis e cuja correção é garantida desde o início.