Abordagem algébrica à igualdade observacional

Abstract

A especificação algébrica de sistemas de software é um importante tópico dos denominados métodos formais de desenvolvimento de software. Neste contexto, modelam-se programas por álgebras e as suas computações por termos, recorrendo-se aos resultados da Álgebra Universal e da Lógica, como ferramentas de verificação e apoio ao processo de implementação. Em grande parte dos trabalhos sobre o tema presentes na literatura, usa-se a Lógica Equacional como lógica de suporte a estes processos. Contudo, esta lógica mostra-se limitada para a especificação de programas Orientados a Objectos, nomeadamente na especificação de programas com dados encapsulados. A separação entre os aspectos internos e externos do sistema induz uma nova perspectiva do conceito de modelação, segundo a qual, um objecto se considera como sendo uma realização correcta do sistema, se satisfaz os seus requisitos observacionalmente, isto é, se os resultados das computações sobre si executadas satisfazem esses requisitos, podendo não os satisfazer em sentido estrito. Seguindo esta linha de ideias, dois objectos de software são considerados equivalentes quando se comportam da mesma forma perante todas as possíveis computações. Este paradigma é denominado por Abordagem Observacional de Sistemas. Uma forma de adequar a Lógica Equacional a esta abordagem, é pela substituição da igualdade estrita pela relação de Igualdade Observacional, segundo a qual dois elementos se consideram iguais quando se comportam da mesma forma perante qualquer computação, isto é, se produzem os mesmos outputs perante as mesmas computações. Neste trabalho estuda-se a abordagem observacional de sistemas segundo diferentes grupos de investigação, com especial atenção aos trabalhos da Lógica Escondida (por Goguen-Rosu), Lógica Comportamental e Observacional (por Bidoit-Hennicker) e da Lógica Algébrica (por Pigozzi- Martins). Um ponto central do texto é a generalização do processo de desenvolvimento de software por Refinamento Passo-a-Passo a este paradigma. Aprofundam-se aqui algumas variantes deste tópico, incluindo o caso onde se admitem encapsulamentos e desencapsulamentos de dados durante o processo de refinamento. Numa primeira fase do texto o assunto é apresentado ao nível mais geral das especificações algébricas estruturadas (e não exclusivamente do caso das especificações flat) e das igualdades comportamentais (congruências parciais arbitrárias).

ABSTRACT: The algebraic specification of software systems is an important topic of socalled formal methods of software development. In this context, programmes are modelled by algebras and computations executed over them by terms, using up the results from Universal Algebra and Logic, as verification and support tools for the implementation process. In a large majority of the works about this subject, it uses the Equational Logic as support logic for these processes. However, this logic is too restrictive for the specification of objectoriented programs, namely, in the programs specification with encapsulated data. The split between the internal and external aspects of the system, induces a new perspective of the modelling concept, whereby an object is considered a correct realization of the system if satisfies observationally their requirements, that is, if the results of computations over it executed satisfies these requirements and being able not to satisfy them in the strict sense. Following this principle, two software objects are considered equivalent when behave the same way at all possible computations. This paradigm is called Observational Approach of Systems. One way to adjust the Equational Logic to the observational approach is by replacing the strict equality by the relation of Observational Equality, according to which two elements are considered equal when behave the same way at the same computations, i.e., if they produce the same outputs before the same computations. We follow this approach according to different research groups, with special attention to the work of Behavioural and Observational Logic (by Bidoit- Hennicker), the Hidden Logic (by Goguen-Rosu) and Abstract Algebraic Logic (by Pigozzi-Martins). A central point of the text is the generalization of the software development process by stepwise refinement to this paradigm. Here some variants of this topic are explored including the case where encapsulated and desencapsulated data are allowed during the refinement process. In a first stage of the text, the subject is presented to a more general level of structured specifications (and not exclusively the case of flat specifications) and the Behavioural Equalities (arbitrary partial congruence).