{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T01:30:53Z","timestamp":1649122253302},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T00:00:00Z","timestamp":1185926400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,8]]},"abstract":"<jats:p>We extend the coalgebraic account of specification and refinement of objects and classes in object-oriented programming given by Reichel and Jacobs to<jats:italic>(generalised) binary methods<\/jats:italic>. These are methods that take more than one parameter of a class type. Class types include products, sums and powerset type constructors. To allow for class<jats:italic>constructors<\/jats:italic>, we model classes as<jats:italic>bialgebras<\/jats:italic>. We study and compare two solutions for modelling generalised binary methods, which use purely covariant functors.<\/jats:p><jats:p>In the first solution, which applies when we already have a class implementation, we reduce the behaviour of a generalised binary method to that of a bunch of unary methods. These are obtained by<jats:italic>freezing<\/jats:italic>the types of the extra class parameters to constant types. If all parameter types are<jats:italic>finitary<\/jats:italic>, the<jats:italic>bisimilarity equivalence<\/jats:italic>induced on objects by this model yields the<jats:italic>greatest congruence<\/jats:italic>with respect to method application.<\/jats:p><jats:p>In the second solution, we treat binary methods as<jats:italic>graphs<\/jats:italic>instead of functions, thus turning contravariant occurrences in the functor into covariant ones.<\/jats:p><jats:p>We show the existence of<jats:italic>final coalgebras<\/jats:italic>in both cases.<\/jats:p>","DOI":"10.1017\/s0960129507006214","type":"journal-article","created":{"date-parts":[[2007,8,2]],"date-time":"2007-08-02T13:34:17Z","timestamp":1186061657000},"page":"647-673","source":"Crossref","is-referenced-by-count":0,"title":["Coalgebraic description of generalised binary methods"],"prefix":"10.1017","volume":"17","author":[{"given":"FURIO","family":"HONSELL","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MARINA","family":"LENISA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"REKHA","family":"REDAMALLA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2007,8,1]]},"reference":[{"key":"S0960129507006214_ref16","unstructured":"Huisman M. (2001) Reasoning about Java programs in Higher-order logic using PVS and Isabelle, Ph.D. thesis, University of Nijmegen, The Netherlands."},{"key":"S0960129507006214_ref26","unstructured":"Tews H. (2002) Coalgebraic Methods for Object-Oriented Specifications, Ph.D. thesis, Dresden University of technology, 2002."},{"key":"S0960129507006214_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00025-1"},{"key":"S0960129507006214_ref25","first-page":"175","article-title":"The Coalgebraic Class Specification Language CCSL","volume":"7","author":"Rothe","year":"2001","journal-title":"Journal of Universal Computer Science"},{"key":"S0960129507006214_ref1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1044"},{"key":"S0960129507006214_ref2","unstructured":"Aczel P. (1988) Non-wellfounded sets, CSLI Lecture Notes 14"},{"key":"S0960129507006214_ref9","first-page":"493","article-title":"Set-theory with free construction principles","volume":"10","author":"Forti","year":"1983","journal-title":"Ann. Scuola Norm. Sup. Pisa"},{"key":"S0960129507006214_ref20","first-page":"222","article-title":"A tutorial on (co)algebras and (co)induction","volume":"62","author":"Jacobs","year":"1996","journal-title":"Bulletin of the EATCS"},{"key":"S0960129507006214_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-1437-0_5"},{"key":"S0960129507006214_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00275-3"},{"key":"S0960129507006214_ref21","doi-asserted-by":"crossref","unstructured":"Lenisa M. (1996) Final Semantics for a Higher Order Concurrent Language. In: Kirchner H. . (eds.) CAAP'96. Springer-Verlag Lecture Notes in Computer Science 1059 102\u2013118.","DOI":"10.1007\/3-540-61064-2_32"},{"key":"S0960129507006214_ref18","doi-asserted-by":"crossref","unstructured":"Jacobs B. (1996a) Inheritance and cofree constructions. In: Cointe P. (ed.) ECOOP'96. Springer-Verlag Lecture Notes in Computer Science 1098 210\u2013231.","DOI":"10.1007\/BFb0053063"},{"key":"S0960129507006214_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S096012959900287X"},{"key":"S0960129507006214_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80275-0"},{"key":"S0960129507006214_ref4","unstructured":"van den Berg J. , Huisman M. , Jacobs B. and Poll E. (1999) A type-theoretic memory model for verification of sequential Java programs. In: Bert . (eds.) WADT'99. Springer-Verlag Lecture Notes in Computer Science 1827 1\u201321."},{"key":"S0960129507006214_ref8","unstructured":"Cirstea C. (2000) Integrating observations and computations in the specification of state-based, dynamical systems, Ph.D. thesis, University of Oxford."},{"key":"S0960129507006214_ref3","doi-asserted-by":"crossref","unstructured":"Aczel P. and Mendler N. (1989) A Final Coalgebra Theorem. In: Pitt D. H. . (eds.) Proc. category theory and computer science. Springer-Verlag Lecture Notes in Computer Science 389 357\u2013365.","DOI":"10.1007\/BFb0018361"},{"key":"S0960129507006214_ref5","first-page":"221","article-title":"On Binary Methods","volume":"1","author":"Bruce","year":"1995","journal-title":"TAPOS"},{"key":"S0960129507006214_ref19","doi-asserted-by":"crossref","unstructured":"Jacobs B. (1997) Behaviour-refinement of object-oriented specifications with coinductive correctness proofs. In: Bidoit M. . (eds.) TAPSOFT'97. Springer-Verlag Lecture Notes in Computer Science 1214 787\u2013802.","DOI":"10.1007\/BFb0030641"},{"key":"S0960129507006214_ref6","doi-asserted-by":"crossref","unstructured":"Cancila D. , Honsell F. and Lenisa M. (2006) Some Properties and Some Problems on Set Functors. CMCS'06. Electronic Notes in Theoretical Computer Science (to appear).","DOI":"10.1016\/j.entcs.2006.06.005"},{"key":"S0960129507006214_ref12","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"S0960129507006214_ref27","first-page":"280","volume-title":"12th LICS","author":"Turi","year":"1997"},{"key":"S0960129507006214_ref13","doi-asserted-by":"crossref","unstructured":"Honsell F. and Lenisa M. (1995) Final Semantics for Untyped Lambda Calculus. In: Dezani M. . (eds.) TLCA'95. Springer-Verlag Lecture Notes in Computer Science 902 249\u2013265.","DOI":"10.1007\/BFb0014057"},{"key":"S0960129507006214_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.024"},{"key":"S0960129507006214_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80915-0"},{"key":"S0960129507006214_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000694"},{"key":"S0960129507006214_ref24","first-page":"252","article-title":"Hidden Congruent Deduction. FTP'98","volume":"1761","author":"Rosu","year":"2000","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129507006214","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T17:55:09Z","timestamp":1556733309000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129507006214\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,8]]}},"alternative-id":["S0960129507006214"],"URL":"https:\/\/doi.org\/10.1017\/s0960129507006214","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8]]}}}