Skip to main content
SpringerLink
Log in
Book cover

Logics of Specification Languages pp 153–240Cite as

A Methodological Guide to the CafeOBJ Logic

  • Chapter
  • First Online:

Abstract

CafeOBJ is an executable industrial-strength algebraic specification language; it is a modern successor of OBJ and incorporates several new algebraic specification paradigms. It was developed in Japan with large-scale support from the Japanese government. Its definition is given in [12], a presentation of its logical foundations can be found in [14], and a presentation of some methodologies developed around CafeOBJ can be found in [15, 16]. CafeOBJ is intended to be used mainly for system specification, formal verification of specifications, rapid prototyping, and even programming.

This is a preview of subscription content, 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   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Arrais and J.L. Fiadeiro. Unifying theories in different institutions. In M. Haveraaen, O. Owe, and O.-J. Dahl, editors, Recent Trends in Data Type Specification, Proceedings of 11th Workshop on Specification of Abstract Data Types, Volume 1130 of Lecture Notes in Computer Science, pages 81–101. Springer, 1996.

    Google Scholar 

  2. G. Birkhoff. On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society, 31:433–454, 1935.

    Article  Google Scholar 

  3. R. Burstall and J. Goguen. The semantics of Clear, a specification language. In D. Bjørner, editor, Proceedings, 1979 Copenhagen Winter School on Abstract Software Specification, Volume 86 of Lecture Notes in Computer Science, pages 292–332, Springer, 1980.

    Google Scholar 

  4. M. Clavel, S. Eker, P. Lincoln and J. Meseguer. Principles of Maude. Electronic Notes in Theoretical Computer Science, 4, 1996. Proceedings, First International Workshop on Rewriting Logic and its Applications, Asilomar, California, September 1996.

    Google Scholar 

  5. R. Diaconescu. 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.

    Article  MathSciNet  Google Scholar 

  6. R. Diaconescu. Category-based constraint logic. Mathematical Structures in Computer Science, 10(3):373–407, 2000.

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  8. R. Diaconescu. Institution-independent ultraproducts. Fundamenta Informaticæ, 55(3–4):321–348, 2003.

    MathSciNet  MATH  Google Scholar 

  9. R. Diaconescu. Elementary diagrams in institutions. Journal of Logic and Computation, 14(5):651–674, 2004.

    Article  MathSciNet  Google Scholar 

  10. R. Diaconescu. An institution-independent proof of Craig Interpolation Theorem. Studia Logica, 77(1):59–79, 2004.

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  14. R. Diaconescu and K. Futatsugi. Logical foundations of CafeOBJ. Theoretical Computer Science, 285:289–318, 2002.

    Article  MathSciNet  Google Scholar 

  15. R. Diaconescu, K. Futatsugi and Shusaku Iida. Component-based algebraic specification and verification in CafeOBJ. In J. M. Wing, J.C.P. Woodcock and J. Davies, editors, FM’99 — Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1644–1663. Springer, 1999.

    Google Scholar 

  16. R. Diaconescu, K. Futatsugi and S. Iida. CafeOBJ Jewels. In K. Futatsugi, A. Nakagawa and T. Tamai, editors, Cafe: An Industrial-Strength Algebraic Formal Method. Elsevier, 2000.

    Google Scholar 

  17. R. Diaconescu, J. Goguen, and P. Stefaneas. Logical support for modularisation. In G. Huet and G. Plotkin, editors, Logical Environments, Proceedings of a Workshop held in Edinburgh, Scotland, May 1991, pages 83–130, Cambridge University Press, 1993.

    Google Scholar 

  18. K. Futatsugi, J. Goguen, J.-P. Jouannaud and J. Meseguer. Principles of OBJ2. In B. K. Reid, editor, Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 52–66. ACM, 1985.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  20. J. Goguen and R. Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(4):363–392, 1994.

    Article  MathSciNet  Google Scholar 

  21. J. Goguen and R. Diaconescu. Towards an algebraic semantics for the object paradigm. In Hartmut Ehrig and Fernando Orejas, editors, Recent Trends in Data Type Specification, volume 785 of Lecture Notes in Computer Science, pages 1–34. Springer, 1994.

    Google Scholar 

  22. J. Goguen and G. Malcolm. A hidden agenda. Technical Report CS97-538, University of California at San Diego, 1997.

    Google Scholar 

  23. J. Goguen and J. Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307–334, 1985.

    MathSciNet  MATH  Google Scholar 

  24. J. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105(2):217–273, 1992. Also, Programming Research Group Technical Monograph PRG-80, Oxford University, December 1989.

    Article  MathSciNet  Google Scholar 

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

    Article  Google Scholar 

  26. J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi and Jean-Pierre Jouannaud. Introducing OBJ. In Joseph Goguen and Grant Malcolm, editors, Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, 2000.

    Google Scholar 

  27. D. Găină and A. Popescu. An institution-independent generalization of Tarski’s Elementary Chain Theorem. Journal of Logic and Computation, 16(6):713–735, 2006.

    Article  MathSciNet  Google Scholar 

  28. D. Găină and A. Popescu. An institution-independent proof of Robinson consistency theorem. Studia Logica, 85(1):41–73, 2007.

    Article  MathSciNet  Google Scholar 

  29. R. Hennicker and M. Bidoit. Observational logic. In A. M. Haeberer, editor, Algebraic Methodology and Software Technology, Proceedings of AMAST’99, Volume 1584 of Lecture Notes in Computer Science, pages 263–277. Springer, 1999.

    Google Scholar 

  30. S. Iida, K. Futatsugi, and R. Diaconescu. Component-based algebraic specification: behavioural specification for component-based software engineering. In Behavioral Specifications of Businesses and Systems, pages 103–119. Kluwer, 1999.

    Google Scholar 

  31. S. Mac Lane. Categories for the Working Mathematician. Springer, second edition, 1998.

    Google Scholar 

  32. J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992.

    Article  MathSciNet  Google Scholar 

  33. J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Pressice, editor, Proceedings of WADT’97, Volume 1376 of Lecture Notes in Computer Science, pages 18–61. Springer, 1998.

    Google Scholar 

  34. T. Mossakowski. Comorphism-based Grothendieck logics. In K. Diks and W. Rytter, editors, Mathematical Foundations of Computer Science, volume 2420 of Lecture Notes in Computer Science, pages 593–604. Springer, 2002.

    Google Scholar 

  35. T. Mossakowski. Relating CASL with other specification languages: the institution level. Theoretical Computer Science, 286:367–475, 2002.

    Article  MathSciNet  Google Scholar 

  36. T. Mossakowski. Heterogeneous specification and the heterogeneous tool set. Habilitation thesis, University of Bremen, 2005.

    Google Scholar 

  37. R. Paré and D. Schumacher. Abstract families and the adjoint functor theorems. In P.T. Johnstone and R. Paré, editors, Indexed Categories and Their Applications. Springer, 1978.

    Google Scholar 

  38. M. Petria and R. Diaconescu. Abstract Beth definability in institutions. Journal of Symbolic Logic, 71(3):1002–1028, 2006.

    Article  MathSciNet  Google Scholar 

  39. H. Reichel. Behavioural equivalence — a unifying concept for initial and final specifications. In Proceedings, Third Hungarian Computer Science Conference. Akademiai Kiado, 1981. Budapest.

    Google Scholar 

  40. H. Reichel. Initial Computability, Algebraic Specifications, and Partial Algebras. Clarendon, 1987.

    Google Scholar 

  41. D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Control, 76:165–210, 1988. An earlier version appeared in Proceedings, International Symposium on the Semantics of Data Types, Volume 173 of Lecture Notes in Computer Science, Springer, 1985.

    MathSciNet  MATH  Google Scholar 

  42. A. Tarlecki. Free constructions in algebraic institutions. In M.P. Chytil and V. Koubek, editors, Proceedings, International Symposium on Mathematical Foundations of Computer Science, Volume 176 of Lecture Notes in Computer Science, pages 526–534. Springer, 1984. Extended version: Report CSR-149-83, Computer Science Department, University of Edinburgh.

    Google Scholar 

  43. A. Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences, 33(3):333–360, 1986. Original version, Report CSR-173-84, Computer Science Department, University of Edinburgh.

    Article  MathSciNet  Google Scholar 

  44. A. Tarlecki, R. Burstall and J. Goguen. Some fundamental algebraic tools for the semantics of computation, part 3: Indexed categories. Theoretical Computer Science, 91:239–264, 1991. Also, Monograph PRG-77, August 1989, Programming Research Group, Oxford University.

    Article  MathSciNet  Google Scholar 

  45. U. Wolter. Institutional frames. In Recent Trends in Data Type Specification. Proceedings of the 10th Workshop on Algebrauic Data Type Specification, Santa Margherita, Italy, 1994., Volume 906 of Lecture Notes in Computer Science, pages 469–482. Springer, Berlin, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics “Simion Stoilow”, PO Box 1-764, Bucharest, 014700, 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. Informatics and Mathematical Modelling, Technical University of Denmark, 2800, Kgs. Lyngby, Denmark

    Dines Bjørner

  2. Department of Computer Science, University of Essex, Wivenhoe Park, CO4 3SQ, Colchester, UK

    Martin C. Henson

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Diaconescu, R. (2008). A Methodological Guide to the CafeOBJ Logic. In: Bjørner, D., Henson, M.C. (eds) Logics of Specification Languages. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74107-7_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74107-7_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74106-0

  • Online ISBN: 978-3-540-74107-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation