On the algebra of structured specifications. (English) Zbl 1252.68199

Summary: We develop a module algebra for structured specifications with model oriented denotations. Our work extends the existing theory with specification building operators for non-protecting importation modes and with new algebraic rules (most notably for initial semantics) and upgrades the pushout-style semantics of parameterized modules to capture the (possible) sharing between the body of the parameterized modules and the instances of the parameters. We specify a set of sufficient abstract conditions, smoothly satisfied in the actual situations, and prove the isomorphism between the parallel and the serial instantiation of multiple parameters. Our module algebra development is done at the level of abstract institutions, which means that our results are very general and directly applicable to a wide variety of specification and programming formalisms that are rigorously based upon some logical system.


68Q65 Abstract data types; algebraic specification


Full Text: DOI Link


[1] Adamek, Jirí; Herrlich, Horst; Strecker, George, Abstract and concrete categories, (1990), John Wiley · Zbl 0695.18001
[2] Aiguier, Marc; Barbier, Fabrice, An institution-independent proof of the beth definability theorem, Studia logica, 85, 3, 333-359, (2007) · Zbl 1134.03043
[3] Bergstra, Jan; Heering, Jan; Klint, Paul, Module algebra, Journal of the association for computing machinery, 37, 2, 335-372, (1990) · Zbl 0696.68040
[4] Bergstra, Jan; Tucker, John, Elementary algebraic specifications of the rational complex numbers, (), 459-475 · Zbl 1132.68485
[5] Borceux, Francis, Handbook of categorical algebra, (1994), Cambridge University Press · Zbl 0911.18001
[6] Borzyszkowski, Tomasz, Logical systems for structured specifications, Theoretical computer science, 286, 2, 197-245, (2002) · Zbl 1061.68104
[7] Burstall, Rod; Goguen, Joseph, Putting theories together to make specifications, (), 1045-1058
[8] Burstall, Rod; Goguen, Joseph, The semantics of clear, a specification language, (), 292-332
[9] Emil Căzănescu, Virgil; Roşu, Grigore, Weak inclusion systems, Mathematical structures in computer science, 7, 2, 195-206, (1997) · Zbl 0886.18001
[10] Diaconescu, Răzvan, Elementary diagrams in institutions, Journal of logic and computation, 14, 5, 651-674, (2004) · Zbl 1104.03036
[11] Diaconescu, Răzvan, An institution-independent proof of Craig interpolation theorem, Studia logica, 77, 1, 59-79, (2004) · Zbl 1048.03026
[12] Diaconescu, Răzvan, Institution-independent model theory, (2008), Birkhäuser · Zbl 1144.03001
[13] Diaconescu, Răzvan; Futatsugi, Kokichi, ()
[14] Răzvan Diaconescu, Joseph Goguen, Petros Stefaneas, Logical support for modularisation, in: Gerard Huet and Gordon Plotkin (Eds.), Logical Environments, Cambridge, 1993, pp. 83-130. Proceedings of a Workshop held in Edinburgh, Scotland, May 1991.
[15] Werner Fey, Pragmatics, concepts, syntax, semantics and correctness notions of ACT TWO: an algebraic module specification and interconnection language, Technical Report 88-26, Technical University of Berlin, Fachbereich Informatik, 1988. · Zbl 1086.68521
[16] Goguen, Joseph; Burstall, Rod, Institutions: abstract model theory for specification and programming, Journal of the association for computing machinery, 39, 1, 95-146, (1992) · Zbl 0799.68134
[17] Goguen, Joseph; Diaconescu, Răzvan, An Oxford survey of order sorted algebra, Mathematical structures in computer science, 4, 4, 363-392, (1994) · Zbl 0939.68710
[18] Goguen, Joseph; Meseguer, José, Order-sorted algebra solves the constructor selector, multiple representation and coercion problems, (), 18-29, Also Report CSLI-87-92, Center for the Study of Language and Information, Stanford University, March 1987; revised version in Information and Computation, 103, 1993 · Zbl 0796.68144
[19] Goguen, Joseph; Roşu, Grigore, Composing hidden information modules over inclusive institutions, (), 96-123 · Zbl 1278.68203
[20] Goguen, Joseph; Winkler, Timothy; Meseguer, José; Futatsugi, Kokichi; Jouannaud, Jean-Pierre, Introducing OBJ, ()
[21] Hodges, Wilfrid, Model theory, (1993), Cambridge University Press · Zbl 0789.03031
[22] Lane, Saunders Mac, Categories for the working Mathematician, (1998), Springer · Zbl 0906.18001
[23] Meseguer, José, General logics, (), 275-329 · Zbl 0691.03001
[24] ()
[25] Popescu, Andrei; Şerbănuţă, Traian; Roşu, Grigore, A semantic approach to interpolation, Theoretical computer science, 410, 12-13, 1109-1128, (2009) · Zbl 1159.03023
[26] Roşu, Grigore, Axiomatisability in inclusive equational logic, Mathematical structures in computer science, 12, 5, 541-563, (2002) · Zbl 1019.03050
[27] Donald Sannella, Andrzej Tarlecki, Foundations of Algebraic Specifications and Formal Program Development, Cambridge University Press (in press). · Zbl 1237.68129
[28] Sannella, Donald; Tarlecki, Andrzej, Specifications in an arbitrary institution, Information and control, 76, 165-210, (1988) · Zbl 0654.68017
[29] Tarlecki, Andrzej, On the existence of free models in abstract algebraic institutions, Theoretical computer science, 37, 269-304, (1986) · Zbl 0608.68014
[30] Tarlecki, Andrzej; Burstall, Rod; Goguen, Joseph, Some fundamental algebraic tools for the semantics of computation, part 3: indexed categories, Theoretical computer science, 91, 239-264, (1991) · Zbl 0755.18004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.