On institutions for modular coalgebraic specifications

We present an algebraic extension of standard coalgebraic specification techniques for state-based systems which allows us to integrate constants and n-ary operations in a smooth way and which leads to institutions enabling the use of modular specification techniques. A sound and complete proof system for first-order observational properties of modular specifications is given. The framework of (Omega, Xi)-structures that we present can be considered as the result of a transformation of concepts of observational logic as in Hennicker and Bidoit (in: A. Haeberer (Ed.), Algebraic Methodology and Software Technology (AMAST'98), Lecture Notes in Computer Science, vol. 1548, Springer, Berlin, 1999) into the coalgebraic world. Moreover, it is shown that the features of (Omega, Xi)-structures that make them suitable models for an observational approach to specifications can be categorically expressed by the fact that the operation mapping an (Omega, Xi)-structure to its behaviour is a fibred idempotent monad. (C) 2002 Elsevier Science B.V. All rights reserved.