Skip to main content
SpringerLink
Log in

CafeOBJ Traces

  • Chapter
Specification, Algebra, and Software

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

  • 735 Accesses

Abstract

We survey two important distinctive features of CafeOBJ, namely behavioural specification based upon coherent hidden algebra and heterogeneous specification based upon Grothendieck institutions. Both of them represent seminal contributions to formal specification culture that go much beyond the realm of CafeOBJ. Our presentation includes rather detailed explanations of the motivations and of the process leading to the inception of these concepts and theories. The paper is dedicated to Professor Kokichi Futatsugi, the leader of the CafeOBJ project, and also close friend and collaborator, on the occasion of his retirement.

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. Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: The common algebraic specification language. Theoretical Computer Science 286(2), 153–196 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  2. Béziau, J.-Y.: 13 questions about universal logic. Bulletin of the Section of Logic 35(2/3), 133–150 (2006)

    MathSciNet  MATH  Google Scholar 

  3. Burstall, R., Diaconescu, R.: Hiding and behaviour: An institutional approach. In: William Roscoe, A. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 75–92. Prentice-Hall, 1994. Also in Technical Report ECS-LFCS-8892-253, Laboratory for Foundations of Computer Science, University of Edinburgh (1992)

    Google Scholar 

  4. Carnielli, W., Coniglio, M., Gabbay, D.M., Gouveia, P., Sernadas, C.: Analysis and Synthesis of Logics How to Cut and Paste Reasoning Systems. Applied Logic —Series, vol. 35. Springer (2008)

    Google Scholar 

  5. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  6. Diaconescu, R.: Behavioural coherence in object-oriented algebraic specification. Technical Report IS-RR-98-0017F, Japan Advanced Institute for Science and Technology (June 1998)

    Google Scholar 

  7. Diaconescu, R.: Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages. Applied Categorical Structures 6(4), 427–453 (1998). A preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997

    Google Scholar 

  8. Diaconescu, R.: Grothendieck institutions. Applied Categorical Structures 10(4), 383–402 (2002); Preliminary version appeared as IMAR Preprint 2-2000 (February 2000) ISSN 250-3638

    Google Scholar 

  9. Diaconescu, R.: Interpolation in Grothendieck institutions. Theoretical Computer Science 311, 439–461 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  10. Diaconescu, R.: Behavioural specification of hierarchical object composition. Theoretical Computer Science 343(3), 305–331 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  11. Diaconescu, R.: Institution-independent Model Theory. Birkhäuser (2008)

    Google Scholar 

  12. Diaconescu, R.: Coinduction for preordered algebras. Information and Computation 209(2), 108–117 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  13. Diaconescu, R.: Grothendieck inclusion systems. Applied Categorical Structures 19(5), 783–802 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  14. Diaconescu, R.: Quasi-varieties and initial semantics in hybridized institutions. Journal of Logic and Computation, doi:10.1093/logcom/ext016

    Google Scholar 

  15. Diaconescu, R., Ţuţu, I.: Foundations for structuring behavioural specifications. Journal of Logic and Algebraic Programming (to appear)

    Google Scholar 

  16. Diaconescu, R., Ţuţu, I.: On the algebra of structured specifications. Theoretical Computer Science 412(28), 3145–3174 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  17. Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol. 6. World Scientific (1998)

    Google Scholar 

  18. Diaconescu, R., Futatsugi, K.: Behavioural coherence in object-oriented algebraic specification. Universal Computer Science 6(1), 74–96 (2000); First version appeared as JAIST Technical Report IS-RR-98-0017F (June 1998)

    Google Scholar 

  19. Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical Computer Science 285, 289–318 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  20. Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 83–130. Cambridge (1993). Proceedings of a Workshop held in Edinburgh, Scotland (May 1991)

    Google Scholar 

  21. Diaconescu, R., Stefaneas, P.: Ultraproducts and possible worlds semantics in institutions. Theoretical Computer Science 379(1), 210–230 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  22. Finger, M., Gabbay, D.M.: Adding a temporal dimension to a logic system. Journal of Logic, Language and Information 1(3), 203–233 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  23. Goguen, J.: Types as theories. In: Reed, G.M., Roscoe, A.W., Wachter, R.F. (eds.) Topology and Category Theory in Computer Science, pp. 357–390. Oxford (1991). Proceedings of a Conference held at Oxford (June 1989)

    Google Scholar 

  24. Goguen, J.: Data, schema, ontology and logic integration. Journal of IGPL 13(6), 685–715 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  25. Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  26. Goguen, J., Diaconescu, R.: Towards an algebraic semantics for the object paradigm. In: Ehrig, H., Orejas, F. (eds.) Abstract Data Types 1992 and COMPASS 1992. LNCS, vol. 785, pp. 1–34. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  27. Goguen, J., Roşu, G.: Institution morphisms. Formal Aspects of Computing 13, 274–307 (2002)

    Article  MATH  Google Scholar 

  28. Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action. Kluwer (2000)

    Google Scholar 

  29. Grothendieck, A.: Catégories fibrées et descente. In: Revêtements Étales et Groupe Fondamental, Séminaire de Géométrie Algébraique du Bois-Marie 1960/61, Exposé VI. Lecture Notes in Mathematics, vol. 224. Institut des Hautes Études Scientifiques (1963); Reprinted in Lecture Notes in Mathematics, vol. 224, pp. 145–194. Springer (1971)

    Google Scholar 

  30. Iida, S.: An Algebraic Formal Method for Component based Software Developments. PhD thesis, Japan Advanced Institute for Science and Technology (1999)

    Google Scholar 

  31. Jacobs, B., Rutten, J.M.: A tutorial on (co)algebras and (co)induction. Bulletin of EATCS 62, 222–259 (1997)

    MATH  Google Scholar 

  32. Martins, M.A., Madeira, A., Diaconescu, R., Barbosa, L.S.: Hybridization of institutions. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 283–297. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  33. 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 

  34. 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 

  35. Mossakowski, T., Kutz, O., Lange, C.: Semantics of Distributed Ontology Language: Institutes and institutions. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 212–230. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  36. Popescu, A., Roşu, G.: Behavioral extensions of institutions. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 331–347. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  37. Reichel, H.: Behavioural equivalence – a unifying concept for initial and final specifications. In: Proceedings, Third Hungarian Computer Science Conference, Akademiai Kiado, Budapest (1981)

    Google Scholar 

  38. Roşu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000)

    Google Scholar 

  39. Roşu, G., Lucanu, D.: Circular coinduction: A proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  40. Sannella, D., Tarlecki, A.: Foundations of Algebraic Specifications and Formal Software Development. Springer (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Simion Stoilow Institute of Mathematics Romanian Academy, Romania

    Răzvan Diaconescu

Authors
  1. Răzvan Diaconescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Network and Information, Senshu University, 2-1-1 Higashi-mita, Tama-ku, 214-8580, Kawasaki, Kanagawa, Japan

    Shusaku Iida

  2. Department of Computer Science, Thomas M. Siebel Center for Computer Science, University of Illinois at Urbana-Champaign (UIUC), 201 N. Goodwin Avenue, MC 258, 61801, Urbana, IL, USA

    José Meseguer

  3. School of Information Science, Advanced Institute of Science and Technology (JAIST), 1-1 Asahidai, 923-1292, Nomi, Ishikawa, Japan

    Kazuhiro Ogata

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Diaconescu, R. (2014). CafeOBJ Traces. In: Iida, S., Meseguer, J., Ogata, K. (eds) Specification, Algebra, and Software. Lecture Notes in Computer Science, vol 8373. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54624-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-54624-2_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-54623-5

  • Online ISBN: 978-3-642-54624-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation