Reasoning about object-oriented programs that use subtypes

ABSTRACT

Programmers informally reason about object-oriented programs by using subtype relationships to classify the behavior of objects of different types and by letting supertypes stand for all their subtypes. We describe formal specification and verification techniques for such programs that mimic these informal ideas. Our techniques are modular and extend standard techniques for reasoning about programs that use abstract data types. Semantic restrictions on subtype relationships guarantee the soundness of these techniques.

REFERENCES

• Ame89: Pierre America. A behavioural approach to subtyping in object-oriented programming languages. Technical Report 443, Philips Research Laboratories, Nederlandse Philips Bedrijven B. V., January 1989.
• BDMN73: G.M. Birtwhistle , O.J. Dahl , B. Myhrhaug , K. Nygaard, Simula Begin, Chartwell-Bratt Ltd, 1979
• BHJL86: Andrew Black , Norman Hutchinson , Eric Jul , Henry Levy, Object structure in the Emerald system, Conference proceedings on Object-oriented programming systems, languages and applications, p.78-86, September 29-October 02, 1986, Portland, Oregon, United States
• BJ82: Dines Bjorner and Cliff B. Jones. Formal Specification and Software Development. Prentice-Hall International, London, 1982.
• BW87: Kim B. Bruce , Peter Wegner, An algebraic model of subtype and inheritance, Advances in database programming languages, ACM Press, New York, NY, 1990 [doi>10.1145/101620.101625]
• Car84: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• CW85: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• GH86a: J V Guttag , J J Horning, A Larch shared language handbook, Science of Computer Programming, v.6 n.2, p.135-157, March 1986
• GH86b: J V Guttag , J J Horning, Report on the Larch shared language, Science of Computer Programming, v.6 n.2, p.103-134, March 1986
• GM87: Joseph A. Goguen and Jose Meseguer. Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. Technical Report CSLI-87-92, Center for the Study of Language and Information, March 1987.
• Gog84: Joseph A. Goguen Parameterized programming.IEEE Transactions on Software Engineering,SE-10(5):528-543, September 1984.
• GR83: Adele Goldberg , David Robson, Smalltalk-80: the language and its implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• Gut80: John Guttag. Notes on type abstractions (version 2). IEEE Transactions on Software Engineering, SE-6(1):13-23, january 1980. Version 1 in Proceedings Specifications of Reliable Software, Cambridge, Mass., IEEE, April, 1979.
• Kee89: S. E. Keene, A programmer's guide to object-oriented programming in Common LISP, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• Lea89: Gary Todd Leavens. Verifying objectoriented programs that use subtypes. Technical Report 439, Massachusetts Institute of Technology, Laboratory for Computer Science, February 1989. The author's Ph.D. thesis.
• Lea90: Gary T. Leavens. Modular verification of object-oriented programs with subtypes. Technical Report 90-09, Department of Computer Science, Iowa State University, July 1990.
• Mey88: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• Mit86: John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• Rey80: John C. Reynolds, Using category theory to design implicit conversions and generic operators, Semantics-Directed Compiler Generation, Proceedings of a Workshop, p.211-258, January 14-18, 1980
• Rey85: J C Reynolds, Three approaches to type structure, Proc. of the international joint conference on theory and practice of software development (TAPSOFT) Berlin, March 25-29, 1985 on Mathematical foundations of software development, Vol. 1: Colloquium on trees in algebra and programming (CAAP'85), p.97-138, April 1985, Berlin, Germany
• Sny86: Alan Snyder, Encapsulation and inheritance in object-oriented programming languages, Conference proceedings on Object-oriented programming systems, languages and applications, p.38-45, September 29-October 02, 1986, Portland, Oregon, United States
• Sta85: R. Statman. Logical relations and the typed )~-calculus. Information and Control, 65(2/3):85-97, May/June 1985.
• WB89: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]
• Win83: J. M. Wing, A TWO-TIERED APPROACH TO SPECIFYING PROGRAMS, Massachusetts Institute of Technology, Cambridge, MA, 1983
• Win87: Jeannette M. Wing, Writing Larch interface language specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.1, p.1-24, Jan. 1987 [doi>10.1145/9758.10500]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Algorithms, Design, Languages, Verification