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

Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip

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

pdf

Isabelle theories in the Archive of Formal Proofs

BibTeX:

@inproceedings{WasserrabNST-OOPSLA06,
author={Daniel Wasserrab and Tobias Nipkow and Gregor Snelting and Frank Tip},
title={An Operational Semantics and Type Safety Proof for Multiple Inheritance
in C++},
booktitle={OOPSLA '06: Object oriented programming, systems, languages, and applications},
publisher={ACM Press},year=2006}