{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T16:49:54Z","timestamp":1772729394053,"version":"3.50.1"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,8,13]],"date-time":"2015-08-13T00:00:00Z","timestamp":1439424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS 08-08913, CCF0916350, CCF0916715, CCF1017262, CNS1228695, CCF-0915611, and CNS-1228930"],"award-info":[{"award-number":["CNS 08-08913, CCF0916350, CCF0916715, CCF1017262, CNS1228695, CCF-0915611, and CNS-1228930"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2015,8,13]]},"abstract":"<jats:p>\n            Verification of a dynamically dispatched method call,\n            <jats:italic>E<\/jats:italic>\n            .\n            <jats:italic>m<\/jats:italic>\n            (), seems to depend on\n            <jats:italic>E<\/jats:italic>\n            \u2019s dynamic type. To avoid case analysis and allow incremental development, object-oriented program verification uses supertype abstraction. In other words, one reasons about\n            <jats:italic>E<\/jats:italic>\n            .\n            <jats:italic>m<\/jats:italic>\n            () using\n            <jats:italic>m<\/jats:italic>\n            \u2019s specification for\n            <jats:italic>E<\/jats:italic>\n            \u2019s static type. Supertype abstraction is valid when each subtype in the program is a behavioral subtype. This article semantically formalizes supertype abstraction and behavioral subtyping for a Java-like sequential language with mutation and proves that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. Specification inheritance, as in JML, is also formalized and proved to entail behavioral subtyping.\n          <\/jats:p>","DOI":"10.1145\/2766446","type":"journal-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T14:08:55Z","timestamp":1440425335000},"page":"1-88","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Behavioral Subtyping, Specification Inheritance, and Modular Reasoning"],"prefix":"10.1145","volume":"37","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[{"name":"University of Central Florida, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,8,13]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/646159.680017"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/34985.35007"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/648142.749839"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90037-I"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.002"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/551462"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/645870.668679"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101824"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2485981"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","volume-title":"Verified Software: Theories, Tools, Experiments","author":"Barnett Mike","unstructured":"Mike Barnett, Robert DeLine, Bart Jacobs, Manuel F\u00e4hndrich, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter. 2005a. The Spec# programming system: Challenges and directions. In Verified Software: Theories, Tools, Experiments. Lecture Notes in Computer Science, Vol. 4171. Springer, 144--152."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1808999"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_17"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040326"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.03.003"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/323648.323756"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90007-7"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/336431.336447"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Yoonsik Cheon Gary T. Leavens Murali Sitaraman and Stephen Edwards. 2005. Model variables: Cleanly supporting abstraction in design by contract. Software\u2014Practice and Experience 35 6 583--599. 10.1002\/spe.v35:6","DOI":"10.1002\/spe.v35:6"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328452"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1525579"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/227726.227772"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/550359"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_6"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.07.008"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.09.006"},{"key":"e_1_2_1_32_1","volume-title":"Eiffel: Analysis, Design, and Programming Language","author":"International ECMA","year":"2006","unstructured":"ECMA International. 2006. Eiffel: Analysis, Design, and Programming Language (2nd ed.). ECMA International, Rue du Rhone 114, CH-1204, Geneva. Available at http:\/\/www.ecma-international.org\/publications\/files\/ECMA-ST\/ECMA-367.pdf.","edition":"2"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504283"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503240"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803415"},{"key":"e_1_2_1_38_1","volume-title":"Programs, Recursion, and Unbounded Choice","author":"Hesselink Wim","unstructured":"Wim Hesselink. 1993. Programs, Recursion, and Unbounded Choice. Cambridge."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_2"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/336431.336448"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178658"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.10.015"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_9"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/62139.62141"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_55_1","volume-title":"Eiffel: A Langauge for Software Engineering. Technical Report TR-CS-85-19","author":"Meyer Bertrand","year":"1985","unstructured":"Bertrand Meyer. 1985. Eiffel: A Langauge for Software Engineering. Technical Report TR-CS-85-19. University of California, Santa Barbara, CA."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/184737"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46406-9"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00215-5"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_14"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.035"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/646155.679699"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498929"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/647541.730154"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90009-9"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328451"},{"key":"e_1_2_1_72_1","volume-title":"Proceedings of the ECOOP Workshop on Formal Techniques for Java-Like Programs.","author":"Pierik Cees","unstructured":"Cees Pierik and Frank S. de Boer. 2005a. On behavioral subtyping and completeness. In Proceedings of the ECOOP Workshop on Formal Techniques for Java-Like Programs."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.018"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/645393.651897"},{"key":"e_1_2_1_75_1","volume-title":"Carlo A. Furia, and Bertrand Meyer","author":"Polikarpova Nadia","year":"2014","unstructured":"Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer. 2014. Flexible invariants through semantic collaboration. In FM 2014: Formal Methods. Lecture Notes in Computer Science, Vol. 8442. Springer, 514--530."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80352-4"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45499-3"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.5555\/251167.251182"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.5555\/983087"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.5555\/647286.723237"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.5555\/647537.729693"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2766446","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2766446","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:20:59Z","timestamp":1750238459000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2766446"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,13]]},"references-count":76,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8,13]]}},"alternative-id":["10.1145\/2766446"],"URL":"https:\/\/doi.org\/10.1145\/2766446","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,13]]},"assertion":[{"value":"2013-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-08-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}