{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T18:16:41Z","timestamp":1780424201740,"version":"3.54.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030029272","type":"print"},{"value":"9783030029289","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02928-9_2","type":"book-chapter","created":{"date-parts":[[2018,11,12]],"date-time":"2018-11-12T08:01:38Z","timestamp":1542009698000},"page":"39-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3271-3921","authenticated-orcid":false,"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2243-2325","authenticated-orcid":false,"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,11,13]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-47891-4_22","volume-title":"ECOOP\u2019 87 European Conference on Object-Oriented Programming","author":"P America","year":"1987","unstructured":"America, P.: Inheritance and subtyping in a parallel object-oriented language. In: B\u00e9zivin, J., Hullot, J.-M., Cointe, P., Lieberman, H. (eds.) ECOOP 1987. LNCS, vol. 276, pp. 234\u2013242. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-47891-4_22"},{"key":"2_CR2","unstructured":"America, P.: A behavioural approach to subtyping in object-oriented programming languages. Technical report 443, Philips Research Laboratories, Nederlandse Philips Bedrijven B. V., April 1989. Revised from the January 1989 version"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/BFb0019440","volume-title":"Foundations of Object-Oriented Languages","author":"P America","year":"1991","unstructured":"America, P.: Designing an object-oriented programming language with behavioural subtyping. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX 1990. LNCS, vol. 489, pp. 60\u201390. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0019440"},{"key":"2_CR4","series-title":"Graduate Texts in Computer Science Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2714-2","volume-title":"Verification of Sequential and Concurrent Programs","author":"KR Apt","year":"1997","unstructured":"Apt, K.R., Olderog, E.: Verification of Sequential and Concurrent Programs. Graduate Texts in Computer Science Series, 2nd edn. Springer, New York (1997). https:\/\/doi.org\/10.1007\/978-1-4757-2714-2","edition":"2"},{"key":"2_CR5","unstructured":"Bao, Y.: Reasoning about frame properties in object-oriented programs. Technical report CS-TR-17-05, Computer Science, University of Central Florida, Orlando, Florida, December 2017. https:\/\/goo.gl\/WZGMiB , the author\u2019s dissertation"},{"issue":"2\/3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1016\/0890-5401(88)90007-7","volume":"76","author":"L Cardelli","year":"1988","unstructured":"Cardelli, L.: A semantics of multiple inheritance. Inf. Comput. 76(2\/3), 138\u2013164 (1988)","journal-title":"Inf. Comput."},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pp. 258\u2013267. IEEE Computer Society Press, Los Alamitos, March 1996. https:\/\/doi.org\/10.1109\/ICSE.1996.493421 , a corrected version is ISU CS TR #95-20c, http:\/\/tinyurl.com\/s2krg","DOI":"10.1109\/ICSE.1996.493421"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: OOPSLA 2001 Conference Proceedings of Object-Oriented Programming, Systems, Languages, and Applications, 14\u201318 October 2001, Tampa Bay, Florida, USA, pp. 1\u201315. ACM, New York, October 2001","DOI":"10.1145\/504311.504283"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19\u201331 (1967)","journal-title":"Proc. Symp. Appl. Math."},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J Guttag","year":"1978","unstructured":"Guttag, J., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10(1), 27\u201352 (1978). https:\/\/doi.org\/10.1007\/BF00260922","journal-title":"Acta Informatica"},{"key":"2_CR11","volume-title":"The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics","author":"M Hennessy","year":"1990","unstructured":"Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, New York (1990)"},{"issue":"10","key":"2_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580, 583 (1969). http:\/\/doi.acm.org\/10.1145\/363235.363259","journal-title":"Communications of the ACM"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284\u2013303. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46428-X_20"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"PJ Landin","year":"1964","unstructured":"Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6, 308\u2013320 (1964). See also Landin\u2019s paper \u201cA Lambda-Calculus Approach\u201d in Advances in Programming and Non-Numerical Computation, L. Fox (ed.), Pergamon Press, Oxford, 1966","journal-title":"Comput. J."},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/365230.365257","volume":"9","author":"PJ Landin","year":"1966","unstructured":"Landin, P.J.: The next 700 programming languages. Commun. ACM 9(3), 157\u2013166 (1966)","journal-title":"Commun. ACM"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11901433_2","volume-title":"Formal Methods and Software Engineering","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T.: JML\u2019s rich, inherited specifications for behavioral subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 2\u201334. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_2"},{"issue":"4","key":"2_CR17","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/2766446","volume":"37","author":"GT Leavens","year":"2015","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. TOPLAS 37(4), 13:1\u201313:88 (2015). https:\/\/doi.acm.org\/10.1145\/2766446","journal-title":"TOPLAS"},{"key":"2_CR18","unstructured":"Leavens, G.T., Naumann, D.A., Rosenberg, S.: Preliminary definition of Core JML. CS Report 2006\u201307, Stevens Institute of Technology, September 2006. http:\/\/www.cs.stevens.edu\/~naumann\/publications\/SIT-TR-2006-07.pdf"},{"key":"2_CR19","unstructured":"Leavens, G.T., et al.: JML Reference Manual, September 2009. http:\/\/www.jmlspecs.org"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Leavens, G.T., Weihl, W.E.: Reasoning about object-oriented programs that use subtypes (extended abstract). In: Meyrowitz, N. (ed.) OOPSLA ECOOP 1990 Proceedings. ACM SIGPLAN Notices, vol. 25, no. 10, pp. 212\u2013223. ACM, October 1990. https:\/\/doi.org\/10.1145\/97945.97970","DOI":"10.1145\/97945.97970"},{"issue":"8","key":"2_CR21","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1007\/BF01178658","volume":"32","author":"GT Leavens","year":"1995","unstructured":"Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8), 705\u2013778 (1995). https:\/\/doi.org\/10.1007\/BF01178658","journal-title":"Acta Informatica"},{"issue":"6","key":"2_CR22","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994). https:\/\/doi.org\/10.1145\/197320.197383","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR23","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New York (1988)"},{"key":"2_CR24","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)","edition":"2"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Wadler, P. (ed.) ACM Symposium on Principles of Programming Languages, pp. 75\u201386. ACM, New York, January 2008","DOI":"10.1145\/1328438.1328451"},{"issue":"3\/4","key":"2_CR26","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01019462","volume":"6","author":"A Sabry","year":"1993","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation passing style. Lisp Symb. Comput. 6(3\/4), 289\u2013360 (1993)","journal-title":"Lisp Symb. Comput."},{"key":"2_CR27","volume-title":"Denotational Semantics: A Methodology for Language Development","author":"DA Schmidt","year":"1986","unstructured":"Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon Inc., Boston (1986)"},{"key":"2_CR28","unstructured":"Scott, D.S., Strachey, C.: Toward a mathematical semantics for computer languages. In: Proceedings Symposium on Computers and Automata. Microwave Institute Symposia Series, vol. 21, pp. 19\u201346. Polytechnic Institute of Brooklyn, New York (1971)"},{"key":"2_CR29","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"J Stoy","year":"1977","unstructured":"Stoy, J.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, Cambridge (1977)"},{"key":"2_CR30","unstructured":"Strachey, C.: Towards a formal semantics. In: IFIP TC2 Working Conference on Formal Language Description Languages for Computer Programming, pp. 198\u2013220. North-Holland, Amsterdam (1966)"},{"key":"2_CR31","unstructured":"Strachey, C.: Fundamental concepts in programming languages. In: Notes International Summer School in Computer Programming (1967)"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/BFb0057015","volume-title":"ECOOP\u201991 European Conference on Object-Oriented Programming","author":"A Wills","year":"1991","unstructured":"Wills, A.: Capsules and types in Fresco. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 59\u201376. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0057015"},{"key":"2_CR33","unstructured":"Wing, J.M.: A two-tiered approach to specifying programs. Technical report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science (1983)"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02928-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T14:09:06Z","timestamp":1572617346000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02928-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030029272","9783030029289"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02928-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.swu-rise.net.cn\/SETSS2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}