Working with multiple logical systems

Abstract

The preceding chapters dealt with various issues in the theory and methodology of software specification and development in the context of an arbitrary logical system formalised as an institution. All of this material was presented in the context of an arbitrary but fixed institution. It is also possible to move smoothly between different institutions and to work with a number of institutions simultaneously. This chapter examines some issues related to this idea, introducing methods for building “heterogeneous” specifications that combine descriptions of different parts or different aspects of a system written using different institutions, and methods for proceeding from one institution to another in the course of stepwise refinement. Using multiple institutions requires the institutions in question to be appropriately related to each other, and a number of possible relationships, formulated as different kinds of morphisms, are studied.