{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:19:57Z","timestamp":1737609597965,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665885"},{"type":"electronic","value":"9783540481188"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48118-4_26","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T01:30:57Z","timestamp":1195003857000},"page":"1439-1459","source":"Crossref","is-referenced-by-count":11,"title":["A weakest precondition semantics for an object-oriented language of refinement"],"prefix":"10.1007","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[]},{"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01215408","volume":"6","author":"P. America","year":"1994","unstructured":"Pierre America and Frank de Boer. Reasoning about dynamically evolving process structures. Formal Aspects of Computing, 6:269\u2013316, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Mart\u00edin Abadi and K. Rustan 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":"26_CR3","doi-asserted-by":"crossref","unstructured":"R. J. R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"26_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054286","volume-title":"Mathematics of Program Construction","author":"M. M. Bonsangue","year":"1998","unstructured":"Marcello M. Bonsangue, Joost N. Kok, and Kaisa Sere. An approach to object-orientation in action systems. In Johan Jeuring, ed., Mathematics of Program Construction, LNCS 1422, pages 68\u201395. Springer, 1998."},{"key":"26_CR5","first-page":"59","volume-title":"I Brazilian Workshop on Formal Methods","author":"P. Borba","year":"1998","unstructured":"Paulo Borba. Where are the laws of object-oriented programming? In I Brazilian Workshop on Formal Methods, pages 59\u201370, Porto Alegre, Brazil, 19th-21st October 1998."},{"key":"26_CR6","unstructured":"A. L. C. Cavalcanti and D. A. Naumann. A Weakest Precondition Semantics for an Object-oriented Language of Refinement-Extended Version. Available at http:\/\/www.di.ufpe.br\/~alcc"},{"issue":"1","key":"26_CR7","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"},{"issue":"1","key":"26_CR8","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0167-6423(97)00015-4","volume":"33","author":"A. L. C. Cavalcanti","year":"1999","unstructured":"A. L. C. Cavalcanti, A. Sampaio, and J. C. P. Woodcock. An inconsistency in procedures, parameters, and substitution in the refinement calculus. Science of Computer Programming, 33(1):87\u201396, 1999.","journal-title":"Science of Computer Programming"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare and J. He. Unifying Theories of Programming. Prentice Hall, 1998.","DOI":"10.1007\/BFb0002714"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare and J. He and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 25(2), 1987.","DOI":"10.1016\/0020-0190(87)90224-9"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Kevin Lano. Formal Object-Oriented Development. Springer, 1995.","DOI":"10.1007\/978-1-4471-3073-4"},{"key":"26_CR12","series-title":"Lect Notes Comput Sci","volume-title":"7th European Symposium on Programming","author":"K. Rustan","year":"1998","unstructured":"K. Rustan M. Leino. Recursive object types in a logic of object-oriented programming. In Chris Hankin, ed., 7th European Symposium on Programming, LNCS 1381. Springer, 1998."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Barbara H. Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6), 1994.","DOI":"10.1145\/197320.197383"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"A. Mikhajlova and E. Sekerinski, Class refinement and interface refinement in object-oriented programs.InProceedings of FME\u201997: Industrial Benefit of Formal Methods. Springer, 1997.","DOI":"10.1007\/3-540-63533-5_5"},{"key":"26_CR15","unstructured":"Carroll Morgan. Programming from Specifications, 2ed. Prentice Hall, 1994."},{"key":"26_CR16","unstructured":"David A. Naumann. Validity of data re nement for a higher order imperative language. Submitted."},{"key":"26_CR17","unstructured":"David A. Naumann. Predicate transformer semantics of a higher order imperative language with record subtypes. Science of Computer Programming, 1998. To appear."},{"key":"26_CR18","unstructured":"U. S. Reddy. Objects and classes in Algol-like languages. In Fifth Intern. Workshop on Foundations of Object-oriented Languages. URL: http:\/\/pauillac.inria.fr\/ remy\/fool\/proceedings.html , Jan 1998."}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48118-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T09:08:56Z","timestamp":1737536936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48118-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665885","9783540481188"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48118-4_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}