{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,3]],"date-time":"2025-08-03T04:05:18Z","timestamp":1754193918241},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442332"},{"type":"electronic","value":"9783540457886"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45788-7_1","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T15:04:02Z","timestamp":1188313442000},"page":"1-20","source":"Crossref","is-referenced-by-count":6,"title":["Formal Methods in CafeOBJ"],"prefix":"10.1007","author":[{"given":"Kokichi","family":"Futatsugi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"1_CR1","unstructured":"Burstall, R. and Goguen, J. A., \u201cPutting Theories Together to Make Specifications\u201d, In Reddy, R. editor, Proc. of 5th IJCAI, 1977, pp. 1045\u20131058. 1, 3, 5, 17"},{"key":"1_CR2","unstructured":"Diaconescu, R., Extra Theory Morphisms for Institutions: logical semantics for multi-paradigm languages, Jour. of Applied Categorical Structures, 1998, a preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997. 5, 6"},{"key":"1_CR3","series-title":"AMAST Series in Computing","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume-title":"CafeOBJ report","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R. and Futatsugi, K., CafeOBJ report. AMAST Series in Computing, 6. World Scientific, Singapore, 1998. 1, 2, 3, 4, 5, 6, 12, 15, 17"},{"issue":"1","key":"1_CR4","first-page":"74","volume":"6","author":"R. Diaconescu","year":"2000","unstructured":"Diaconescu, R. and Futatsugi, K., Behavioural Coherence in Object-Oriented Algebraic Specification. Journal of Universal Computer Science, 6(1):74\u201396, 2000. 4, 5","journal-title":"Journal of Universal Computer Science"},{"key":"1_CR5","unstructured":"Diaconescu, R. and Futatsugi, K., Logical Foundations of CafeOBJ, Theoretical Comupter Science, to appear. 6"},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1644","DOI":"10.1007\/3-540-48118-4_37","volume-title":"Component-based Algebraic Specification and Verification in CafeOBJ","author":"R. Diaconescu","year":"1999","unstructured":"Diaconescu, R., Futatsugi, K., and Iida, S., Component-based Algebraic Specification and Verification in CafeOBJ, Lecture Notes in Computer Science, 1708, pp. 1644\u20131663, 1999. 3, 12, 15"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K., and Iida, S., CafeOBJ Jewels, in Futatsugi, K., Nakagawa, A.T., and Tamai, T., editors, CAFE: An Industiral-Strength Algebraic Formal Method, Elsevier, pp.33\u201360, 2000. 1","DOI":"10.1016\/B978-044450556-9\/50062-9"},{"key":"1_CR8","unstructured":"Futatsugi, K., Hierarchical Software Development in HISP, in Computer Science and Technologies 1982, ed. Kitagawa, T., Japan Annual Review in Electronics, Computers and Telecommunications Series, OHMSHA\/North-Holland, pp.151\u2013174, 1982. 1, 3, 17, 18"},{"key":"1_CR9","unstructured":"Futatsugi, K., An Overview of OBJ2\u201d, Proc. of Franco-Japanese Symp. on Programming of Future Generation Computers, Tokyo, Oct. 1986, published as Programming of Future Generation Computers, ed. Fuchi, K. and Nivat, M., North-Holland, pp.139\u2013160, 1988. 2, 3, 4"},{"key":"1_CR10","unstructured":"Futatsugi, K., Trends in Formal Specification Methods based on Algebraic Specification Techniques \u2014 from Abstract Data Types to Software Processes: A Personal Perspective \u2014, Proceedings of the International Conference of Information Technology to Commemorating the 30th Anniversary of the Information Processing Society of Japan (InfoJapan\u201990), pp.59\u201366, October 1990, (invited talk). 1, 3, 17"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Goguen, J. A., Jouannaud, J.-P., and Meseguer, J., Principles of OBJ2, Proceedings of the 12th ACM Symposium on Principles of Programming Languages, ACM, pp.55\u201366, 1985. 2, 3, 4","DOI":"10.1145\/318593.318610"},{"volume-title":"OBJ\/CafeOBJ\/Maude at Formal Methods\u2019 99","year":"1999","key":"1_CR12","unstructured":"Futatsugi, K., Goguen, J., Meseguer, J., editors, OBJ\/CafeOBJ\/Maude at Formal Methods\u2019 99, The Theta Foundation, Bucharest, Romania, (ISBN 973-99097-1-X), 1999. 1"},{"key":"1_CR13","unstructured":"Futatsugi, K., Goguen, J.A., Meseguer, J., and Okada, K., Parameterized Programming in OBJ2, Proc. of the 9th ICSE, IEEE, pp.51\u201360, 1987. 1, 3, 18"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Futatsugi, K. and Nakagawa, A., An Overview of CAFE Specification Environment \u2014 an algebraic approach for creating, verifying, and maintaining formal specifications over networks \u2014, Proc. 1st Intl. Conf. of Formal Engineering Methods, IEEE Press, pp.170\u2013181, 1997. 3","DOI":"10.1109\/ICFEM.1997.630424"},{"key":"1_CR15","unstructured":"Futatsugi, K. and Ogata, K., Rewriting Can Verify Distributed Real-time Systems, Proc. of International Symposium on Rewriting, Proof, and Computation, PRC\u201901, pp.60\u201379, Oct. 2001, (invited talk). 3"},{"key":"1_CR16","unstructured":"Futatsugi, K. and Okada, K., Specification Writing as Construction of hierarchically Structured Clusters of Operators, Proc. of IFIP Congress 80, Tokyo, pp. 287\u2013292, Oct.1980. 3, 18"},{"key":"1_CR17","unstructured":"Futatsugi, K. and Okada, K., A Hierarchical Structuring Method for Functional Software Systems, Proc. of the 6th ICSE, pp.393\u2013402, 1982. 3, 18"},{"key":"1_CR18","unstructured":"Futatsugi, K. and Sawada, T., Design Considerations for Cafe Specification Environment, in Proc. OBJ2 10th Anniversary Workshop, Numazu, Japan, Oct.1995. 1, 3"},{"volume-title":"CAFE: An Industrial-Strength Algebraic Formal Method","year":"2000","key":"1_CR19","unstructured":"Futatsugi, K., Nakagawa, A., and Tamai, T., editors, CAFE: An Industrial-Strength Algebraic Formal Method, Elsevier Science B.V., Amsterdam, The Netherlands, (ISBN 0-444-50556-3), 2000. 1"},{"issue":"1","key":"1_CR20","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J. Goguen","year":"1992","unstructured":"Goguen, J. and Burstall, R., Institutions: Abstract Model Theory for Specification and Programming, Journal of the Association for Computing Machinery, 39(1), pp.95\u2013146, 1992. 5, 6","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4","key":"1_CR21","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1017\/S0960129500000517","volume":"4","author":"J. Goguen","year":"1994","unstructured":"Goguen, J. and Diaconescu, R., An Oxford Survey of Order Sorted Algebra, Mathematical Structures in Computer Science, 4(4), pp.363\u2013392, 1994. 5, 6","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR22","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S0304-3975(99)00275-3","volume":"245","author":"J. Goguen","year":"2000","unstructured":"Goguen, J. and Malcolm, G., A hidden agenda. Theoret. Comput. Sci., 245:55\u2013101, 2000. 4","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR23","unstructured":"Goguen, J. and Meseguer, J., Eqlog: Equality, Types, and Generic Modules for Logic Programming, in Logic Programming: Functions, Relations and Equations, DeGroot, D. and Lindstrom, G. editors, Prentice-Hall, pp.295\u2013363, 1986. 3, 6"},{"issue":"2","key":"1_CR24","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A. and Meseguer, J., Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations, Theoretical Computer Science, 105(2), pp.217\u2013273, 1992. 5, 7","journal-title":"Theoretical Computer Science"},{"key":"1_CR25","unstructured":"Goguen, J. and Meseguer, J., Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics, in Research Directions in Object-Oriented Programming, Shriver, B. and Wegner, P. editors, MIT Press, pp.417\u2013477, 1987. 3, 6"},{"key":"1_CR26","unstructured":"Goguen, J.A., Thatcher, J.W., and Wagner, E.G., An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types, IBM Research Report RC-6487, 1976; also in Current Trends in Programming Methodology, Vol.4: Data Structuring, ed. Yeh, R. T., Prentice-Hall, pp.80\u2013149, 1978. 1"},{"key":"1_CR27","unstructured":"Goguen, J.A., Thatcher, J.W., Wagner, E.G., and Wright, J. B., Abstract Data Types as Initial Algebras and the Correctness of Data Representation, Computer Graphics, Pattern Recognition and Data Structure, IEEE, pp.89\u201393, 1975. 1"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., and Jouannaud, J.P., Introducing OBJ, in Joseph Goguen and Grant Malcolm, editors, Software Engineering with OBJ, pp.3\u2013167, Kluwer Academic Publishers, 2000. 2, 4, 18","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"1_CR29","first-page":"27","volume":"10","author":"J.V. Guttag","year":"1978","unstructured":"Guttag, J.V. and Horning, J. J., The Algebraic Specification of Abstract Data Types, Acta Infomatica, 10, pp.27\u201352, 1978. 1","journal-title":"Acta Infomatica"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Iida, S., Diaconescu, R., Futatsugi, K., Component-Based Algebraic Specification-Behavioural Specification for Component-based Software Engineering-, in Behavioral Specifications of Bussiness and Systems, Kluwer Academic Publishers, pp.105\u2013121, 1999. 4, 12, 15","DOI":"10.1007\/978-1-4615-5229-1_8"},{"key":"1_CR31","unstructured":"Ishikawa, H., Futatsugi, K., and Watanabe, T., Concurrent Reflective Computations in Rewriting Logic (Extended Abstract), in Proc. of TRS Sympo. at RIMS, Kyoto, June, 1995. 17"},{"key":"1_CR32","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1073\/pnas.50.5.869","volume":"50","author":"F. W. Lawvere","year":"1963","unstructured":"Lawvere, F. W., Functorial Semantics of Algebraic Theories (Summary of Ph.D. Thesis, Columbia University), Proceedings, National Academy of Sciences, U. S.A., 50, pp.869\u2013872, 1963. 3","journal-title":"Proceedings, National Academy of Sciences"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Meseguer, J., A logical theory of cuncurrent objects, In ECOOP-OOPSLA\u201990 Conference on Object-Oriented Programming, ACM, Oct.1990, pp.101\u2013115. 3, 5, 6","DOI":"10.1145\/97945.97958"},{"issue":"1","key":"1_CR34","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, 96(1), pp73\u2013155, 1992. 3, 5, 6, 17","journal-title":"Theoretical Computer Science"},{"key":"1_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Proc. WADT\u201997","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J., Membership algebra as a logical framework for equational specification, in Parisi-Presicce, F. ed., Proc. WADT\u201997, Springer LNCS 1376, pp.18\u201361, 1998. 6"},{"key":"1_CR36","unstructured":"Okada, K. and Futatsugi, K., Supporting the Formal Description Process for Communication Protocols by an Algebraic Specification Language OBJ2, Proc. Of Second International Symposium on Interoperable Information System (ISIIS\u201988), Tokyo, pp.127\u2013134, 1988. 3"},{"key":"1_CR37","unstructured":"Ohmaki, K., Futatsugi, K., and Takahashi, K., A Basic LOTOS Simulator in OBJ, Proceedings of InfoJapan\u201990 Computer Conference, Part 1, IPSJ, pp.497\u2013504, 1990. 3"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Smolka, G., Nutt, W. Goguen, J., and Meseguer, J., Order-Sorted Equational Computation, in Resolution of Equations in Algebraic Structures, Vol 2., Rewriting Techniques, eds A\u00eft-Kaci, H. and Nivat, M., Academic Press, Inc., pp.297\u2013368, 1989. 7","DOI":"10.1016\/B978-0-12-046371-8.50016-X"},{"key":"1_CR39","unstructured":"Srinivas, Y.V., J\u00fclling, R., SPECWARE: Formal Support for Composing Software, Tech. Reprot KES.U.94.5, Kestrel Institute, 1994. 1, 18"},{"key":"1_CR40","unstructured":"Stevens, A. and Goguen, J., Mechanised theorem proving with 2OBJ: A tutorial introduction, Programming Research Group, University of Oxford, 1993. 3"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45788-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T17:11:58Z","timestamp":1556817118000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45788-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442332","9783540457886"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-45788-7_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}