Weighted computations: semantics and program logics

Abstract

Esta tese debruça-se sobre computações pesadas ou, por outras palavras, programas e asserções sobre estes cuja execução ou avaliação tem alguma forma de peso associado. Por peso queremos dizer um valor que pode representar, por exemplo, uma incerteza na execução, ou uma quantidade de recursos consumidos, como energia ou tempo. Exemplos de sistemas que contêm alguma componente com pesos variam desde comunicações entre dispositivos, processos biológicos em rede, sistemas de apoio à decisão clínica ou controlo de robots, estando cada vez mais presentes no nosso quotidiano. Neste sentido, devido à alta complexidade subjacente à introdução destes parâmetros, exige-se que a engenharia de software recorra a metodologias de desenvolvimento rigorosas para garantir a alta fiabilidade de cada produto de software. E se é verdade que o desenvolvimento, análise e verificação destes sistemas são cada vez mais assentes nessa mesma abordagem formal, as práticas correntes de programação não são ainda capazes de oferecer uma estrutura que seja, ao mesmo tempo, genérica o suficiente por forma a capturar estes paradigmas e capaz de satisfazer os requisitos específicos para cada domínio de aplicação. Nós queremos atacar este desafio através da apresentação de uma metodologia de desenvolvimento sistemático de semânticas e lógicas para raciocinar sobre duas classes distintas de programas. Na primeira classe, a que nós chamamos de computação de fluxo único, cada execução é uma única transição com um peso associado. Na segunda classe, a que nós chamamos computação de fluxo múltiplo, cada execução pode assumir múltiplos caminhos em simultâneo, cada um com um peso possivelmente distinto. Nesta tese definimos, para cada classe de computação, uma semântica, e provamos que esta forma uma álgebra apropriada para raciocinar sobre programas dessa classe. Para esse fim, definimos operadores que interpretam as construções básicas de uma linguagem de programação imperativa: composição sequencial, condicionais e iteração. A partir daqui construímos uma lógica, incluindo o respetivo sistema axiomático, que permite verificar propriedades sobre estes programas. Uma das virtudes desta metodologia é a sua parametricidade, que é dada por uma estrutura matemática genérica que oferece tanto um modelo de computação para representar programas como um espaço de verdade para avaliar asserções sobre eles. Para a classe de computações de fluxo único, definimos também uma noção de bisimilaridade nos modelos dos lógicas geradas, provando-se invariância modal para essas lógicas.

This thesis deals with weighted computations or, more precisely, programs and assertions about them whose execution or evaluation has some form of weight associated. By weight we mean a value which may represent, for example, an uncertainty in the execution, or a quantity of resources consumed, such as energy or time. Examples of systems containing some component with weights range from device-to-device communications, network biological processes, clinical decision support systems or robot control, being these growingly present in our everyday life. In this sense, due to the complexity underlying the introduction of these parameters, software engineering is forced to call upon rigorous development methodologies which provides a high assurance of each software product. And if it is true that the development, analysis and verification of these systems are increasingly laid on this exactly approach, the current programming practices are not capable to offer a framework which is, at the same time, generic enough to capture such paradigms, and able to satisfy the specific requirements for each application domain. We intend to address this challenge by presenting a methodology for the systematic development of semantics and logics to reason about two distinct classes of programs. In the first class, that we call single-flow computation, each execution is a single transition with an associated weight. In the second class, that we call multi-flow computation, each execution may assume multiple simultaneous execution paths, each one of them with a, possible distinct, weight. In this thesis we define, for each class of computation, a semantics, and we prove that it forms a suitable algebra to reason about programs of that class. For that end, we define operators which interpret the basic constructions of an imperative programming language: sequential composition, conditionals and iteration. From here we construct a logic, including the respective axiomatic system, allowing to verify properties over those programs. One of the merits of this methodology is its parametricity, which is given by a generic mathematical structure offering both a computational model to represent programs and a truth space to evaluate assertions over them. For single-flow computations, we define as well a notion of bisimilarity on the models of the generated logics, and prove the modal invariance property for those logics.