Resumo: In Computer Science, stepwise refinement of algebraic
specifications is a well known formal methodology for rigorous
program development. This talk illustrates how techniques from Algebraic
Logic, in particular the notion of interpretation,
understood as a multifunction that preserves and reflects logical
consequence, captures a number of relevant transformations
in the context of software design difficult to deal with in classical
approaches. Examples include data
encapsulation and the decomposition of operations into atomic
transactions. But if interpretations open such a new research
avenue in program refinement, (conceptual) tools are needed to reason
about them. Therefore, we will also discuss a correspondence
between logical interpretations and morphisms for a particular kind of
coalgebras, so that usual coalgebraic constructions, such as
bisimulation, can be used to reason about interpretations between
(abstract) logics.
|