×

zbMATH — the first resource for mathematics

Structured theories and institutions. (English) Zbl 1070.68090
Summary: Category theory provides an excellent foundation for studying structured specifications and their composition. For example, theories can be structured together in a diagram, and their composition can be obtained as a colimit. There is, however, a growing awareness, both in theory and in practice, that structured theories should not be viewed just as the “scaffolding” used to build unstructured theories: they should become first-class citizens in the specification process. Given a logic formalized as an institution \(\mathcal I\), we therefore ask whether there is a good definition of the category of structured \(\mathcal I\)-theories, and whether they can be naturally regarded as the ordinary theories of an appropriate institution \(\mathcal S(\mathcal I)\) generalizing the original institution \(\mathcal I\). We answer both questions in the affirmative, and study good properties of the institution \(\mathcal I\) inherited by \(\mathcal S(\mathcal I)\). We show that, under natural conditions, a number of important properties are indeed inherited, including cocompleteness of the category of theories, liberality, and extension of the basic framework by freeness constraints. The results presented here have been used as a foundation for the module algebra of the Maude language, and seem promising as a semantic basis for a generic module algebra that could be both specified and executed within the logical framework of rewriting logic.
Reviewer: Reviewer (Berlin)

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
18C10 Theories (e.g., algebraic theories), structure, and semantics
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barr, M.; Wells, C., Toposes, triples and theories, (1985), Springer Berlin · Zbl 0567.18001
[2] Baumeister, H., Unifying initial and loose semantics of parameterized specifications in an arbitrary institution, (), 103-120 · Zbl 0967.68533
[3] M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas, D. Sannella (Eds.), Algebraic System Specification and Development. A Survey and Annotated Bibliography, Lecture Notes in Computer Science, Vol. 501, Springer, Berlin, 1991. · Zbl 0875.68642
[4] Burstall, R.; Goguen, J., The semantics of clear, a specification language, (), 292-332 · Zbl 0456.68024
[5] M. Clavel, Reflection in general logics and in rewriting logic with applications to the Maude language, Ph.D. Thesis, Universidad de Navarra, 1998.
[6] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martı́-Oliet, N.; Meseguer, J.; Quesada, J., Maudespecification and programming in rewriting logic, Theoret. comput. sci., 285, 187-243, (2002) · Zbl 1001.68059
[7] Clavel, M.; Meseguer, J., Reflection and strategies in rewriting logic, (), available at · Zbl 0917.68107
[8] CoFI Task Group on Language Design, CASL—The common algebraic specification language, version 1.0, available at , October 1998.
[9] Diaconescu, R.; Futatsugi, K., Cafeobj report, AMAST series, (1998), World Scientific Singapore
[10] Diaconescu, R.; Goguen, J.; Stefaneas, P., Logical support for modularisation, (), 83-130
[11] T. Dimitrakos, Parameterising (algebraic) specifications on diagrams, in: Proc. of 13th IEEE Internat. Conf. on Automated Software Engineering (ASE’98), 1998.
[12] F. Durán, A reflective module algebra with applications to the Maude language, Ph.D. Thesis, Universidad de Málaga, June 1999.
[13] Durán, F.; Meseguer, J., An extensible module algebra for maude, (), available at · Zbl 0919.68076
[14] Durán, F.; Meseguer, J., Structured theories and institutions, (), 71-90, available at
[15] H. Ehrig, B. Mahr, Fundamentals of Algebraic Specification, Vol. 1, Equations and Initial Semantics, Springer, Berlin, 1985. · Zbl 0557.68013
[16] H. Ehrig, B. Mahr, Fundamentals of Algebraic Specification, Vol. 2, Module Specifications and Constraints, Springer, Berlin, 1990. · Zbl 0759.68013
[17] Gogolla, M.; Cerioli, M., What is an abstract data type after all?, (), 499-523
[18] Goguen, J.; Burstall, R., Introducing institutions, (), 221-256 · Zbl 1288.03001
[19] Goguen, J.; Burstall, R., Institutionsabstract model theory for specification and programming, J. ACM, 39, 1, 95-146, (1992) · Zbl 0799.68134
[20] J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, J.-P. Jouannaud, Introducing OBJ, Tech. Report SRI-CSL-92-03, Computer Science Laboratory, SRI International, March 1992.
[21] MacLane, S., Categories for the working Mathematician, (1971), Springer Berlin
[22] Martı́-Oliet, N.; Meseguer, J., From abstract data types to logical frameworks, (), 504-514
[23] Martı́-Oliet, N.; Meseguer, J., Rewriting logic as a logical and semantic framework, (), available at · Zbl 0912.68096
[24] Meseguer, J., General logics, (), 275-329
[25] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. comput. sci., 96, 73-155, (1992) · Zbl 0758.68043
[26] Meseguer, J., Membership algebra as a semantic framework for equational specification, (), 18-61 · Zbl 0903.08009
[27] Orejas, F.; Pino, E.; Ehrig, H., Institutions for logic programming, Theor. comput. sci., 173, 485-511, (1997) · Zbl 0901.68027
[28] Reichel, H., Initially-restricting algebraic theories, (), 504-514 · Zbl 0469.68026
[29] Sannella, D.; Tarlecki, A., Specifications in an arbitrary institution, Inform. and comput., 76, 2/3, 165-210, (1988) · Zbl 0654.68017
[30] Sannella, D.; Wirsing, M., A kernel language for algebraic specification and implementation, (), 415-427
[31] Schubert, H., Categories, (1972), Springer Berlin
[32] Srinivas, Y.; Jüllig, R., SPECWARE: formal support for composing software, (), 399-422
[33] A. Tarlecki, Towards heterogeneous specifications, in: Proc. of Workshop on Frontiers of Combining Systems (FroCos’98), Kluwer Academic, Dordrecht, 1998. · Zbl 0988.03056
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.