KIT | KIT-Bibliothek | Impressum | Datenschutz

An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++

Wasserrab, Daniel; Nipkow, Tobias; Snelting, Gregor; Tip, Frank

We present an operational semantics and type safety proof for multiple inheritance in C++.The semantics models the behavior 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 behavior 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++.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Jahr 2006
Sprache Englisch
Identifikator ISSN: 0362-1340
KITopen-ID: 1000017691
Erschienen in OOPSLA 2006 proceedings - 21st International Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 22 - 26, 2006, Portland, Oregon, USA
Verlag ACM, New York (NY)
Seiten 345 - 362
Serie SIGPLAN notices ; 41,10
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page