Autor(es):
Madeira, Alexandre Leite de Castro 
Data: 2008
Identificador Persistente: http://hdl.handle.net/10773/2907
Origem: RIA - Repositório Institucional da Universidade de Aveiro
Assunto(s): Matemática; Computação matemática; Álgebra universal; Lógica simbólica e matemática; Desenvolvimento de software
Descrição
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). Mestrado em Matemática
