Institutions: An Abstract Framework for Formal Specifications

Abstract

In this chapter we present some basic concepts and results of the theory of institutions, introduced by Goguen and Burstall to formally capture the informal notion of a logical system viewed from a model-theoretic perspective. We also sketch some possibilities of linking this to more proof-oriented concepts. We argue that the theory of institutions provides an appropriate framework for much of the work on formal software specification and development, as presented in this volume. Many standard logical systems used in particular versions of the algebraic specification paradigm may be viewed as institutions; some examples are given explicitly here, some others are hinted at. Developing (as much as possible) the ideas common to different versions of the algebraic specification paradigm in the framework of an arbitrary institution, and in particular providing a theory of formal specification and software development parameterized by an arbitrary institution rather than having a particular logical system built in, should be beneficial both by helping to avoid repetitious work and by bringing the concepts and results to an appropriate level of mathematical and practical abstraction.