HOME | ENGLISH | IMPRESSUM | KIT

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

[wasserrab06oopsla]Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip, An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++, 21th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 345--362, ACM, Portland, Oregon, USA, October 2006.

Zusammenfassung

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

Download

  [PDF]   [DOI]

BibTeX

Institutsinterne Autoren

Lehrstuhlinhaber
Prof. Gregor Snelting
Ehemalige Mitarbeiter
Dr.-Ing. Daniel Wasserrab

Projekte

Projekt
CoreC++