{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:37:05Z","timestamp":1759991825121},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357046"},{"type":"electronic","value":"9783642357053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35705-3_10","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T01:49:52Z","timestamp":1357091392000},"page":"204-223","source":"Crossref","is-referenced-by-count":6,"title":["Higher-Order UTP for a Theory of Methods"],"prefix":"10.1007","author":[{"given":"Frank","family":"Zeyda","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer (1996)","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Back, R.-J., Preoteasa, V.: Reasoning About Recursive Procedures with Parameters. In: Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding. ACM (August 2003)","DOI":"10.1145\/976571.976573"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-21437-0_20","volume-title":"FM 2011: Formal Methods","author":"A. Cavalcanti","year":"2011","unstructured":"Cavalcanti, A., Wellings, A., Woodcock, J.: The Safety-Critical Java Memory Model: A Formal Account. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 246\u2013261. Springer, Heidelberg (2011)"},{"issue":"1","key":"10_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/1328897.1328452","volume":"43","author":"W.-N. Chin","year":"2008","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing Modular OO Verification with Separation Logic. ACM SIGPLAN Not\u00a043(1), 87\u201399 (2008)","journal-title":"ACM SIGPLAN Not"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-85762-4_10","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"W. Harwood","year":"2008","unstructured":"Harwood, W., Cavalcanti, A., Woodcock, J.: A Theory of Pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 141\u2013155. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"10_CR6","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.tcs.2006.07.034","volume":"365","author":"J. He","year":"2006","unstructured":"He, J., Li, X., Liu, Z.: rCOS:\u00a0A refinement calculus for object systems. Theoretical Computer Science\u00a0365(1-2), 109\u2013142 (2006)","journal-title":"Theoretical Computer Science"},{"key":"10_CR7","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall (February 1998)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/11526841_5","volume-title":"FM 2005: Formal Methods","author":"I.T. Kassios","year":"2005","unstructured":"Kassios, I.T.: Decoupling in Object Orientation. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 43\u201358. Springer, Heidelberg (2005)"},{"key":"10_CR9","unstructured":"Naumann, D.: Predicate Transformer Semantics of an Oberon-Like Language. In: Proceedings of the IFIP TC2\/WG2.1\/WG2.2\/WG2.3 Working Conference on Programming Concepts, Methods and Calculi, PROCOMET 1994, pp. 467\u2013487 (1994)"},{"issue":"1","key":"10_CR10","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/0304-3975(94)00247-G","volume":"150","author":"D. Naumann","year":"1995","unstructured":"Naumann, D.: Predicate transformers and higher-order programs. Theoretical Computer Science\u00a0150(1), 111\u2013159 (1995)","journal-title":"Theoretical Computer Science"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/11768173_13","volume-title":"Unifying Theories of Programming","author":"G. Nuka","year":"2006","unstructured":"Nuka, G., Woodcock, J.: Mechanising a Unifying Theory. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol.\u00a04010, pp. 217\u2013235. Springer, Heidelberg (2006)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11768173_8","volume-title":"Unifying Theories of Programming","author":"M. Oliveira","year":"2006","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying Theories in ProofPower-Z. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol.\u00a04010, pp. 123\u2013140. Springer, Heidelberg (2006)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11768173_2","volume-title":"Unifying Theories of Programming","author":"T. Santos","year":"2006","unstructured":"Santos, T., Cavalcanti, A., Sampaio, A.: Object-Orientation in the UTP. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol.\u00a04010, pp. 18\u201337. Springer, Heidelberg (2006)"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/BF01214920","volume":"8","author":"M. Spivey","year":"1996","unstructured":"Spivey, M.: The Consistency Theorem for Free Type Definitions in Z. Formal Aspects of Computing\u00a08, 369\u2013375 (1996)","journal-title":"Formal Aspects of Computing"},{"key":"10_CR16","unstructured":"Woodcock, J., Davies, J.: Using Z:\u00a0Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall (July 1996)"},{"key":"10_CR17","unstructured":"Zeyda, F.: A Theory of Methods:\u00a0Validation of Laws. Technical report (July 2012), \n                  \n                    http:\/\/www.cs.york.ac.uk\/circus\/hijac\/publication.html"},{"issue":"4","key":"10_CR18","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1016\/j.scico.2010.02.010","volume":"77","author":"F. Zeyda","year":"2012","unstructured":"Zeyda, F., Cavalcanti, A.: Mechanical reasoning about families of UTP theories. Science of Computer Programming\u00a077(4), 444\u2013479 (2012)","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35705-3_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:24:15Z","timestamp":1620134655000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35705-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642357046","9783642357053"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35705-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}