Consider the set of operations in a specification for a state-based system. It is a common idea to split the set into “observers,” which determine an equivalence for the objects under consideration, and “operations,” which are compatible with that equivalence. The aim of the authors is to realize such a splitting through a very general formal scheme: basic objects are n-sorted sets structured by two functors, the observational Ob and the operational Op, and two morphisms, Op(X)→X → Ob(X). The coalgebra morphism X → Ob(X) is the fundamental one; in sections 2 and 3 the authors demonstrate how to define observational equivalence, and how to get operational morphism Op(X) → X compatible with it. Section 4 is of a highly technical nature: a description of a fibration of the category of the triples (X,Ob,Op). After a welcome example in section 5, section 6 deals with more concrete situations: for special functors Op(X) → X → Ob(X), one can define a first order language and a notion of satisfaction in which the equality symbol is interpreted by the observational equivalence. Proofs in such a language may be defined by means of infinitary logic. A “soundness and completeness” theorem then shows that proof and satisfaction are correctly correlated.

The authors look at things from a very general and formal point of view. They therefore multiply definitions to get to currently tractable situations, a feature which makes the paper hard to read. I hope that they are able improve this situation in the future.