×

Heterogeneous logical environments for distributed specifications. (English) Zbl 1253.68231

Corradini, Andrea (ed.) et al., Recent trends in algebraic development techniques. 19th international workshop, WADT 2008, Pisa, Italy, June 13–16, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03428-2/pbk). Lecture Notes in Computer Science 5486, 266-289 (2009).
Summary: We use the theory of institutions to capture the concept of a heterogeneous logical environment as a number of institutions linked by institution morphisms and comorphisms. We discuss heterogeneous specifications built in such environments, with inter-institutional specification morphisms based on both institution morphisms and comorphisms. We distinguish three kinds of heterogeneity: (1) specifications in logical environments with universal logic (2) heterogeneous specifications focused at a particular logic, and (3) heterogeneous specifications distributed over a number of logics.
For the entire collection see [Zbl 1173.68005].

MSC:

68Q65 Abstract data types; algebraic specification
03G30 Categorical logic, topoi

Software:

Hets; Isabelle/HOL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arrais, M., Fiadeiro, J.-L.: Unifying theories in different institutions. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 81–101. Springer, Heidelberg (1996)
[2] Burstall, R.M., Goguen, J.A.: The semantics of CLEAR, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980) · Zbl 0456.68024
[3] Borceux, F.: Handbook of Categorical Algebra I. Cambridge University Press, Cambridge (1994) · Zbl 0911.18001
[4] Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1998)
[5] Cornelius, F., Baldamus, M., Ehrig, H., Orejas, F.: Abstract and behaviour module specifications. Mathematical Structures in Computer Science 9(1), 21–62 (1999) · Zbl 0923.68089
[6] Cengarle, M.V., Knapp, A., Tarlecki, A., Wirsing, M.: A heterogeneous approach to UML semantics. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 383–402. Springer, Heidelberg (2008) · Zbl 1143.68373
[7] Classen, I.: Compositionality of application oriented structuring mechanisms for algebraic specification languages with initial algebra semantics. Phd thesis, Technische Universität Berlin (1993)
[8] Codescu, M., Mossakowski, T.: Heterogeneous colimits. In: Boulanger, F., Gaston, C., Schobbens, P.-Y. (eds.) MoVaH 2008 Workshop on Modeling, Validation and Heterogeneity. IEEE press, Los Alamitos (2008)
[9] Codescu, M.: Generalized theoroidal institution comorphisms. This volume · Zbl 1253.68226
[10] Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 83–130. Cambridge Univ. Press, Cambridge (1993)
[11] Diaconescu, R.: Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages. J. Applied Categorical Structures 6, 427–453 (1998) · Zbl 0919.68087
[12] Diaconescu, R.: Grothendieck institutions. J. Applied Categorical Structures 10, 383–402 (2002) · Zbl 1008.68078
[13] Diaconescu, R.: Institution-independent model theory. Birkhäuser, Basel (2008) · Zbl 1144.03001
[14] Durán, F., Meseguer, J.: Structured theories and institutions. Theor. Comput. Sci. 309(1-3), 357–380 (2003) · Zbl 1070.68090
[15] Ehrig, H., Baldamus, M., Cornelius, F., Orejas, F.: Theory of algebraic module specification including behavioral semantics and constraints. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Algebraic Methodology and Software Technology AMAST 1991, Proc. 2nd Intl. Conf., Iowa City, 1991, Workshops in Computing, pp. 145–172. Springer, Heidelberg (1992)
[16] Ehrig, H., Baldamus, M., Orejas, F.: New concepts of amalgamation and extension for a general theory of specifications. In: Bidoit, M., Choppy, C. (eds.) Abstract Data Types 1991 and COMPASS 1991. LNCS, vol. 655, pp. 199–221. Springer, Heidelberg (1993)
[17] Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992) · Zbl 0799.68134
[18] Goguen, J.A., Rosu, G.: Institution morphisms. Formal Aspects of Compututing 13(3-5), 274–307 (2002) · Zbl 1001.68019
[19] Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993) · Zbl 0778.03004
[20] Mossakowski, T., Diaconescu, R., Tarlecki, A.: What is a logic translation? In: Beziau, J.-Y. (ed.) Logica Universalis, Birkhäuser, Basel (to appear, 2009) · Zbl 1255.03023
[21] Meseguer, J.: General logics. In: Logic Colloquium 1987, pp. 275–329. North Holland, Amsterdam (1989)
[22] Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007) · Zbl 05185799
[23] Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2), 121–154 (2002) · Zbl 1027.68613
[24] Mossakowski, T.: Different types of arrow between logical frameworks. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 158–169. Springer, Heidelberg (1996) · Zbl 1046.68509
[25] Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002) · Zbl 1014.68098
[26] Mossakowski, T.: Heterogeneous development graphs and heterogeneous borrowing. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 326–341. Springer, Heidelberg (2002) · Zbl 1077.68609
[27] Mossakowski, T.: Foundations of heterogeneous specification. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 359–375. Springer, Heidelberg (2003) · Zbl 1278.68208
[28] Mossakowski, T.: Heterogeneous Specification and the Heterogeneous Tool Set. Habilitation thesis, Universität Bremen (2005)
[29] Martini, A., Wolter, U.: A single perspective on arrows between institutions. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 486–501. Springer, Heidelberg (1998) · Zbl 1089.03510
[30] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[31] López Pombo, C., Frias, M.F.: Fork algebras as a sufficiently rich universal institution. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 235–247. Springer, Heidelberg (2006) · Zbl 1235.03086
[32] Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988) · Zbl 0654.68017
[33] Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica 25, 233–281 (1988) · Zbl 0621.68004
[34] Sannella, D., Tarlecki, A.: Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9, 229–269 (1997) · Zbl 0887.68070
[35] Tarlecki, A.: Institution representation. Unpublished note, Dept. of Computer Science, University of Edinburgh (1987)
[36] Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)
[37] Tarlecki, A.: Towards heterogeneous specifications. In: Gabbay, D., de Rijke, M. (eds.) Frontiers of Combining Systems 2. Studies in Logic and Computation, pp. 337–360. Research Studies Press (2000) · Zbl 0988.03056
[38] Tarlecki, A.: Abstract specification theory: An overview. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logics of Engineering Software. NATO Science Series – Computer and System Sciences, vol. 191, pp. 43–79. IOS Press, Amsterdam (2003)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.