| Publication type: |
Article in Proceedings |
| Author: |
T. Mossakowski |
| Editor: |
M. Haveraaen, O. Owe, O.-J. Dahl |
| Title: |
Using limits of parchments to systematically construct institutions of partial algebras |
| Book / Collection title: |
Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types |
| Volume: |
1130 |
| Page(s): |
379 – 393 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
1996 |
| Publisher: |
Springer Verlag, London |
| Abstract: |
It has been widely accepted that partial algebras are an important semantical basis for the specification of software systems. The motivation for this work grew out of a systematic study of institutions capturing partiality in different ways. When constructing an institution of partial algebras, one usually redefines every concept for total algebras from scratch, and generalizes it to the partial case. This may become a tedious process. Moreover, often one has to choose between different generalizations, but the design decisions are scattered all over the definitions. In this work, we try to systematize the combination of different institutions. Goguen and Burstall have argued that combinations can be done via (co-)limits. Now the category of institutions and institution morphisms is complete, but limits in this category put together different concepts only without true interaction. Therefore, we move to Goguen's and Burstall's parchments , which allow defining institutions using
# initial algebra semantics for the definition of sentence syntax,
# a special signature for the definition of models and
# a semantical algebra for the definition of semantical evaluation of sentences.
We introduce a notion of morphism between parchments, which allows us to combine different concepts with interaction, using limits. Now there is the problem that, in many cases, the limit contains unwanted ``junk'' truth values and thus the space of truth values need not be preserved. This problem can be solved by imposing a congruence relation on the semantical algebra of the limit. The congruence can usually be generated from a small number of axioms, which state how different concepts interact. Thus, we cannot expect a combination to be done automatically (as in the case of combining theories), but we have to use a two-step semi-automatic method: first specify the components to be combined, and then specify interaction of concepts. These ideas are illustrated by generalizing several concepts from total to partial algebras. The role of the congruence relation here is to decide whether we want a two- or three-valued logic and to determine which concept of equality to use. |
| ISBN: |
3-540-61629-2 |
| Internet: |
http://www.springerlink.com/(bt4qw245oavupgzdxw3zpuul)/app/home/contribution.asp?referrer=parent&backto=searchcitationsresults,3,38; |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~till/papers/parch.ps |
| Status: |
Reviewed |
| Last updated: |
01. 02. 2006 |
|
 |
