Advertisement

An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping

  • Gary T. LeavensEmail author
  • David A. Naumann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11174)

Abstract

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.

Keywords

Object-oriented programming Hoare-style verification JML specification language Behavioral subtyping Supertype abstraction Specification inheritance 

Notes

Acknowledgments

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.

References

  1. 1.
    America, P.: Inheritance and subtyping in a parallel object-oriented language. In: Bézivin, J., Hullot, J.-M., Cointe, P., Lieberman, H. (eds.) ECOOP 1987. LNCS, vol. 276, pp. 234–242. Springer, Heidelberg (1987).  https://doi.org/10.1007/3-540-47891-4_22CrossRefGoogle Scholar
  2. 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
  3. 3.
    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–90. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0019440CrossRefGoogle Scholar
  4. 4.
    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-2CrossRefzbMATHGoogle Scholar
  5. 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
  6. 6.
    Cardelli, L.: A semantics of multiple inheritance. Inf. Comput. 76(2/3), 138–164 (1988)MathSciNetCrossRefGoogle Scholar
  7. 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. 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
  9. 9.
    Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19–31 (1967)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Guttag, J., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10(1), 27–52 (1978).  https://doi.org/10.1007/BF00260922MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, New York (1990)zbMATHGoogle Scholar
  12. 12.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580, 583 (1969). http://doi.acm.org/10.1145/363235.363259CrossRefGoogle Scholar
  13. 13.
    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–303. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-46428-X_20CrossRefGoogle Scholar
  14. 14.
    Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6, 308–320 (1964). See also Landin’s paper “A Lambda-Calculus Approach” in Advances in Programming and Non-Numerical Computation, L. Fox (ed.), Pergamon Press, Oxford, 1966CrossRefGoogle Scholar
  15. 15.
    Landin, P.J.: The next 700 programming languages. Commun. ACM 9(3), 157–166 (1966)CrossRefGoogle Scholar
  16. 16.
    Leavens, G.T.: JML’s rich, inherited specifications for behavioral subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 2–34. Springer, Heidelberg (2006).  https://doi.org/10.1007/11901433_2CrossRefGoogle Scholar
  17. 17.
    Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. TOPLAS 37(4), 13:1–13:88 (2015). https://doi.acm.org/10.1145/2766446CrossRefGoogle Scholar
  18. 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. 19.
    Leavens, G.T., et al.: JML Reference Manual, September 2009. http://www.jmlspecs.org
  20. 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
  21. 21.
    Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8), 705–778 (1995).  https://doi.org/10.1007/BF01178658MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994).  https://doi.org/10.1145/197320.197383CrossRefGoogle Scholar
  23. 23.
    Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New York (1988)Google Scholar
  24. 24.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)zbMATHGoogle Scholar
  25. 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
  26. 26.
    Sabry, A., Felleisen, M.: Reasoning about programs in continuation passing style. Lisp Symb. Comput. 6(3/4), 289–360 (1993)CrossRefGoogle Scholar
  27. 27.
    Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon Inc., Boston (1986)Google Scholar
  28. 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
  29. 29.
    Stoy, J.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, Cambridge (1977)zbMATHGoogle Scholar
  30. 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. 31.
    Strachey, C.: Fundamental concepts in programming languages. In: Notes International Summer School in Computer Programming (1967)Google Scholar
  32. 32.
    Wills, A.: Capsules and types in Fresco. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 59–76. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0057015CrossRefGoogle Scholar
  33. 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

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of Central FloridaOrlandoUSA
  2. 2.Stevens Institute of TechnologyHobokenUSA

Personalised recommendations