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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Béziau, J.-Y.: 13 questions about universal logic. Bulletin of the Section of Logic 35(2/3), 133–150 (2006)
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)
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)
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)
Diaconescu, R.: Behavioural coherence in object-oriented algebraic specification. Technical Report IS-RR-98-0017F, Japan Advanced Institute for Science and Technology (June 1998)
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
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
Diaconescu, R.: Interpolation in Grothendieck institutions. Theoretical Computer Science 311, 439–461 (2004)
Diaconescu, R.: Behavioural specification of hierarchical object composition. Theoretical Computer Science 343(3), 305–331 (2005)
Diaconescu, R.: Institution-independent Model Theory. Birkhäuser (2008)
Diaconescu, R.: Coinduction for preordered algebras. Information and Computation 209(2), 108–117 (2011)
Diaconescu, R.: Grothendieck inclusion systems. Applied Categorical Structures 19(5), 783–802 (2011)
Diaconescu, R.: Quasi-varieties and initial semantics in hybridized institutions. Journal of Logic and Computation, doi:10.1093/logcom/ext016
Diaconescu, R., Ţuţu, I.: Foundations for structuring behavioural specifications. Journal of Logic and Algebraic Programming (to appear)
Diaconescu, R., Ţuţu, I.: On the algebra of structured specifications. Theoretical Computer Science 412(28), 3145–3174 (2011)
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)
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)
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.) Logical Environments, pp. 83–130. Cambridge (1993). Proceedings of a Workshop held in Edinburgh, Scotland (May 1991)
Diaconescu, R., Stefaneas, P.: Ultraproducts and possible worlds semantics in institutions. Theoretical Computer Science 379(1), 210–230 (2007)
Finger, M., Gabbay, D.M.: Adding a temporal dimension to a logic system. Journal of Logic, Language and Information 1(3), 203–233 (1992)
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)
Goguen, J.: Data, schema, ontology and logic integration. Journal of IGPL 13(6), 685–715 (2006)
Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)
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)
Goguen, J., Roşu, G.: Institution morphisms. Formal Aspects of Computing 13, 274–307 (2002)
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)
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)
Iida, S.: An Algebraic Formal Method for Component based Software Developments. PhD thesis, Japan Advanced Institute for Science and Technology (1999)
Jacobs, B., Rutten, J.M.: A tutorial on (co)algebras and (co)induction. Bulletin of EATCS 62, 222–259 (1997)
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)
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)
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., 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)
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)
Reichel, H.: Behavioural equivalence – a unifying concept for initial and final specifications. In: Proceedings, Third Hungarian Computer Science Conference, Akademiai Kiado, Budapest (1981)
Roşu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000)
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)
Sannella, D., Tarlecki, A.: Foundations of Algebraic Specifications and Formal Software Development. Springer (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)