{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:17:43Z","timestamp":1737091063357,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_27","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"471-490","source":"Crossref","is-referenced-by-count":10,"title":["Forward Simulation for Data Refinement of Classes"],"prefix":"10.1007","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and K. Rustan M. Leino. A logic of object-oriented programs. In Proceedings, TAPSOFT 1997. Springer-Verlag, 1997. Expanded in DEC SRC report 161.","DOI":"10.1007\/BFb0030634"},{"key":"27_CR2","series-title":"Ser. A","volume-title":"Technical report","author":"R. J. R. Back","year":"1987","unstructured":"R. J. R. Back. Procedural Abstraction in the Refinement Calculus. Technical report, Department of Computer Science, \u00c5bo-Finland, 1987. Ser. A No. 55."},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"R. J. R. Back and J. Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Anindya Banerjee and David Naumann. Representation independence, confinement and access control. In POPL2002, pages 166\u2013177, 2001.","DOI":"10.1145\/565816.503289"},{"key":"27_CR5","unstructured":"Martin B\u00fcchi and Wolfgang Weck. The greybox approach: When blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science, August 1999. http:\/\/www.abo.fi\/~mbuechi\/publications\/TR297.html ."},{"key":"27_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1439","DOI":"10.1007\/3-540-48118-4_26","volume-title":"FM\u201999: World Congress on Formal Methods","author":"A. L. C. Cavalcanti","year":"1999","unstructured":"A. L. C. Cavalcanti and D. Naumann. A Weakest Precondition Semantics for an Object-oriented Language of Refinement. In J. M. Wing, J. C. P. Woodcock, and J. Davies, editors, FM\u201999: World Congress on Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1439\u20131459. Springer-Verlag, September 1999."},{"issue":"8","key":"27_CR7","doi-asserted-by":"crossref","first-page":"713","DOI":"10.1109\/32.879810","volume":"26","author":"A. L. C. Cavalcanti","year":"2000","unstructured":"A. L. C. Cavalcanti and D. A. Naumann. A Weakest Precondition Semantics for Refinement of Object-oriented Programs. IEEE Transactions on Software Engineering, 26(8):713\u2013728, August 2000.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"27_CR8","unstructured":"A. L. C. Cavalcanti and D. A. Naumann. Forward Simulation for Data Refinement of Classes-Extended Version. Technical Report 2001-4, Computer Science, Stevens Institute of Technology, 2001. http:\/\/www.cs.stevens-tech.edu\/~naumann\/tr2001-4.ps ."},{"key":"27_CR9","unstructured":"A. L. C. Cavalcanti and David A. Naumann. On a specification-oriented model for object-orientation. In Proceedings of the VI Brazilian Symposium on Programming Languares, 2002. To appear."},{"issue":"1","key":"27_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1590\/S0104-65001998000200002","volume":"5","author":"A. L. C. Cavalcanti","year":"1998","unstructured":"A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. Procedures and Recursion in the Refinement Calculus. Journal of the Brazilian Computer Society, 5(1):1\u201315, 1998.","journal-title":"Journal of the Brazilian Computer Society"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Willem-Paul de Roever and Kai Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9780511663079"},{"key":"27_CR12","unstructured":"David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Technical Report Report 159, Compaq Systems Research Center, December 1998."},{"key":"27_CR13","unstructured":"Martin Fowler. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 1999."},{"key":"27_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(91)90029-2","volume":"87","author":"P. H. B. Gardiner","year":"1991","unstructured":"P. H. B. Gardiner and C. C. Morgan. Data Refinement of Predicate Transformers. Theoretical Computer Science, 87:143\u2013162, 1991.","journal-title":"Theoretical Computer Science"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"J. He, C. A. R. Hoare, and J. W. Sanders. Prespecification in Data Refinement. Information Processing Letters, 25(1), 1987.","DOI":"10.1016\/0020-0190(87)90224-9"},{"key":"27_CR16","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C. A. R. Hoare","year":"1972","unstructured":"C. A. R. Hoare. Proof of Correctness of Data Representations. Acta Informatica, 1:271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"27_CR17","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"C. A. R. Hoare","year":"1993","unstructured":"C. A. R. Hoare, J. He, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701\u2013739, 1993.","journal-title":"Acta Informatica"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Samin Ishtiaq and Peter W. O\u2019Hearn. BI as an assertion language for mutable data structures. In POPL. ACM Press, 2001.","DOI":"10.1145\/360204.375719"},{"key":"27_CR19","unstructured":"C. B. Jones. Software Development: A Rigorous Approach. Prentice-Hall, 1980."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"G. T. Leavens and W. E. Weihl. Specification and verification of object-oriented programas using supertype abstraction. Acta Informatica, 32, 1995.","DOI":"10.1007\/s002360050032"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota, pages 105\u2013106. ACM, October 2000.","DOI":"10.1145\/367845.367996"},{"key":"27_CR22","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/s002360050168","volume":"36","author":"G. T. Leavens","year":"2000","unstructured":"Gary T. Leavens and Don Pigozzi. A complete algebraic characterization of behavioral subtyping. Acta Informatica, 36:617\u2013663, 2000.","journal-title":"Acta Informatica"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"K.R.M Leino, A. Poetzsch-Heffter, and Y. Zhou. Using data groups to specify and check side effects. In Programming Language Design and Implementation 2002, 2002. To appear.","DOI":"10.1145\/512529.512559"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"B. H. Liskov and J. M. Wing. A Behavioural Notion of Subtyping. ACM Transactions on Programming Languages and Systems, 16(6), 1994.","DOI":"10.1145\/197320.197383"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Nancy Lynch and Frits Vaandrager. Forward and backward simulations part I: Untimed systems. Information and Computation, 121(2), 1995.","DOI":"10.1006\/inco.1995.1134"},{"key":"27_CR26","unstructured":"C. C. Morgan. Programming from Specifications. Prentice-Hall, 2nd edition, 1994."},{"issue":"6","key":"27_CR27","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/BF00277386","volume":"27","author":"C. C. Morgan","year":"1990","unstructured":"C. C. Morgan and P. H. B. Gardiner. Data Refinement by Calculation. Acta Informatica, 27(6):481\u2013503, 1990.","journal-title":"Acta Informatica"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"P. M\u00fcller. Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversit\u00e4t Hagen, 2001. Available from http:\/\/www.informatik.fernuni-hagen.de\/pi5\/publications.html .","DOI":"10.1007\/3-540-45651-1"},{"issue":"1\u20132","key":"27_CR29","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/S0304-3975(00)00339-X","volume":"278","author":"D. A. Naumann","year":"2002","unstructured":"David A. Naumann. Soundness of data refinement for a higher order imperative language. Theoretical Computer Science, 278(1\u20132):271\u2013301, 2002.","journal-title":"Theoretical Computer Science"},{"key":"27_CR30","unstructured":"Gordon Plotkin. Lambda definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence, 1973."},{"key":"27_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems (ESOP\u2019 99)","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"A. Poetzsch-Heffter and P. M\u00fcller. A programming logic for sequential Java. In S. D. Swierstra, editor, Programming Languages and Systems (ESOP\u2019 99), volume 1576 of Lecture Notes in Computer Science, pages 162\u2013176. Springer-Verlag, 1999."},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"John Power and Edmund Robinson. Logical relations and data abstraction. In Computer Science Logic, 2000.","DOI":"10.1007\/3-540-44622-2_34"},{"key":"27_CR33","unstructured":"U. S. Reddy. Objects and classes in Algol-like languages. In Fifth Intern. Workshop on Foundations of Object-oriented Languages, Jan 1998. Full version to appear in Information and Computation."},{"key":"27_CR34","unstructured":"John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millenial Perspectives in Computer Science. Palgrave, 2001."},{"key":"27_CR35","unstructured":"Clemens Szyperski. Component Software: Beyond Object-Oriented Programming. ACM Press Books. Addison-Wesley, 1999."},{"key":"27_CR36","unstructured":"R. D. Tennent. Correctness of data representations in Algol-like languages. In A. W. Roscoe, editor, A Classical Mind: Essays Dedicated to C A. R. Hoare. Prentice-Hall, 1994."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T11:09:34Z","timestamp":1737025774000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}