Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Engineering Trustworthy Software Systems (SETSS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11174))

Included in the following conference series:

  • 370 Accesses

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.

Leavens’s work was supported in part by the US National Science Foundation under grants CNS 08-08913 and CCF 1518789 and Naumann’s work was supported in part by the US NSF under grant CNS 1718713.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The size is not specified to decrease, since it can stay the same if the element being removed was not in the set in the pre-state.

  2. 2.

    Recall that a call such as is shorthand for in Java, thus substituting iset for in turns it into .

  3. 3.

    There still are some other details omitted, such as how declarations (e.g., of the variable ) are handled.

  4. 4.

    Note that the transformation must ensure that any variables declared are fresh.

  5. 5.

    If classes can be created or loaded at runtime, then CT would contain all the classes that might be available to the program at runtime.

  6. 6.

    In Java, and Smalltalk-80 and C#, the values of expressions may be references, but the parameter passing mechanism is call by value, since one cannot write a method that modifies variables passed as actual parameters, such as swap. However, the semantics of method calls would need to be different for a language like C++ where parameters can be declared to be passed by reference (using ).

References

  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_22

    Chapter  Google Scholar 

  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 version

    Google Scholar 

  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/BFb0019440

    Chapter  Google Scholar 

  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-2

    Book  MATH  Google 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

  6. Cardelli, L.: A semantics of multiple inheritance. Inf. Comput. 76(2/3), 138–164 (1988)

    Article  MathSciNet  Google Scholar 

  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 2001

    Google Scholar 

  9. Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19–31 (1967)

    Article  MathSciNet  Google Scholar 

  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/BF00260922

    Article  MathSciNet  MATH  Google Scholar 

  11. Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, New York (1990)

    MATH  Google Scholar 

  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.363259

    Article  Google Scholar 

  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_20

    Chapter  Google Scholar 

  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, 1966

    Article  Google Scholar 

  15. Landin, P.J.: The next 700 programming languages. Commun. ACM 9(3), 157–166 (1966)

    Article  Google Scholar 

  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_2

    Chapter  Google Scholar 

  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/2766446

    Article  Google 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

  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/BF01178658

    Article  MathSciNet  MATH  Google Scholar 

  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.197383

    Article  Google Scholar 

  23. Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New York (1988)

    Google Scholar 

  24. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)

    MATH  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 2008

    Google Scholar 

  26. Sabry, A., Felleisen, M.: Reasoning about programs in continuation passing style. Lisp Symb. Comput. 6(3/4), 289–360 (1993)

    Article  Google 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 

  29. Stoy, J.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, Cambridge (1977)

    MATH  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 

  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/BFb0057015

    Chapter  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 

Download references

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.

Author information

Authors and Affiliations

  1. University of Central Florida, Orlando, FL, 32816, USA

    Gary T. Leavens

  2. Stevens Institute of Technology, Hoboken, NJ, 07030, USA

    David A. Naumann

Authors
  1. Gary T. Leavens
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David A. Naumann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gary T. Leavens .

Editor information

Editors and Affiliations

  1. London South Bank University, London, UK

    Jonathan P. Bowen

  2. Southwest University, Chongqing, China

    Zhiming Liu

  3. Faculty of Computer and Information Science, Southwest University, Chongqing, China

    Zili Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Leavens, G.T., Naumann, D.A. (2018). An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping. In: Bowen, J., Liu, Z., Zhang, Z. (eds) Engineering Trustworthy Software Systems. SETSS 2017. Lecture Notes in Computer Science(), vol 11174. Springer, Cham. https://doi.org/10.1007/978-3-030-02928-9_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02928-9_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02927-2

  • Online ISBN: 978-3-030-02928-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation