An operational semantics and type safety prooffor multiple inheritance in C++

ABSTRACT

We present an operational semantics and type safety proof for multiple inheritance in C++. The semantics models the behaviour of method calls, field accesses, and two forms of casts in C++ class hierarchies exactly, and the type safety proof was formalized and machine-checked in Isabelle/HOL. Our semantics enables one, for the first time, to understand the behaviour of operations on C++ class hierarchies without referring to implementation-level artifacts such as virtual function tables. Moreover, it can - as the semantics is executable - act as a reference for compilers, and it can form the basis for more advanced correctness proofs of, e.g., automated program transformations. The paper presents the semantics and type safety proof, and a discussion of the many subtleties that we encountered in modeling the intricate multiple inheritance model of C++.

REFERENCES

• 1: David Aspinall, Proof General: A Generic Tool for Proof Development, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.38-42, March 25-April 02, 2000
• 2: Isabelle Attali , Denis Caromel , Sidi Ould Ehmety, A natural semantics for Eiffel dynamic binding, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.6, p.711-729, Nov. 1996 [doi>10.1145/236114.236118]
• 3: Stefan Berghofer , Tobias Nipkow, Executing Higher Order Logic, Selected papers from the International Workshop on Types for Proofs and Programs, p.24-40, December 08-12, 2000
• 4: Gilad Bracha , William Cook, Mixin-based inheritance, Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, p.303-311, September 1990, Ottawa, Canada
• 5: V. Breazu-Tannen , C. A. Gunter , A. Scedrov, Computing with coercions, Proceedings of the 1990 ACM conference on LISP and functional programming, p.44-60, June 27-29, 1990, Nice, France [doi>10.1145/91556.91590]
• 6: Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
• 7: Luca Cardelli. Type systems. In The Computer Science and Engineering Handbook. 2 edition, 2004.
• 8: Sophia Drossopoulou and Susan Eisenbach. Java is type safe - probably. In Proc. of ECOOP'97, volume 1241 of Lect. Notes in Comp. Sci., pages 389--418, 1997.
• 9: Michale Hohmuth and Hendrik Tews. The semantics of C++ data types: Towards verifying low-level system components. In D. Basin and B. Wolff, editors, Theorem Proving in Higher Order Logics, Emerging Trends Proc., pages 127--144. Universität Freiburg, 2003. Tech. Rep. 187.
• 10: Paul Jolly, Sophia Drossopoulou, Christopher Anderson, and KlausOstermann. Simple dependent types: Concord. In Proc. of FTfJP'05, 2005.
• 11: Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006 [doi>10.1145/1146809.1146811]
• 12: Henry Lieberman, Using prototypical objects to implement shared behavior in object-oriented systems, Conference proceedings on Object-oriented programming systems, languages and applications, p.214-223, September 29-October 02, 1986, Portland, Oregon, United States
• 13: O. L. Madsen , B. Moller-Pedersen, Virtual classes: a powerful mechanism in object-oriented programming, Conference proceedings on Object-oriented programming systems, languages and applications, p.397-406, October 02-06, 1989, New Orleans, Louisiana, United States
• 14: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348--375, 1978.
• 15: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 16: Nathaniel Nystrom , Stephen Chong , Andrew C. Myers, Scalable extensibility via nested inheritance, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 17: Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. An overview of the Scala programming language. Technical Report IC/2004/64, école Polytechnique Fédérale de Lausanne, Lausanne, Switzerland, 2004. Available from scala.epfl.ch.
• 18: Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. A nominal theory of objects with dependent types. In Proc. of ECOOP'03.
• 19: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 20: G. Ramalingam , Harini Srinivasan, A member lookup algorithm for C++, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.18-30, June 16-18, 1997, Las Vegas, Nevada, United States
• 21: Jonathan G. Rossie, Jr. , Daniel P. Friedman, An algebraic semantics of subobjects, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.187-199, October 15-19, 1995, Austin, Texas, United States
• 22: Jonathan G. Rossie, Jr. , Daniel P. Friedman , Mitchell Wand, Modeling Subobject-based Inheritance, Proceedings of the 10th European Conference on Object-Oriented Programming, p.248-274, July 08-12, 1996
• 23: Adam Seligman. FACTS: A formal analysis for C++. Williams College, 1995. Undergraduate thesis.
• 24: Gregor Snelting , Frank Tip, Understanding class hierarchies using concept analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.3, p.540-582, May 2000 [doi>10.1145/353926.353940]
• 25: Gregor Snelting , Frank Tip, Semantics-Based Composition of Class Hierarchies, Proceedings of the 16th European Conference on Object-Oriented Programming, p.562-584, June 10-14, 2002
• 26: Mirko Streckenbach , Gregor Snelting, Refactoring class hierarchies with KABA, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 27: Bjarne Stroustrup. Multiple inheritance for C++. Computing Systems, 2(4), 1989.
• 28: Bjarne Stroustrup, The design and evolution of C++, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1995
• 29: Bjarne Stroustrup. The C++ Standard: Incorporating Technical Corrigendum No. 1. John Wiley, 2 edition, 2003.
• 30: Peter F. Sweeney , Michael Burke, Quantifying and evaluating the space overhead for alternative C++ memory layouts, Software—Practice & Experience, v.33 n.7, p.595-636, June 2003 [doi>10.1002/spe.519]
• 31: Peter F. Sweeney , Joseph (Yossi) Gil, Space and time-efficient memory layout for multiple inheritance, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.256-275, November 01-05, 1999, Denver, Colorado, United States
• 32: Ewan Tempero , Robert Biddle, Simulating multiple inheritance in Java, Journal of Systems and Software, v.55 n.1, p.87-100, Dec. 2000 [doi>10.1016/S0164-1212(00)00061-3]
• 33: Krishnaprasad Thirunarayan, Günter Kniesel, and Haripriyan Hampapuram. Simulating multiple inheritance and generics in Java. Computer Languages, 25:189--210, 1999.
• 34: Frank Tip , Peter F. Sweeney, Class hierarchy specialization, Acta Informatica, v.36 n.12, p.927-982, Jan. 2000 [doi>10.1007/PL00013298]
• 35: John Viega , Bill Tutt , Reimer Behrends, Automated Delegation is a Viable Alternative to Multiple Inheritance in Class Based Languages, University of Virginia, Charlottesville, VA, 1998
• 36: Charles Wallace, The semantics of the C++ programming language, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
• 37: Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, and Frank Tip. An Operational Semantics and Type Safety Proof for C++-like Multiple Inheritance. Technical Report RC23709, IBM, 2005.
• 38: Markus Wenzel. Isabelle/Isar - A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut für Informatik, Technische Universität München, 2002. http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.
• 39: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 40: Yoav Zibin and Joseph Gil. Two-dimensional bi-directional object layout. In Proc. of ECOOP'03, volume 3013 of Lect. Notes in Comp. Sci., pages 329--350, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Inheritance

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
C++, multiple inheritance, semantics, type safety