Foundations of algebraic specification and formal software development. (Q610397): Difference between revisions

The authors write in the preface: ``As its title promises, this book provides foundations for software specification and formal software development from the perspective of work on algebraic specification. It concentrates on developing basic concepts and studying their fundamental properties. [\dots] The foundations are built on a solid mathematical basis, using elements of universal algebra, category theory and logic. Once formally defined, these notions become subject to mathematical investigation in their own right.'' To this I may add that the authors of the book under review have the conviction that work on algebraic specification is founded on the fundamental principle that software systems may be modeled as many-sorted algebras (hence, a class of software systems will be determined by a specification, i.e., essentially, by a suitable system of axioms). Moreover, they provide mechanisms for structuring specifications and develop software systems from its specifications through a series of small refinement steps, similar to the stepwise refinement. The book is divided, apart from the introductory chapter, into ten chapters (grouped into four parts: many-sorted universal algebra -- including many-sorted specifications -- and category theory, theory of institutions, formal specification and development, and proof methods); it also has a bibliography, and four indices: of categories and functors, of institutions, of notation, and of concepts. The chapters consist essentially of definitions -- there are also some theorems in the book, but almost all of them state entirely unsurprising results. There are certainly some exceptions to this. Moreover, every chapter is overcrowded with examples, facts, exercises (for the most part not too difficult to solve) with detailed hints, and ends with a section on bibliographical remarks. The first part, Chapters 1--3, deals with many-sorted universal algebra, many-sorted specifications, and category theory, and it contains results which are well known. As the authors themselves say: ``[Chapters 1--3] provide a generally accessible summary rather than an expository introduction.'' As regards many-sorted universal algebra, treated in Chapter 1, I must remind the reader that the founding father of this mathematical theory is \textit{P. J. Higgins} [Math. Nachr. 27, 115--132 (1963; Zbl 0117.25903)]. The constructs treated in many-sorted universal algebra are, for a set of sorts \(S\) and an \(S\)-sorted signature \(\Sigma\), pairs \(((A_{s})_{s\in S},F)\), where \((A_{s})_{s\in S}\) is a family of sets, indexed by \(S\), together with a family of mappings \(F = (F_{w,s})_{(w,s)\in S^{\star}\times S}\), where, for every \((w,s)\in S^{\star}\times S\) and every formal operation \(\sigma\in \Sigma_{w,s}\), \(F_{w,s}(\sigma)\colon\prod_{i\in n} A_{w_{i}}\rightarrow A_{s}\), where \(n\) is \(| w|\), the length of the word \(w\). This generalization of the usual algebraic systems, where all \(A_{s}\) are the same set, is designed to include, among others, graded systems, directed systems, automata, etc. It seems also appropriate to recall that \textit{J. Bénabou} in [Cah. Topol. Geom. Differ. 10, 1--126 (1968; Zbl 0162.32602)], and \textit{G. Matthiessen} [Theorie der heterogenen Algebren. Diss. Universität Bremen. Mathematik-Arbeitspapiere, Nr. 3 (1976)] -- neither of them mentioned in the bibliography of the book under review -- have been instrumental in the development of many-sorted universal algebra. To this I add that, strangely enough, the authors of the book do not exploit the simplicity of the category-theoretic approach to (single-sorted and many-sorted) universal algebra, pioneered, among others, by W. Lawvere, J. Bénabou, F. Linton, P. Freyd, and E. G. Manes. Chapter 1, `Universal algebra', starts, for a set of sorts \(S\), with the notion of an \(S\)-sorted set, the usual operations on them (union, intersection, etc.), and follows with the concepts of \(S\)-sorted mapping between \(S\)-sorted sets, \(S\)-sorted binary relation between \(S\)-sorted sets, kernel of an \(S\)-sorted mapping, and \(S\)-sorted equivalence on an \(S\)-sorted set. I warn the readers about the fact that the authors define the composition of \(S\)-sorted mappings (as well as the composition of \(S\)-sorted binary relations) in diagrammatic order (using the archaic notation of E. Schröder on the relative multiplication). Thus, if \(f\colon A\rightarrow B\) and \(g\colon B\rightarrow C\) are two consecutive \(S\)-sorted mappings, then \(f;g\colon A\rightarrow C\) stands for the composition of \(f\) and \(g\) which, for \(s\in S\) and \(a\in A_{s}\), they define as \((f;g)_{s}(a) = g_{s}(f_{s}(a))\). After this, the authors introduce the elements of many-sorted algebra. Concretely, they define the concepts of many-sorted signature, many-sorted algebra, subalgebra, reachable algebra, product algebra, homomorphism, isomorphism, congruence (without saying that for its definition it suffices to require the compatibility with the operations which are not \(0\)-ary), quotient algebra, and culminate with the proof that, for a set of sorts \(S\), an \(S\)-sorted signature \(\Sigma\), and an \(S\)-sorted set \(X\), there exists \(\mathbf{T}_{\Sigma}(X)\), the free many-sorted algebra on \(X\), which has the usual universal property. I think that the following construction of \(\mathbf{T}_{\Sigma}(X)\) is more transparent than that provided by the authors of the book. For a set of sorts \(S\), an \(S\)-sorted signature \(\Sigma\), and an \(S\)-sorted set (of variables) \(X\), define in the first place a \(\Sigma\)-algebra \(\mathbf{W}_{\Sigma}(X)\), the \(\Sigma\)-\textit{algebra of} \(\Sigma\)-\textit{rows} in \(X\), as follows: \(\mathrm{W}_{\Sigma}(X) = ({\mathrm{W}_{\Sigma}(X)}_{s})_{s\in S}\), the underlying \(S\)-sorted set of \(\mathbf{W}_{\Sigma}(X)\), is \(((\coprod\Sigma \amalg \coprod X)^{\star})_{s\in S}\), i.e., for every \(s\) in \(S\), \({\mathrm{W}_{\Sigma}(X)}_{s}=(\coprod\Sigma\amalg\coprod X)^{\star}\), where \((\coprod\Sigma \amalg\coprod X)^{\star}\) is the underlying set of the free monoid on \(\coprod\Sigma \amalg \coprod X\). On the \(S\)-sorted set \(\mathrm{W}_{\Sigma}(X)\) define a \(\Sigma\)-algebra structure by concatenation; thus, for every \((w,s)\in S^{\star}\times S\) and every \(\sigma\in\Sigma_{w,s}\), \(F_{\sigma}\), the structural operation associated to \(\sigma\), is the mapping from \(\mathrm{W}_{\Sigma}(X)_{w}\) to \({\mathrm{W}_{\Sigma}(X)}_{s}\), i.e., from \(((\coprod\Sigma\amalg\coprod X)^{\star})^{| w |}\) to \((\coprod\Sigma\amalg \coprod X)^{\star}\), which sends \((P_{i})_{i\in| w |}\) in \(((\coprod\Sigma\amalg\coprod X)^{\star})^{| w |}\) to \((\sigma)\curlywedge P_{0} \curlywedge\dots \curlywedge P_{| w |-1}\) in \((\coprod\Sigma\amalg \coprod X)^{\star}\), i.e., to the concatenation of \((\sigma)\) and of the words \(P_{i}\) in the family \((P_{i})_{i\in| w |}\), where \((\sigma)\) is the image of \(\sigma\) under the canonical embeddings from \(\Sigma_{w,s}\) to \((\coprod\Sigma\amalg\coprod X)^{\star}\). Then \(\mathbf{T}_{\Sigma}(X)\), the free \(\Sigma\)-algebra on \(X\), is the subalgebra de \(\mathbf{W}_{\Sigma}(X)\) generated by the \(S\)-sorted set \((\{(x)\mid x\in X_{s}\})_{s\in S}\), where, for every \(s\in S\) and every \(x\in X_{s}\), \((x)\) is the image of \(x\) under the canonical embeddings from \(X_{s}\) to \((\coprod\Sigma\amalg\coprod X)^{\star}\). The rest of the chapter is devoted to define signature morphisms, composition of signature morphisms, reduct algebras, reduct homomorphisms, term translation, and the notion of derivor, defined by \textit{J. A. Goguen}, \textit{J. Thatcher} and \textit{E. Wagner} in [``An initial algebra approach to the specification, correctness, and implementation of abstract data types'', in: R. T. Yeh (ed.), Current trends in programming methodology. Vol. IV: Data structuring. Englewood Cliffs, New Jersey: Prentice-Hall, Inc. (1978)], which is a slight generalization of the concept of signature morphism. In the final section of this chapter (p. 39) the authors say that ``since the 1970s, derived signature morphisms have made only sporadic appearances in the algebraic specification literature [\dots]''. In this respect I refer the reader to the article [Rep. Math. Logic 45, 37--95 (2010; Zbl 1243.03079)], written by the reviewer and \textit{J. Soliveres Tur}. (There, among others, the theory of \textit{T. Fujiwara} on morphisms [Osaka Math. J. 11, 153--172 (1959; Zbl 0093.03603)] is extended to the, not necessarily similar, many-sorted algebras by defining the concept of polyderivor between many-sorted signatures, which assigns to basic sorts, words and to formal operations, families of derived terms, and under which the standard signature morphisms, the basic mapping-formulas of Fujiwara, and the derivors of Goguen,Thatcher and Wagner are subsumed. Then, by means of the homomorphisms between Bénabou algebras, which are the algebraic counterpart of the finitary many-sorted algebraic theories of Bénabou (a generalization of the finitary single-sorted algebraic theories of Lawvere), the composition of polyderivors is defined from which it is obtained a corresponding category. Next, by defining the notion of transformation between polyderivors, which generalizes the relation of conjugation of \textit{T. Fujiwara} [Osaka Math. J. 12, 253--268 (1960; Zbl 0201.34401)], the category of many-sorted signatures and polyderivors is equipped with a structure of a \(2\)-category. Moreover, from this a derived \(2\)-category of many-sorted specifications is obtained.) Chapter 2, `Simple equational specifications', begins with the definitions of equation (I warn the readers about the fact that the authors consider, for a set of sorts \(S\), equations which have only finite \(S\)-sorted sets of variables), the relation of satisfaction, and equation translation. After that, the authors state the satisfaction lemma (which says that the translations of syntax and semantics induced by signature morphisms are coherent with the definition of satisfaction). Next, they define the concepts of many-sorted equational presentation (or specification), model of a presentation, equationally definable class, variety, and, following this, they state the Birkhoff's Variety Theorem (for a signature with a finite set of sorts). I point out that the authors are aware of the fact that in the many-sorted case (in contrast to what happens in the single-sorted case) one has two Birkhoff's Variety Theorems (this was first proved, to the best of my knowledge, by G. Matthiessen in his aforementioned Dissertation): one for those equations \((X,P=Q)\) for which the \(S\)-sorted set \(X\) is finite, i.e., \(X\) is such that \(\text{card}(\mathrm{supp}_{S}(X))<\aleph_{0}\), where \(\mathrm{supp}_{S}(X)\), the support of \(X\), is \(\{s\in S\mid X_{s}\neq \varnothing\}\), and, for every \(s\in \mathrm{supp}_{S}(X)\), \(\text{card}(X_{s})<\aleph_{0}\); and another for those equations \((X,P=Q)\) for which the \(S\)-sorted set \(X\) is such that, for every \(s\in S\), \(\text{card}(X_{s})<\aleph_{0}\). (I warn the readers, in passing, that even after the results contained in the above-mentioned Dissertation of G. Matthiessen and in [\textit{J. A. Goguen} and \textit{J. Meseguer}, Houston J. Math. 11, 307--334 (1985; Zbl 0602.08004)], one of the standard articles in this area, one can still find authors, e.g., \textit{J. Adámek} and \textit{J. Rosický}, who in Chapter 3 of their book [Locally presentable and accessible categories. Lond. Math. Soc. Lect. Note Ser. 189. Cambridge: Cambridge University Press (1994; Zbl 0795.18007)] surprisingly and unbelievably state, in the many-sorted case, exactly one Birkhoff's Variety Theorem and also exactly one Quasivariety Theorem (both theorems being direct translations of their homologous in the single-sorted case). Perhaps it is appropriate at this point to note that W. Tholen in his MathSciNet-review [MR2757312] of the book [\textit{J. Adámek}, \textit{J. Rosický} and \textit{E. M. Vitale}, Algebraic theories. A categorical introduction to general algebra. Cambridge: Cambridge University Press (2011; Zbl 1209.18001)] makes the following assertion: ``[\dots] and prove a new [\textit{sic}] multi-sorted Birkhoff variety theorem: equationally defined subcategories of algebras are those closed under products, subalgebras, regular quotients, and directed unions, with the last condition being redundant in the one-sorted context.'' Ignorantia eorum quæ quis scire tenetur non excusat.) Afterwards, Sannella and Tarlecki, for an \(S\)-sorted signature \(\Sigma\), define the Galois connection \((\mathrm{Mod}_{\Sigma},\mathrm{Th}_{\Sigma})\), the binary relation of semantic consequence between sets of equations and equations, and the concepts of theory and theory morphism. Following this, they define the binary relation of syntactic consequence between sets of equations and equations and state the soundness (\(\vdash_{\Sigma}\subseteq \models_{\Sigma}\)) and adequacy (\(\models_{\Sigma}\subseteq \vdash_{\Sigma}\)) theorems, obtaining in this way the completeness theorem (\(\vdash_{\Sigma} = \models_{\Sigma}\)) for the many-sorted equational logic. I must point out that the reviewer and \textit{J. Soliveres Tur} in [Houston J. Math. 31, No. 1, 103--129 (2005; Zbl 1068.18004)], after defining the concepts of equational class and equational theory for a monad in a category of sorted sets and the concept of projective limit-compatible congruence on a category, proved that the lattice of product-compatible congruences on the dual of the Kleisli category of a monad in a category of sorted sets is identical to the lattice of equational theories for the same monad. In this way we obtained a completeness theorem for monads in categories of sorted sets, and therefore independent of any explicit syntactical representation of the relevant concepts, that generalizes the completeness theorem of Goguen and Meseguer [loc. cit., Zbl 0602.08004] and provides a full categorization of many-sorted equational deduction. Moreover, the reviewer and \textit{J. Soliveres Tur} in [Rep. Math. Logic 40, 127--158 (2006; Zbl 1096.03031)], after simplifying the specification of Hall algebras as given by Goguen and Meseguer, obtained another many-sorted equational calculus from which they proved that the inference rules of abstraction and concretion laid down by Goguen and Meseguer in the aforementioned article are derived rules. After the section on many-sorted equational calculus, once defined \(\equiv_{\mathcal{E}}\), the \(\Sigma\)-congruence on \(\mathbf{T}_{\Sigma} = \mathbf{T}_{\Sigma}((\varnothing)_{s\in S})\) generated by \(\mathcal{E}\), for a presentation \((S,\Sigma,\mathcal{E})\), Sannella and Tarlecki state that \(\mathbf{T}_{\Sigma}/\equiv_{\mathcal{E}}\) is an initial model of \((S,\Sigma,\mathcal{E})\). Moreover, they state that there is a presentation \((S,\Sigma,\mathcal{E})\) such that there is no proof system which is sound and adequate with respect to satisfaction of equations in the class of initial models of \((S,\Sigma,\mathcal{E})\). In the following section the authors treat term rewriting for many-sorted universal algebra. The rest of the chapter is devoted, as the authors say, to ways in which the standard framework can be improved to make it more suitable for particular kinds of applications: conditional equations, reachable semantics, error algebras, partial algebras, order-sorted algebras, and to sketch other variations: first order predicate logic, higher-order functions, polymorphic types, non-deterministic functions and recursive definitions. As regards to category theory, treated in Chapter 3, it must be recalled that the founding fathers of this mathematical theory are \textit{S. Eilenberg} and \textit{S. MacLane} [Trans. Am. Math. Soc. 58, 231--294 (1945; Zbl 0061.09204)] in attempting to mathematically explain the notion of a natural transformation. It seems suitable to remark, by its value as a guiding principle for other disciplines in the process of approaching the standards of rigor of mathematics (as is the case of some branches of theoretical computer science), that for them: ``In a metamathematical sense our theory provides general concepts applicable to all branches of abstract mathematics, and so contributes to the current trend towards uniform treatment of different mathematical disciplines. In particular, it provides opportunities for the comparison of constructions and of the isomorphisms occurring in different branches of mathematics; in this way it mat occasionally suggest new results by analogy.'' Concerning category theory the authors of the book under review say: ``This chapter introduces the basic concepts and results of category theory. It is not our intention to provide a full-blown introductory text of category theory; although a few concepts are introduced which will not be used elsewhere in this book, we consciously refrain from discussing many important but more involved concepts and results. Our aim in this chapter is to provide a brief but comprehensive overview of the basics of category theory, both in order to make this book self-contained and to provide a handy reference.'' Furthermore, they say that: ``The most fundamental `categorical dogma' is that for many purposes it does not really matter exactly what the objects we study are; more important are their mutual relationships.'' This is an idea contained, essentially, e.g., in \textit{R. Dedekind}'s masterpiece [Was sind und was sollen die Zahlen? Braunschweig: Vieweg \& Sohn (1888; JFM 20.0049.05)], and explicitly stated, e.g., by \textit{F. W. Lawvere} in [Rev. Colomb. Mat. 20, No. 3--4, 147--178 (1986; Zbl 0648.18001)], as ``\dots it is the \textit{mutability} of mathematically precise structures (by morphisms) which is the essential content of category theory, and if the structures are themselves categories, this mutability is expressed by functors, while if the structures are functors, this mutability is expressed by natural transformations.'' In addition to the above fundamental `categorical dogma' I want to emphasize that, contrary to a widely-held belief, category theory is not only a convenient language, but an autonomous mathematical theory and a possible foundation for all of mathematics (replacing the classical theory of sets in such a foundational role). Chapter 3, `Category theory', starts with the definitions of category, small category, locally small category, and subcategory. It continues with the definition of some constructions on categories as, e.g., opposite category, product category, morphism category, and slice category. Next, the authors introduce the definitions of several types of morphisms (epimorphisms, monomorphisms, and isomorphisms) and objects (initial and final objects) in a category. Then they go on by defining some standard constructions in the categories (product, coproduct, equalizer, coequalizer, pullback, and pushout). After this they introduce the concepts of cone, cocone, limit, colimit, completeness, cocompleteness, factorization system (on p. 124, line 8, from top, instead of ``\(m_{f}\in \mathbf{K}\)'' is ``\(m_{f}\in \mathbf{M}\)''), subobject, quotient object, reachable object, co-well-powered category, and quasi-variety. The rest of the chapter is devoted to defining the concepts of functor and natural transformation and to the operations and constructions associated to them, in particular, they define the concepts of comma category, indexed category, the Grothendieck construction, and functor categories, and culminates with the definition of adjunction. I remark that the functor \(\mathbf{Tot}\) in Example 3.4.17 (p. 130) can be defined in a nice way by using the Axiom of Regularity, thus eliminating the problems in the exercise following the example. Moreover, in Exercise 3.5.23, on (p. 151) the authors say: ``Recall that any partial order gives rise to a corresponding preorder category (cf. Example 3.1.3).'' Related to this I point out that every partial order \(\mathbf{P} = (P,\leq)\), with \(\leq\) reflexive, antisymmetric and transitive on \(P\), has canonically associated a category \(\mathbf{C}(\mathbf{P})\) such that, for every \(x,y\in P\), \(\text{card}(\mathrm{Hom}_{\mathbf{C}(\mathbf{P})}(x,y)\cup \mathrm{Hom}_{\mathbf{C}(\mathbf{P})}(y,x))\leq 1\). The second part, Chapters 4 and 10, deals with the theory of institutions and morphisms between institutions and contains results which are well known. As the authors themselves say: ``[Chapters 4 and 10] provide a suitable basis for a general theory of formal software specification and development.'' However, both chapters are liable to lend support to the prejudice that category theory is an obfuscation tool for clothing simple facts in complicated terminology. The theory of institutions of Goguen and Burstall, which arose within theoretical computer science, in response to the proliferation of logics in use there, is a categorial formalization of the \textit{semantic} or \textit{model-theoretical} aspect of the intuitive notion of ``logical system'', and it has as objectives, according to \textit{J. A. Goguen} and \textit{R. M. Burstall} in [Lect. Notes Comput. Sci. 240, 313--333 (1986; Zbl 0615.68002)]: ``(1) To support as much computer science as possible independently of the underlying logical system, (2) to facilitate the transfer of results (and artifacts such as theorem provers) from one logical system to another, and (3) to permit combining a number of different logical systems.'' As a historical remark that might be helpful, it seems appropriate to remember that direct ancestors of the concept of institution, as defined by \textit{J. A. Goguen} and \textit{R. M. Burstall} in [Lect. Notes Comput. Sci. 164, 221--256 (1984; Zbl 0543.68021)], are, at the very least, the following two: (1) the concept of a \textit{regular model-theoretic language} defined by \textit{S. Feferman} in [Fundam. Math. 82, 153--165 (1974; Zbl 0296.02026)], as a system \(L = (\mathrm{Typ}_{L},\mathrm{Str}_{L},\mathrm{Stc}_{L},\models_{L})\), where \(\mathrm{Typ}_{L}\) is a non-empty set of similarity types, called the \textit{admitted types} of \(L\), and \(\mathrm{Str}_{L}\), \(\mathrm{Stc}_{L}\), \(\models_{L}\) are functions with domain \(\mathrm{Typ}_{L}\) such that for each admitted types \(\tau\), \(\tau'\): {\parindent=8mm \begin{itemize}\item[(i)] \(\mathrm{Str}_{L}(\tau)\) is a sub-collection of \(\mathrm{Str}(\tau)\) called the \textit{admitted structures for} \(L(\tau)\); \item[(ii)] \(\mathrm{Stc}_{L}(\tau)\) is a collection called the \textit{sentences} of \(L(\tau)\); \item[(iii)] \(\models_{L,\tau}\) is a sub-relation of \(\mathrm{Str}_{L}(\tau)\times \mathrm{Stc}_{L}(\tau)\) called the \textit{satisfaction} (or \textit{truth}) \textit{relation of} \(L(\tau)\); \item[(iv)] \textsl{Expansion}. If \(\tau\subseteq \tau'\), then \(\mathrm{Stc}_{L}(\tau)\subseteq \mathrm{Stc}_{L}(\tau')\); if \(\mathfrak{M}'\in \mathrm{Str}_{L}(\tau')\), then \(\mathfrak{M}'\upharpoonright\tau\in \mathrm{Str}_{L}(\tau)\) and if \(\varphi\in \mathrm{Stc}_{L}(\tau)\), then \(\mathfrak{M}'\upharpoonright\tau\models \varphi\) if, and only if \(\mathfrak{M}'\models \varphi\); \item[(v)] \textsl{Renaming.} Each \(\tau\equiv_{\gamma}\tau'\) induces a \(1-1\) correspondence \[ \overline{\gamma}\colon \mathrm{Stc}(\tau)\rightarrow \mathrm{Stc}(\tau') \] such that if \(\mathfrak{M}\in \mathrm{Str}_{L}(\tau)\) and \(\mathfrak{M}'\in \mathrm{Str}(\tau')\) and \(\mathfrak{M}\equiv_{\gamma}\mathfrak{M}'\), then \(\mathfrak{M}'\in \mathrm{Str}_{L}(\tau')\) and \(\mathfrak{M}\models \varphi \Leftrightarrow \mathfrak{M}'\models \overline{\gamma}(\varphi)\); \item[(vi)] \textsl{Isomorphism.} If \(\mathfrak{M}\in \mathrm{Str}_{L}(\tau)\) and \(\mathfrak{M}'\in \mathrm{Str}(\tau)\) and \(\mathfrak{M}\cong \mathfrak{M}'\), then \(\mathfrak{M}'\in\mathrm{Str}_{L}(\tau)\) and \(\mathfrak{M}\models \varphi \Leftrightarrow \mathfrak{M}'\models \varphi\). \end{itemize}} (2) that of a \textit{logic} \(\mathfrak{L}^{\ast}\) defined by \textit{K. J. Barwise} in [Ann. Math. Logic 7, 221--265 (1974; Zbl 0324.02034)], where he says that it consists of a syntax and a semantics which fit together nicely. The \textit{syntax of} \(\mathfrak{L}^{\ast}\) is a functor \(\ast\) on some category \(\mathbf{C}\) of languages to the category of classes. The functor \(\ast\) satisfies the following axiom: {\parindent=6mm \begin{itemize}\item{} \textsl{Occurrence Axiom.} For every \(\mathfrak{L}^{\ast}\)-sentence \(\varphi\) there is a smallest (under \(\subseteq\)) language \(L_{\varphi}\) in \(\mathbf{C}\) such that \(\varphi\in L_{\varphi}^{\ast}\). If \(i\colon L_{\varphi}\subseteq K\) is an inclusion morphism, so is \(i^{\ast}\colon L_{\varphi}^{\ast}\subseteq K^{\ast}\). \end{itemize}} The \textit{semantics of} \(\mathfrak{L}^{\ast}\) is a relation \(\models\) such that if \(\mathfrak{M}\models \varphi\), then \(\mathfrak{M}\) is an \(L\)-structure for some \(L\) in \(\mathbf{C}\) and \(\varphi\in L^{\ast}\). It satisfies the following axiom: {\parindent=6mm \begin{itemize}\item{}\textsl{Isomorphism Axiom.} If \(\mathfrak{M}\models \varphi\) and \(\mathfrak{M}\cong \mathfrak{N}\), then \(\mathfrak{N}\models \varphi\). \end{itemize}} The syntax and semantics of \(\mathfrak{L}^{\ast}\) fit together according to the final axiom. {\parindent=6mm \begin{itemize}\item{}\textsl{Translation Axiom}. For every \(\mathfrak{L}^{\ast}\) sentence \(\varphi\), every \(K\)-structure \(\mathfrak{M}\) and every morphism \(\alpha\colon L_{\varphi}\rightarrow K\), \[ \mathfrak{M}\models \alpha^{\ast}(\varphi) \text{\,\, iff \,\,} \mathfrak{M}^{-\alpha} \text{\, is an \,} L_{\varphi}\!\!-\!\!\text{structure\,} \text{\,\,and\,\,} \mathfrak{M}^{-\alpha}\models \varphi. \] \end{itemize}} I can point out that \textit{J. A. Goguen} and \textit{R. M. Burstall} in [Zbl 0543.68021], define an \textit{institution} as a category \(\mathbf{Sign}\), of signatures, a functor \(\mathrm{Sen}\) from \(\mathbf{Sign}\) to \(\mathbf{Set}\), giving the set of \textit{sentences} over a given signature, a functor \(\mathrm{Mod}\) from \(\mathbf{Sign}\) to \(\mathbf{Cat}^{\mathrm{op}}\), giving the category of \textit{models} of a given signature, and, for each \(\Sigma\in \mathbf{Sign}\), a satisfaction relation \(\models_{\Sigma}\subseteq|{\mathbf{Mod}(\Sigma)}|\times\mathrm{Sen}(\Sigma)\), where \(|\cdot|\) is the endofunctor of \(\mathbf{Cat}\) which sends a category to the discrete category on its set of objects, such that, for each morphism \(\varphi\colon \Sigma\rightarrow\Sigma'\), the {\parindent=6mm \begin{itemize}\item{}\textsl{Satisfaction Condition}: \( \mathbf{M'}\models_{\Sigma'} \varphi(e) \text{\,\, iff \,\,} \varphi(\mathbf{M'})\models_{\Sigma} e, \) \end{itemize}} holds for each \(\mathbf{M'}\in |\mathbf{Mod}(\Sigma')|\) and each \(e\in \mathrm{Sen}(\Sigma)\). Later on, in [Zbl 0615.68002], they define an \textit{institution} as a category \(\mathbf{Sign}\), of signatures, a functor \(\mathrm{Sen}\) from \(\mathbf{Sign}\) to \(\mathbf{Cat}\) (observe the large-scale change from \(\mathbf{Set}\) to \(\mathbf{Cat}\)), giving \textit{sentences} and \textit{proofs} over a given signature, a functor \(\mathrm{Mod}\) from \(\mathbf{Sign}\) to \(\mathbf{Cat}^{\mathrm{op}}\), giving the category of \textit{models} of a given signature, and a satisfaction relation \(\models_{\Sigma}\subseteq|\mathbf{Mod}(\Sigma)|\times|\mathbf{Sen}(\Sigma)|\), for each \(\Sigma\in |\mathbf{Sign}|\), such that {\parindent=6mm \begin{itemize}\item{}\textsl{\textbf{Satisfaction Condition}}: \( \mathbf{M'}\models_{\Sigma'} \mathrm{Sen}(\varphi)s \text{\, iff \,} \mathrm{Mod}(\varphi)\mathbf{M'}\models_{\Sigma} s, \) for each \(\varphi\colon \Sigma\rightarrow \Sigma'\) in \(\mathbf{Sign}\), \(\mathbf{M'}\in |\mathbf{Mod}(\Sigma')|\) and \(s\in |\mathbf{Sen}(\Sigma)|\), and \item{}\textsl{Soundness Condition}: \( \text{if } \mathbf{M}\models_{\Sigma}s, \text{ then } \mathbf{M}\models_{\Sigma} s', \) for each \(\mathbf{M}\in|\mathbf{Mod}(\Sigma)|\) and \(s\rightarrow s'\in \mathbf{Sen}(\Sigma)\). \end{itemize}} Besides, the same authors, in [Zbl 0615.68002], define, for a category \(\mathbf{V}\), a \textit{generalized} \(\mathbf{V}\)-\textit{institution} as a pair of functors \(\mathrm{Mod}\), from \(\mathbf{Sign}^{\mathrm{op}}\) to \(\mathbf{Cat}\), and \(\mathrm{Sen}\), from \(\mathbf{Sign}\) to \(\mathbf{Cat}\), with an extranatural transformation \(\models\) from \(|\mathrm{Mod}(\cdot)|\times \mathrm{Sen}(\cdot)\) to \(\mathbf{V}\). It can be observed that the second concept of institution falls under this last one because, taking as \(\mathbf{V}\) the category \(\mathbf{2}\), with two objects and just one morphism not the identity, the existence of an extranatural transformation from \(|\mathrm{Mod}(\cdot)|\times \mathrm{Sen}(\cdot)\) to \(\mathbf{2}\) is equivalent to the above satisfaction and soundness conditions. Chapter 4, `Working within an arbitrary logical system', gives a development of the formalism of the theory of institutions. The topics treated are: institutions, flat specifications (or \(\Sigma\)-presentations, for a signature \(\Sigma\)) in an arbitrary institution, the category of theories, constraints (the authors show how the different methods that are used to constraint the semantics of presentations do fit into the institutional framework), exact institutions, and institutions with reachability structure (in the last two sections the authors present extensions of the concept of institution by, as they say: ``additional structure or properties that are required to support study of more detailed properties of specifications.''). Concerning the theory of institutions I recommend that the reader consult the standard monograph in this area by \textit{R. Diaconescu} [Institution-independent model theory. Basel: Birkhäuser (2008; Zbl 1144.03001)]. On the other hand, the reviewer and \textit{J. Soliveres Tur} in [Stud. Log. 95, No. 3, 301--344 (2010; Zbl 1220.03053)] improve the classical concepts of institution with a 2-categorical dimension by replacing the signatures category by a 2-category, the model and sentence functors with pseudo-functors and the satisfaction relation by a pseudo-extranatural transformation, providing a motivating example which represents a 2-categorical extension of the equational logic institution. This generalization is founded, ultimately, on the fact that the compatibility of generalized many-sorted terms and many-sorted algebras with respect to transformations between many-sorted signatures is also valid when generalized many-sorted terms and many-sorted algebras (of different many-sorted signatures) are equipped with natural category structures. And it is the following: Let \(\mathbf{C}\) be a category. Then a \(2\)-\textit{institution on} \(\mathbf{C}\) is a quadruple \((\mathbf{Sig},\mathrm{Mod},\mathrm{Sen},(\alpha,\beta))\), where {\parindent=6mm \begin{itemize}\item[-] \(\mathbf{Sig}\) is a \(2\)-category. \item[-] \(\mathrm{Mod}\colon\mathbf{Sig}^{\mathrm{op}}\rightarrow \mathbf{Cat}\) a pseudo-functor. \item[-] \(\mathrm{Sen}\colon\mathbf{Sig}\rightarrow\mathbf{Cat}\) a pseudo-functor. \item[-] \((\alpha,\beta)\colon\mathrm{Mod}(\cdot)\times\mathrm{Sen}(\cdot)\rightarrow \mathrm{K}_{\mathbf{C}}\) a pseudo-extranatural transformation, where \(\mathrm{K}_{\mathbf{C}}\) is the functor which picks \(\mathbf{C}\). \end{itemize}} If \(\mathbf{Sig}\) is an ordinary category, then it is called an \textit{institution on} \(\mathbf{C}\). This bidimensionality, by supplying one additional degree of freedom, generates a richer world which opens the possibility to deal, e.g., not only with isomorphic but also with adjoint and equivalent many-sorted specifications. Thus carrying further the previous development which was incomplete because of its restriction to categories. Actually, if \(2\)-institutions and institutions on a category are understood as pseudo-extra\-natural transformations, then they go beyond both the classical conception of semantical truth defined (mathematically for the first time, through a recursive definition of satisfaction of a formula in an arbitrary relational system by a valuation of the variables in the system) by \textit{A. Tarski} and \textit{R. L. Vaught} in [Compos. Math. 13, 82--102 (1957; Zbl 0091.01201)], and the latest conception of institution by Goguen and Burstall in [Zbl 0615.68002]. Chapter 10, `Working with multiple logical systems', which one would have expected to follow Chapter 4, at the beginning of a `usual' treatment of the theory of institutions concentrates on the following topics: moving specifications between institutions (institution semi-morphisms, duplex institutions, and migrating specifications), institution morphisms, the category of institutions, and institution comorphisms. The authors, on p. 519, say the following: ``We will not discuss here in any detail ``forward'' (co)morphisms, in which translations of sentences and models are covariant -- they are somewhat esoteric, even though they have received some attention in the literature.'' That forward morphisms are not ``somewhat esoteric'' is shown, e.g., by the reviewer and \textit{J. Soliveres Tur} in [``A transformation between institutions representing the theorem of Herbrand-Schmidt-Wang'', Bull. Sect. Log., Univ. Łódź, Dep. Log. 38, No. 1--2, 77--94 (2009)], where it is proved that domain unification, when viewed as a suitable transformation between two convenient institutions, represents the theorem of Herbrand-Schmidt-Wang encoding many-sorted first-order logic into single-sorted first-order logic (something which, I think, is understood not only by a small number of people). The third part, Chapters 5--8, deals with formal specifications and development, and a large part of the material in these chapters is taken from works previously published by the authors. A part of the core of the book, Chapters 5 and 6, which are devoted to structured specifications and parameterisation, has become, in the opinion of the reviewer, superseded by the work by \textit{R. Diaconescu} and \textit{I. Ţuţu} in [Theor. Comput. Sci. 412, No. 28, 3145--3174 (2011; Zbl 1252.68199)]. In [loc. cit.] the authors develop module algebra for structured specifications giving semantics to specification modules through the class of models of the specification. This is done from the standpoint of the theory of institutions of Goguen and Busrtall. More explicitly, in Section 2, after stating notations and conventions about category theory and institution theory, Diaconescu and Ţuţu define, for commutative squares of signature morphisms, (weak) model amalgamation, and after that the concept of institution with (weak) model amalgamation and that of semi-exact institution (an institution with a model contravariant functor that preserves pullbacks). Next, they define the notion of an inclusion system for a category \(\mathbf{C}\) (it is a pair \((\mathbf{E},\mathbf{M})\) of wide subcategories of \(\mathbf{C}\) (the morphisms of \(\mathbf{E}\) are called abstract surjections and those of \(\mathbf{M}\) abstract inclusions) such that \(\mathbf{M}\) is a partial order and every morphism \(f\) of \(\mathbf{C}\) is uniquely factorizable as \(f = i\circ e\) with \(e\in \mathbf{E}\) and \(i\in \mathbf{M}\)) and develop a series of new concepts (and results) necessary to carry out their work, e.g., the notion of inclusive institution (i.e., an institution such that its category of signatures is endowed with an inclusion system such that whenever \(\Sigma\subseteq \Sigma'\), then \(\mathrm{Sen}(\Sigma)\subseteq \mathrm{Sen}(\Sigma')\)), and, for suitable categories, those of disjoint objects, of compatible morphisms, of preservation of objects, of free extensions along inclusions, and of idempotent-by-extension. In Section 3, Diaconescu and Ţuţu define, for an inclusive institution \(\mathbf{I}\), its structured specifications (including the introduction of new specification building operators that cover the non-protecting important situations) relative to an arbitrary, but fixed, triple \((\mathcal{T},\mathcal{D},\mathcal{H})\), where \(\mathcal{T}\) and \(\mathcal{D}\) are classes of signature morphisms of \(\mathbf{I}\) and \(\mathcal{H}\) is a class of model homomorphisms of \(\mathbf{I}\). (For an institution \(\mathbf{I}\) and a triple \((\mathcal{T},\mathcal{D},\mathcal{H})\) as above, the \((\mathcal{T},\mathcal{D},\mathcal{H})\)-structured specifications of \(\mathbf{I}\) are those that belong to the smallest class that contains the finite presentations of \(\mathbf{I}\) and is closed under the five specification building operators explicitly indicated on p. 3153.) Moreover, the semantics of each (structured) specification is given by its signature and its category of models, and the structured specifications support a natural preorder. After defining (structured) specification morphisms one obtains a category and the canonical forgetful functor from it to \(\mathbf{Sig}\) lifts finite inductive limits. In Section 4, Diaconescu and Ţuţu, among others, prove a series of new rules for the model oriented denotations of structured specifications. Finally, in Section 5, Diaconescu and Ţuţu begin by defining the concept of parameterized specification and the instantiation of parameters as a pushout of specification morphisms (which takes into account the possible sharings between the body of the parameterized module and the instance of the parameter). Concerning this they say:``[\dots] parameterized specifications are often defined just as specification morphisms \(P\rightarrow SP\) (as do Sannella and Tarlecki). We think that this is much general and does not capture precisely enough the realities of parameterized specifications, our additional condition that \(\text{Sig}[P]\subseteq \text{Sig}[SP]\) filling this additional gap. Below we will see that one of the consequences of our inclusion systems based approach is the possibility to consider sharing in a rather natural and clean way.'' After that they give interesting characterizations of the concept of instantiation of parameters. Next, since specification modules may contain more than one parameter, they define multiple parameterized specifications (a specification with a finite number of parameters satisfying a suitable condition). Following this Diaconescu and Ţuţu consider the definition of parallel instantiation of multiple parameters stating that it is an instance of the instantiation of a single parameter. Subsequently, they define the serial instantiation of multiple parameters and assuming, among others, that: (1) there exists an initial signature both in \(\mathbf{Sig}\) and in the wide subcategory of the abstract inclusions \(\mathbf{M}\), (2) the inclusion system is epic (i.e., the morphisms of \(\mathbf{E}\) are epimorphisms) and distributive (i.e., \(\mathbf{M}\) has finite (nonempty) joins, finite (nonempty) meets, and the distributive laws are satisfied), and (3) each idempotent-by-extension signature morphism admits free extensions, prove that the parallel and the serial instantiation of multiple parameters are isomorphic. Chapter 7, `Formal program development', deals with simple implementations, constructor implementations, and modular decomposition. Chapter 8, `Behavioural specifications', discusses the following topics: behavioural equivalence and abstraction, behavioural satisfaction, behavioural implementations, and to partial algebras and beyond. I believe that in connection with this chapter it is suitable to recall the very important but, unfortunately, forgotten article [in: Contributions to general algebra, Proc. Klagenfurt Conf. 1978, 193--211 (1979; Zbl 0402.08008)], written by \textit{G. Matthiessen}. In this article the author shows, in particular, that there exist notions (reduction, observability, controllability, behaviour) and theorems in many-sorted algebra which originate in the theory of automata but have no counterpart in the theory of universal algebra. The fourth part, Chapter 9, deals with proof methods and contains results which are well known. I think that it is right to say that the study of the properties of the consequence operators of logical systems starts with \textit{A. Tarski}'s 1930 article [``Über einige fundamentale Begriffe der Metamathematik'', C. R. Soc. Sc. Varsovie 23 (1930), 22--29 (1930; JFM 57.1318.03)]. Chapter 9, `Proofs for specifications', discusses the following topics: entailment systems, proof in structured specifications, entailment between specifications, correctness of constructor implementations, and proving behavioural properties. In connection with part of the subject matter of this chapter I strongly recommend the series of articles devoted to various aspects of categorical abstract algebraic logic by G. Voutsadakis. Moreover, I notice that the reviewer and \textit{J. Soliveres Tur} in [``On the morphisms and transformations of Tsuyoshi Fujiwara (as a concretion of a bidimensional many-sorted general algebra and its application to the equivalence between many-sorted clones and algebraic theories)'', Preprint, \url{arXiv: 1201.5239}], state that the closure operators \(\mathrm{Cn}_{\mathbf{\Sigma}}\), of consequence, are, essentially, the components of a suitable pseudo-functor \(\mathrm{Cn}\) from the category \(\mathbf{Sig}\), of signatures, to a convenient \(2\)-category \(\mathbf{Mnd}_{{\mathcal{V}},\mathrm{alg}}\), of monads, for a Grothendieck universe \({\mathcal{V}}\) such that \({\mathcal{U}}\in {\mathcal{V}}\), obtained by properly choosing the \(2\)-cells in the \(2\)-category \(\mathbf{Mnd}_{{\mathcal{V}}}\), of monads for \({\mathcal{V}}\), and that the pseudo-functor \(\mathrm{Cn}\) is in fact part of an entailment system, understood in a more general sense than that defined by \textit{J. Meseguer} in [Stud. Logic Found. Math. 129, 275--329 (1989; Zbl 0691.03001)] . The book is well written and the authors have made it as self-contained as it is reasonable for a part of the intended audience (see below). However, the length of the book is perhaps a little excessive (when compared to its overall depth) and, at times, reading it becomes a bit tedious; essentially, it forces the reader to plow through endlessly stacked notation and definitions (about 235 throughout 532 pages) without hardly ever arriving at a mathematically relevant or deep result. The book, as I said at the beginning of the review, is full of illustrative examples, facts, and exercises. It also contains many references for further study and also to original sources. On the other hand, according to the authors, this book has ``researchers and advanced students as its target audience.'' I believe that for a researcher more than half the book is absolutely unnecessary (how can a researcher ignore the rudiments of many-sorted universal algebra, category theory, and the theory of institutions in a field like this?), but, doubtless, the detailed explanation of notions, constructions, and problems makes it recommendable for an advanced student eager to work hard. Summarizing, to the book under review it is generally applicable what \textit{G. Birkhoff} said in [Proc. Camb. Philos. Soc. 31, 433--454 (1935; Zbl 0013.00105; JFM 61.1026.07)]: ``General classifications of abstract systems are usually characterized by a wealth of terminology and illustration, and a scarcity of consequential deduction.'' Reviewer's remarks: The authors of the book should have updated several items of the bibliography, e.g., [AHS90], [Awo06], [BW85], [Coh65], and [Mac71]. On the other hand, on p. 536, line 20 from bottom, there is ``Clavel'' instead of ``Clavela''.