An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping
Object-oriented (OO) programs, which use subtyping and dynamic dispatch, make specification and verification difficult because the code executed by a method call may dynamically be dispatched to an overriding method in any subtype, even ones that did not exist at the time the program was specified. Modular reasoning for such programs means allowing one to add new subtypes to a program without re-specifying and re-verifying it. In a 2015 ACM TOPLAS paper we presented a model-theoretic characterization of a Hoare-style modular verification technique for sequential OO programs called “supertype abstraction,” defined behavioral subtyping, and proved that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. The present paper is aimed at graduate students and other researchers interested in formal methods and gives a comprehensive overview of our prior work, along with the motivation and intuition for that work, with examples.
KeywordsObject-oriented programming Hoare-style verification JML specification language Behavioral subtyping Supertype abstraction Specification inheritance
Thanks to David Cok for comments on an earlier draft and for fixing some errors with the IntSet example. Thanks also to David for his work on the OpenJML tool (see http://www.openjml.org/) and his help with using it.
Notations. As an aid to the reader, we present a table of defined notations in Fig. 18 on the next page.
- 2.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 versionGoogle Scholar
- 5.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’s dissertation
- 7.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–267. 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
- 8.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–18 October 2001, Tampa Bay, Florida, USA, pp. 1–15. ACM, New York, October 2001Google Scholar
- 18.Leavens, G.T., Naumann, D.A., Rosenberg, S.: Preliminary definition of Core JML. CS Report 2006–07, Stevens Institute of Technology, September 2006. http://www.cs.stevens.edu/~naumann/publications/SIT-TR-2006-07.pdf
- 19.Leavens, G.T., et al.: JML Reference Manual, September 2009. http://www.jmlspecs.org
- 20.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–223. ACM, October 1990. https://doi.org/10.1145/97945.97970
- 23.Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New York (1988)Google Scholar
- 25.Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Wadler, P. (ed.) ACM Symposium on Principles of Programming Languages, pp. 75–86. ACM, New York, January 2008Google Scholar
- 27.Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon Inc., Boston (1986)Google Scholar
- 28.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–46. Polytechnic Institute of Brooklyn, New York (1971)Google Scholar
- 30.Strachey, C.: Towards a formal semantics. In: IFIP TC2 Working Conference on Formal Language Description Languages for Computer Programming, pp. 198–220. North-Holland, Amsterdam (1966)Google Scholar
- 31.Strachey, C.: Fundamental concepts in programming languages. In: Notes International Summer School in Computer Programming (1967)Google Scholar
- 33.Wing, J.M.: A two-tiered approach to specifying programs. Technical report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science (1983)Google Scholar