Skip to main content
SpringerLink
Log in

Heterogeneous Logical Environments for Distributed Specifications

  • Conference paper
Recent Trends in Algebraic Development Techniques (WADT 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5486))

Included in the following conference series:

Abstract

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.

This work has been partially supported by European projects IST-2005-015905 MOBIUS and IST-2005-016004 SENSORIA, by a visiting grant to the University of Illinois at Urbana-Champaign (AT) and by the German Federal Ministry of Education and Research (Project 01 IW 07002 FormalSafe) and by the DFG-funded SFB/TR 8 “Spatial cognition” (TM).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  3. Borceux, F.: Handbook of Categorical Algebra I. Cambridge University Press, Cambridge (1994)

    Book  MATH  Google Scholar 

  4. Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1998)

    Google Scholar 

  5. Cornelius, F., Baldamus, M., Ehrig, H., Orejas, F.: Abstract and behaviour module specifications. Mathematical Structures in Computer Science 9(1), 21–62 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  7. Classen, I.: Compositionality of application oriented structuring mechanisms for algebraic specification languages with initial algebra semantics. Phd thesis, Technische Universität Berlin (1993)

    Google Scholar 

  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)

    Google Scholar 

  9. Codescu, M.: Generalized theoroidal institution comorphisms. This volume

    Google Scholar 

  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)

    Google Scholar 

  11. Diaconescu, R.: Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages. J. Applied Categorical Structures 6, 427–453 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  12. Diaconescu, R.: Grothendieck institutions. J. Applied Categorical Structures 10, 383–402 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  13. Diaconescu, R.: Institution-independent model theory. Birkhäuser, Basel (2008)

    MATH  Google Scholar 

  14. Durán, F., Meseguer, J.: Structured theories and institutions. Theor. Comput. Sci. 309(1-3), 357–380 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  17. Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  18. Goguen, J.A., Rosu, G.: Institution morphisms. Formal Aspects of Compututing 13(3-5), 274–307 (2002)

    Article  MATH  Google Scholar 

  19. Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  21. Meseguer, J.: General logics. In: Logic Colloquium 1987, pp. 275–329. North Holland, Amsterdam (1989)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  23. Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2), 121–154 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  25. Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  28. Mossakowski, T.: Heterogeneous Specification and the Heterogeneous Tool Set. Habilitation thesis, Universität Bremen (2005)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  30. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  32. Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  33. Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica 25, 233–281 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  34. Sannella, D., Tarlecki, A.: Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9, 229–269 (1997)

    Article  MATH  Google Scholar 

  35. Tarlecki, A.: Institution representation. Unpublished note, Dept. of Computer Science, University of Edinburgh (1987)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Computer Science, Albert-Ludwigs-Universität Freiburg, Germany

    Till Mossakowski

  2. Safe and Secure Cognitive Systems, DFKI GmbH, Bremen, Germany

    Till Mossakowski

  3. Institute of Informatics, University of Warsaw, Poland

    Andrzej Tarlecki

  4. Institute of Computer Science, Polish Academy of Sciences, Poland

    Andrzej Tarlecki

Authors
  1. Till Mossakowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrzej Tarlecki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Largo Bruno Pontecorvo 3, 56127, Pisa, Italy

    Andrea Corradini  & Ugo Montanari  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mossakowski, T., Tarlecki, A. (2009). Heterogeneous Logical Environments for Distributed Specifications. In: Corradini, A., Montanari, U. (eds) Recent Trends in Algebraic Development Techniques. WADT 2008. Lecture Notes in Computer Science, vol 5486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03429-9_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-03429-9_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-03428-2

  • Online ISBN: 978-3-642-03429-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation