{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T22:25:39Z","timestamp":1693866339356},"reference-count":51,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2001,9,1]],"date-time":"2001-09-01T00:00:00Z","timestamp":999302400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4337,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2001,9]]},"DOI":"10.1016\/s0167-6423(00)00005-8","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:55:58Z","timestamp":1027594558000},"page":"1-51","source":"Crossref","is-referenced-by-count":21,"title":["Predicate transformer semantics of a higher-order imperative language with record subtyping"],"prefix":"10.1016","volume":"41","author":[{"given":"David A.","family":"Naumann","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0167-6423(00)00005-8_BIB1","series-title":"A Theory of Objects","author":"Abadi","year":"1996"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB2","doi-asserted-by":"crossref","unstructured":"M. Abadi, K.R. Leino, A logic of object-oriented programs, in: M. Bidout, M. Hauchet (Eds.), Proc. TAPSOFT \u201997, Lecture Notes in Computer Science, Vol. 1214, Springer, Berlin, 1997. Expanded in DEC SRC Report 161.","DOI":"10.1007\/BFb0030634"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB3","series-title":"Operational semantics of a parallel object-oriented language, Proc. POPL \u201986","first-page":"194","author":"America","year":"1986"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB4","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF01215408","article-title":"Reasoning about dynamically evolving process structures","volume":"6","author":"America","year":"1994","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"10.1016\/S0167-6423(00)00005-8_BIB5","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","article-title":"Ten years of Hoare's logic, a survey, Part I","volume":"3","author":"Apt","year":"1981","journal-title":"ACM Trans. Prog. Lang. Systems"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB6","series-title":"Verification of Sequential and Concurrent Programs","author":"Apt","year":"1991"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB7","article-title":"Exploring summation and product operators in the refinement calculus","volume":"Vol. 957","author":"Back","year":"1995"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB8","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0167-6423(89)90002-6","article-title":"Calculating with pointers","volume":"12","author":"Bijlsma","year":"1989","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB9","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0020-0190(93)90098-T","article-title":"Calculating with procedure calls","volume":"46","author":"Bijlsma","year":"1993","journal-title":"Inform Process. Lett."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB10","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF00289144","article-title":"A sharp proof rule for procedures in wp semantics","volume":"26","author":"Bijlsma","year":"1989","journal-title":"Acta Inform."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB11","first-page":"301","volume":"Vol. 711","author":"Bonsangue","year":"1993"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB12","first-page":"68","article-title":"An approach to object-orientation in action systems","volume":"Vol. 1422","author":"Bonsangue","year":"1998"},{"issue":"3","key":"10.1016\/S0167-6423(00)00005-8_BIB13","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/203095.203096","article-title":"Covariance and contravariance: conflict without a cause","volume":"17","author":"Castagna","year":"1995","journal-title":"ACM Trans. Programming Language Systems"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB14","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","article-title":"Programming language constructs for which it is impossible to obtain good Hoare-like axioms","volume":"26","author":"Clarke","year":"1979","journal-title":"J. ACM"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB15","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1006\/inco.1994.1090","article-title":"A denotational model of inheritance and its correctnesss","volume":"114","author":"Cook","year":"1994","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB16","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF00264295","article-title":"A sound and relatively complete Hoare-logic for a language with higher type procedures","volume":"20","author":"Damm","year":"1983","journal-title":"Acta Inform"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB17","series-title":"Forcing behavioral subtyping through specification inheritance, Proc. 18th Int. Conf. on Software Engineering, Berlin, Germany","first-page":"258, ;267","author":"Dhara","year":"1996"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB18","series-title":"Predicate Calculus and Program Semantics","author":"Dijkstra","year":"1990"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB19","first-page":"3","article-title":"A lambda calculus of objects and method specialization","volume":"1","author":"Fisher","year":"1994","journal-title":"Nordic J. Comput."},{"issue":"3","key":"10.1016\/S0167-6423(00)00005-8_BIB20","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1002\/j.1096-9942.1995.tb00018.x","article-title":"The development of type systems for object-oriented languages","volume":"1","author":"Fisher","year":"1995","journal-title":"Theory Practice Object Systems"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB21","series-title":"Program Verification","author":"Francez","year":"1992"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB22","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0890-5401(89)90040-0","article-title":"Reasoning about procedures as parameters in the language L4","volume":"83","author":"German","year":"1989","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB23","series-title":"Programs, Recursion, and Unbounded Choice","author":"Hesselink","year":"1993"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB24","series-title":"Programming: the Derivation of Algorithms","author":"Kaldewaij","year":"1990"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB25","series-title":"Theoretical Aspects of Object-Oriented Programming","article-title":"Two semantic models of object-oriented languages","author":"Kamin","year":"1994"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB26","unstructured":"K. Lano, H. Haughton (Eds.), Object-Oriented Specification Case Studies, Prentice-Hall, Englewood Cliffs, NJ, 1994."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB27","doi-asserted-by":"crossref","unstructured":"G.T. Leavens, Verifying object-oriented programs that use subtypes, Tech. Rep. TR-439, MIT LFCS, February 1989. Ph.D. Thesis.","DOI":"10.21236\/ADA209118"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB28","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1007\/BF01178658","article-title":"Specification and verification of object-oriented programs using supertype abstraction","volume":"32","author":"Leavens","year":"1995","journal-title":"Acta Inform."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB29","unstructured":"C.E. Martin, Preordered categories and predicate transformers, Dissertation, Oxford University, 1991."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB30","series-title":"Class refinement and interface refinement in object-oriented programs, Proc. FME\u201997","author":"Mikhajlova","year":"1997"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB31","series-title":"Programming from Specifications","author":"Morgan","year":"1994"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB32","doi-asserted-by":"crossref","unstructured":"D.A. Naumann, On the essence of Oberon, in: J. Gutknecht (Ed.), Proc., Programming Languages and System Architectures, Lecture Notes in Computer Science, Vol. 782, Springer, Berlin, 1994.","DOI":"10.1007\/3-540-57840-4_39"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB33","series-title":"Programming Concepts, Methods and Calculi, IFIP Transactions A-56","first-page":"467","article-title":"Predicate transformer semantics of an Oberon-like language","author":"Naumann","year":"1994"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB34","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(94)00247-G","article-title":"Predicate transformers and higher order programs","volume":"150","author":"Naumann","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB35","doi-asserted-by":"crossref","unstructured":"D. A. Naumann, Soundness of data refinement for a higher order imperative language, Theoret. Comput. Sci., to appear.","DOI":"10.1016\/S0304-3975(00)00339-X"},{"issue":"4","key":"10.1016\/S0167-6423(00)00005-8_BIB36","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1017\/S0960129598002552","article-title":"A categorical model for higher order imperative programming","volume":"8","author":"Naumann","year":"1998","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB37","unstructured":"D. A. Naumann, Predicate transformer semantics of a higher order imperative language with record subtypes, Tech. Rep. 9801, Stevens Institute of Technology, 1998."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB38","series-title":"Programming Concepts and Methods","first-page":"346","article-title":"Towards squiggly refinement algebra","author":"Naumann","year":"1998"},{"issue":"3","key":"10.1016\/S0167-6423(00)00005-8_BIB39","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1145\/210346.210425","article-title":"Parametricity and local variables","volume":"42","author":"O'Hearn","year":"1995","journal-title":"J. ACM"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB40","series-title":"Algol-like Languages, Two volumes","author":"O'Hearn","year":"1997"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB41","article-title":"Hoare's logic for programs with procedures \u2014 what has been achieved?","volume":"Vol. 164","author":"Olderog","year":"1983"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB42","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0304-3975(84)90066-5","article-title":"Correctness of programs with Pascal-like procedures without global variables","volume":"30","author":"Olderog","year":"1984","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB43","series-title":"Reasoning about local variables with operationally-based logical relations, Proc. LICS \u201996","author":"Pitts","year":"1996"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB44","series-title":"The Craft of Programming","author":"Reynolds","year":"1981"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB45","unstructured":"J.C. Reynolds, The essence of Algol, in: J.W. de Bakker, J.C. van Vliet (Eds.), Algorithmic Languages, North-Holland, Amsterdam, 1981."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB46","doi-asserted-by":"crossref","unstructured":"K. Sieber, A partial correctness logic for procedures (in an Algol-like language), in: R. Parikh (Ed.), Proc. Logics of Programs, Lecture Notes in Computer Science, Vol. 193, Springer, Berlin, 1985.","DOI":"10.1007\/3-540-15648-8_25"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB47","unstructured":"K. Sieber, Full abstraction for the second order subset of an ALGOL-like language, Tech. Rep. A 04\/95, Universitat des Saarlandes, Saarbrucken, 1995."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB48","doi-asserted-by":"crossref","unstructured":"W. Stephan, A. Wolpers, A calculus for higher order procedures with global variables, in: A. Borzyszkowski, S. Sokolowski (Eds.), Proc. MFCS \u201993, Lecture Notes in Computer Science, Vol. 711, Springer, Berlin, 1993.","DOI":"10.1007\/3-540-57182-5_62"},{"key":"10.1016\/S0167-6423(00)00005-8_BIB49","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0890-5401(90)90045-J","article-title":"Semantical analysis of specification logic","volume":"85","author":"Tennant","year":"1990","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB50","unstructured":"R.D. Tennant, Correctness of data representations in Algol-like languages, in: A.W. Roscoe (Ed.), A Classical Mind: Essays Dedicated to C.A.R. Hoare, Prentice-Hall, Englewood Cliffs, NJ, 1994."},{"key":"10.1016\/S0167-6423(00)00005-8_BIB51","doi-asserted-by":"crossref","unstructured":"M. Utting, K. Robinson, Modular reasoning in an object-oriented refinement calculus, in: R.S. Bird, C.C. Morgan, J.C.P. Woodcock (Eds.), Mathematics of Program Construction, Lecture Notes in Computer Science, Vol. 669, Springer, Berlin, 1992.","DOI":"10.1007\/3-540-56625-2_22"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642300000058?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642300000058?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T04:44:01Z","timestamp":1578458641000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642300000058"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,9]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,9]]}},"alternative-id":["S0167642300000058"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(00)00005-8","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2001,9]]}}}