Abstract
We provide a semantic basis for heterogeneous specifications that not only involve different logics, but also different kinds of translations between these. We show that Grothendieck institutions based on spans of (co)morphisms can serve as a unifying framework providing a simple but powerful semantics for heterogeneous specification.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alagi, S.: Institutions: integrating objects, XML and databases. Information and Software Technology 44, 207–216 (2002)
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)
Astesiano, E., Cerioli, M.: Relationships between logical frameworks. In: Bidoit, M., Choppy, C. (eds.) Abstract Data Types 1991 and COMPASS 1991. LNCS, vol. 655, pp. 126–143. Springer, Heidelberg (1993)
Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an evolutionary formal software-development using Casl. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 73–88. Springer, Heidelberg (2000)
Bidoit, M., Hennicker, R.: Using an institution encoding for proving consequences of structured COL-specifications. Talk at the WADT 2002, Frauenchiemsee (2002)
Borzyszkowski, T.: Logical systems for structured specifications. Theoretical Computer Science 286, 197–245 (2002)
Brinksma, E. (ed.): Information processing systems — open systems interconnection. LOTOS: a formal description technique based on the temporal ordering of observational behaviour (1988); International Standard ISO 8807
Cerioli, M.: Relationships between Logical Formalisms. PhD thesis, TD-4/93, Università di Pisa-Genova-Udine (1993)
Cerioli, M., Meseguer, J.: I borrow your logic (transporting logical structures along maps). Theoretical Computer Science 173, 311–347 (1997)
CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible from http://www.cofi.info
CoFI Semantics Task Group. Casl – The CoFI Algebraic Specification Language – Semantics. Note S-9 (Documents/CASL/Semantics, version 0.96). In: [10] (July 1999)
Diaconescu, R.: Grothendieck institutions. Applied categorical structures 10, 383–402 (2002)
Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical computer science 285, 289–318 (2002)
Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Proceedings of a Workshop on Logical Frameworks (1991)
Durán, F., Meseguer, J.: Structured theories and institutions. In: Hofmann, M., Rosolini, G., Pavlovic, D. (eds.) CTCS 1999 Conference on Category Theory and Computer Science. ENTCS 29 (1999)
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 2. Springer, Heidelberg (1990)
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B. Elsevier / MIT Press (1990)
Ghribi, B., Logrippo, L.: A validation environment for LOTOS. In: Protocol Specification, Testing and Verification, pp. 93–108 (1993)
Gibson, P., Mermet, B., Mery, D.: Feature interactions: A mixed semantic model approach. In: IWFM (1997)
Goguen, J., Rosu, G.: Institution morphisms. Formal aspects of computing 13, 274–307 (2002)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39, 95–146 (1992); Predecessor in: LNCS, vol. 164, pp. 221–256 (1984)
Goguen, J.A., Tracz, W.: An implementation-oriented semantics for module composition. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems. ch. 11, pp. 231–263. Cambridge University Press, New York (2000)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Kreowski, H.-J., Mossakowski, T.: Equivalence and difference of institutions: Simulating Horn clause logic with based algebras. Mathematical Structures in Computer Science 5, 189–215 (1995)
Martí-Oliet, N., Meseguer, J.: From abstract data types to logical frameworks. In: Reggio, G., Astesiano, E., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol. 906, pp. 48–80. Springer, Heidelberg (1995)
Meseguer, J.: General logics. In: Logic Colloquium 87, pp. 275–329. North-Holland, Amsterdam (1989)
Meseguer, J.: Conditional rewriting as a unified model of concurrency. Theoretical Computer Science 96(1), 73–156 (1992)
Mossakowski, T.: Equivalences among various logical frameworks of partial algebras. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 403–433. Springer, Heidelberg (1996)
Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002)
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)
Mossakowski, T.: Relating Casl with other specification languages: the institution level. Theoretical Computer Science 286, 367–475 (2002)
Mossakowski, T., Autexier, S., Hutter, D.: Extending development graphs with hiding. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 269–283. Springer, Heidelberg (2001)
Kolyang, T.M., Krieg-Brückner, B.: Static semantic analysis and theorem proving for Casl. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 333–348. Springer, Heidelberg (1998)
Mosses, P.D.: CoFI: The Common Framework Initiative for Algebraic Specification and Development. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 115–137. Springer, Heidelberg (1997)
Reggio, G., Astesiano, E., Choppy, C.: Casl-LTL - a Casl extension for dynamic reactive systems - summary. Technical Report of DISI - Università di Genova,DISITR- 99-34, Italy (2000)
Roggenbach, M.: CSP-Casl – a new integration of process algebra and algebraic specification. Manuscript, Bremen, submitted for publication
Roggenbach, M., Mossakowski, T.: The Csp-Casl institution and its relation to temporal logic. Manuscript, University of Bremen
Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)
Salibra, A., Scollo, G.: A soft stairway to institutions. In: Bidoit, M., Choppy, C. (eds.) Proc. 8th ADT workshop. LNCS, vol. 655, pp. 310–329. Springer, Heidelberg (1992)
Salibra, A., Scollo, G.: Interpolation and compactness in categories of preinstitutions. Mathematical Structures in Computer Science 6(3), 261–286 (1996)
Sannella, D., Tarlecki, A.: Working with multiple logical systems. In: Foundations of Algebraic Specifications and Formal Program Development. ch. 10. Cambridge University Press, Cambridge (to appear), See http://zls.mimuw.edu.pl/~tarlecki/book/index.html
Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988)
Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementations revisited. Acta Inf. 25, 233–281 (1988)
Scollo, G.: On the engineering of logics. PhD thesis, University of Twente, Enschede (1993)
Tarlecki, A.: Institution representation. draft note (1987)
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)
Tarlecki, A.: Towards heterogeneous specifications. In: Gabbay, D., Rijke, M.d. (eds.) Frontiers of Combining Systems 2, 1998. Studies in Logic and Computation, pp. 337–360. Research Studies Press, Hertfordshire (2000)
Wolter, U., Didrich, K., Cornelius, F., Klar, M., Wessäly, R., Ehrig, H.: How to cope with the spectrum of spectrum. In: Jähnichen, S., Broy, M. (eds.) KORSO 1995. LNCS, vol. 1009, pp. 173–189. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mossakowski, T. (2003). Foundations of Heterogeneous Specification. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds) Recent Trends in Algebraic Development Techniques. WADT 2002. Lecture Notes in Computer Science, vol 2755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40020-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-40020-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20537-1
Online ISBN: 978-3-540-40020-2
eBook Packages: Springer Book Archive