×

zbMATH — the first resource for mathematics

Logical foundations of CafeOBJ. (English) Zbl 1001.68079
Summary: This paper surveys the logical and mathematical foundations of CafeOBJ, which is a successor of the famous algebraic specification language OBJ but adds to it several new primitive paradigms such as behavioural concurrent specification and rewriting logic. We first give a concise overview of CafeOBJ. Then we focus on the actual logical foundations of the language at two different levels: basic specification and structured specification, including also the definition of the CafeOBJ institution. We survey some novel or more classical theoretical concepts supporting the logical foundations of CafeOBJ, pointing out the main results but without giving proofs and without discussing all mathematical details. Novel theoretical concepts include the coherent hidden algebra formalism and its combination with rewriting logic, and Grothendieck (or fibred) institutions. However, for proofs and for some of the mathematical details not discussed here we give pointers to relevant publications. The logical foundations of CafeOBJ are structured by the concept of institution. Moreover, the design of CafeOBJ emerged from its logical foundations, and institution concepts played a crucial rôle in structuring the language design.

MSC:
68Q65 Abstract data types; algebraic specification
Software:
CafeOBJ; Maude; OBJ3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R. Burstall, J. Goguen, The semantics of Clear, a specification language, in: D. Bjorner (Ed.), Proceedings, 1979 Copenhagen Winter School on Abstract Software Specification, Springer, Berlin, 1980, pp. 292-332 (Lecture Notes in Computer Science, Vol. 86; based on unpublished notes handed out at the Symposium on Algebra and Applications, Stefan Banach Center, Warsaw, Poland, 1978.) · Zbl 0456.68024
[2] Buss, S.; Roşu, G., Incompleteness of behavioural logics, (), 61-79
[3] M. Clavel, S. Eker, P. Lincoln, J. Meseguer, Principles of Maude, Electronic Notes in Theoretical Computer Science, Vol. 4, Elseiver Science, Amsterdam, 1996. (Proc., 1st Internat. Workshop on Rewriting Logic and its Applications, Asilomar, CA, September 1996.)
[4] Căzănescu, V.E.; Roşu, G., Weak inclusion systems, Math. struct. comput. sci., 7, 2, 195-206, (1997) · Zbl 0886.18001
[5] R. Diaconescu, Category-based semantics for equational and constraint logic programming, DPhil. Thesis, University of Oxford, 1994.
[6] Diaconescu, R., Completeness of category-based equational deduction, Math. struct. comput. sci., 5, 1, 9-41, (1995) · Zbl 0835.18003
[7] R. Diaconescu, Behavioural rewriting logic: semantic foundations and proof theory, October 1996, unpublished manuscript. · Zbl 0912.68092
[8] R. Diaconescu, Completeness of semantic paramodulation: a category-based approach, Technical Report IS-RR-96-0006S, Japan Advanced Institute for Science and Technology, 1996.
[9] R. Diaconescu, Foundations of behavioural specification in rewriting logic, Electronic Notes in Theoretical Computer Science, Vol. 4, Elseiver Science, Amsterdam, 1996. (Proc., 1st Internat. Workshop on Rewriting Logic and its Applications. Asilomar, CA, September 1996.) · Zbl 0912.68092
[10] R. Diaconescu, Extra theory morphisms for institutions: logical semantics for multi-paradigm languages, J. Appl. Categorical Struct. 6(4) (1998) 427-453. (A preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997.) · Zbl 0919.68087
[11] Diaconescu, R., Category-based constraint logic, J. math. struct. comput. sci., 10, 3, 373-407, (2000) · Zbl 0955.68022
[12] R. Diaconescu, Grothendieck institutions, IMAR Preprint 2-2000, Institute of Mathematics of the Romanian Academy, February 2000, ISSN 250-3638.
[13] Diaconescu, R.; Futatsugi, K., cafeobj report: the language, proof techniques, and methodologies for object-oriented algebraic specification, of AMAST series in computing, Vol. 6, (1998), World Scientific Singapore
[14] R. Diaconescu, K. Futatsugi, Behavioural coherence in object-oriented algebraic specification, J. Universal Comput. Sci. 6(1) (2000) 74-96. (First version appeared as JAIST Technical Report IS-RR-98-0017F, June 1998.) · Zbl 0963.68104
[15] Diaconescu, R.; Futatsugi, K.; Iida, S., Component-based algebraic specification and verification in cafeobj, (), 1644-1663
[16] Diaconescu, R.; Futatsugi, K.; Iida, S., cafeobj jewels, ()
[17] R. Diaconescu, J. Goguen, P. Stefaneas, Logical support for modularisation, in: G. Huet, G. Plotkin (Eds.), Logical Environments, Cambridge University Press, Cambridge, 1993, pp. 83-130. (Proc. a Workshop held in Edinburgh, Scotland, May 1991.)
[18] R. Diaconescu, P. Stefaneas, Categorical foundations of modularization for multi-paradigm languages, Technical Report IS-RR-98-0014F, Japan Advanced Institute for Science and Technology, 1998.
[19] Futatsugi, K.; Goguen, J.; Jouannaud, J.-P.; Meseguer, J., Principles of OBJ2, (), 52-66
[20] J. Goguen, Theorem Proving and Algebra, MIT Press, Cambridge, MA, 2002, in preparation.
[21] Goguen, J.; Burstall, R., Institutionsabstract model theory for specification and programming, J. ACM, 39, 1, 95-146, (1992) · Zbl 0799.68134
[22] Goguen, J.; Diaconescu, R., An Oxford survey of order sorted algebra, Math. struct. comput. sci., 4, 4, 363-392, (1994) · Zbl 0939.68710
[23] Goguen, J.; Diaconescu, R., Towards an algebraic semantics for the object paradigm, (), 1-34 · Zbl 0941.68637
[24] J. Goguen, G. Malcolm, A hidden agenda, Technical Report CS97-538, University of California at San Diego, 1997. · Zbl 0946.68070
[25] J. Goguen, J. Meseguer, Eqlog: Equality, types, and generic modules for logic programming, in: D. DeGroot, G. Lindstrom (Eds.), Logic Programming: Functions, Relations and Equations, Prentice-Hall, Englewood Cliffs, NJ, 1986, pp. 295-363. (An earlier version appears in J. Logic Programming, 1(2) (1984) 179-210.)
[26] J. Goguen, J. Meseguer, Unifying functional, object-oriented and relational programming, with logical semantics, in: B. Shriver, P. Wegner (Eds.), Research Directions in Object-Oriented Programming, MIT Press, Cambridge, MA, 1987, pp. 417-477. (Preliminary version in SIGPLAN Notices 21(10) (1986) 153-162.)
[27] J. Goguen, J. Meseguer, Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. Comput. Sci. 105(2) (1992) 217-273. (Also, Programming Research Group Technical Monograph PRG-80, Oxford University, December 1989.) · Zbl 0778.68056
[28] Goguen, J.; Thatcher, J.; Wagner, E., An initial algebra approach to the specification, correctness and implementation of abstract data types, technical report RC 6487, IBM T.J. Watson research center, October 1976, (), 80-149
[29] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J.-P., Introducing OBJ, ()
[30] A. Grothendieck, Catégories fibrées et descente, in: Revêtements étales et groupe fundamental, Séminaire de Géométrie Algébraique du Bois-Marie 1960/61, Exposé VI, Institut des Hautes Études Scientifiques, 1963. (Reprinted in Lecture Notes in Mathematics, Vol. 224, Springer, Berlin, 1971, pp. 145-94.)
[31] R. Hennicker, M. Bidoit, Observational logic, in: A.M. Haeberer (Ed.), Algebraic Methodology and Software Technology, Vol. 1584, Lecture Notes in Computer Science, Springer, Berlin, 1999, pp. 263-277. (Proc. AMAST’99.) · Zbl 1088.68112
[32] H. Hilberdink, Foundations for rewriting logic, in: K. Futatsugi (Ed.), The 3rd Internat. Workshop on Rewriting Logic and its Applications, Kanazawa, Japan, 2000. · Zbl 0966.68088
[33] Iida, S.; Futatsugi, K.; Diaconescu, R., Component-based algebraic specification: — behavioural specification for component-based software engineering, (), 103-119
[34] MacLane, S., Categories for the working Mathematician, (1998), Springer Berlin
[35] J. Meseguer, Rewriting as a unified model of concurrency, Technical Report SRI-CSL-90-02R, SRI International, Computer Science Laboratory, February 1990, Revised June 1990. · Zbl 0758.68043
[36] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. comput. sci., 96, 1, 73-155, (1992) · Zbl 0758.68043
[37] Meseguer, J., Membership algebra as a logical framework for equational specification, (), 18-61 · Zbl 0903.08009
[38] Meseguer, J.; Goguen, J., Initiality, induction and computability, (), 459-541 · Zbl 0571.68004
[39] R. Paré, D. Schumacher, Indexed Categories and their Applications, Lecture Notes in Mathematics, Vol. 661, Springer, Berlin, 1978, pp. 1-125 (chapter Abstract Families and the Adjoint Functor Theorems).
[40] A. Tarlecki, R. Burstall, J. Goguen, Some fundamental algebraic tools for the semantics of computation, part 3: indexed categories, Theoret. Comput. Sci. 91 (1991) 239-264. (Also, Monograph PRG-77, August 1989, Programming Research Group, Oxford University.) · Zbl 0755.18004
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.