| Abstract / Kurzbeschreibung: |
There is a variety of specification languages for the formal specification and development of correct software systems. They differ in purpose, expressiveness, level of abstraction (requirement, design, implementation), notation, available tools etc. It has been argued that one should not construct one universal all-purpose specification language (which would be very clumsy), but rather relate different languages based on different logical frameworks. Thus there is a need for a meta-notion of logical framework and a notion of map between logical frameworks in order to relate them. This leads to a category of logical frameworks. In the literature, there are described not only one, but many categories of logical frameworks: institutions with maps of institutions, specification frames, institutions with simulations, pre-institutions with transformations, institutional frames, pi- and tau-institutions, institutions with contexts, etc. Some of these were related by Maura Cerioli in her thesis. Thus, there are quite different types of logical frameworks, and each type of logical framework (together with a type of arrow between logical frameworks) leads to a new category of logical frameworks. The purpose of the morphisms in the above mentioned categories of logical frameworks is that of encoding, or representing one logical framework into another one. With this, one can
# write heterogeneous specifications with components written in different logical frameworks,
# switch between different types of logical framework by borrowing missing logical structure along maps, e.g. endow an institution with an entailment relation and a proof calculus,
# compare expressiveness of different logical frameworks (within one type of logical framework, of course),
# use logical framework independent specification language constructs being preserved by maps.
But if we do not follow some neat structuring principle in the meta theory (i. e. types of logical framework), there is the danger to end in the same Babylonian realm of different languages as in the object theories (i. e. different logical frameworks). After all, the meta theory should help us to structure and compare the object theories, and not to produce the same diversity of notions! The main argument for having several types of logical framework is the distinction between proof theory and model theory. Except for the case of specification frames, this was examined by Cerioli and Meseguer. A second argument is the observation that different degrees of more or less good representation of one logical framework in another are possible. Many examples require some intermediate notion between map of institutions and map of specification frames. This has to do with the distinction of signatures and sentences in an institution. This distinction is necessary (using just specification frames abandons the notion of sentence and of theorem proving), but there are many choices for what should be included into the signature part, and what into the sentences. Therefore the need of types of arrow which may mix up this distinction. In this paper we argue that these different types of arrow can be generated by one basic type of arrow and monadic constructions on categories of logical frameworks, with the effect of automatically having functors relating the new categories of logical frameworks with the old ones. |
