Semantik der Mehrfachvererbung in C++

Objective

One of the main sources of complexity in C++ is a complex form of multiple inheritance, in which a combination of shared ("virtual") and repeated ("nonvirtual") inheritance is permitted. Because of this complexity, the behavior of operations on C++ class hierarchies has traditionally been defined informally, and in terms of implementation-level constructs such as v-tables.

We provide a formal treatment of the semantics of C++, focusing on the way it uses multiple inheritance. The formalisation was realised and machine checked in the theorem prover Isabelle/HOL, and we were able to prove the type safety of this formalisation. The type safety property that we prove is the fact that the execution of a well-typed, terminating program will deliver a result of the expected type, or end with an exception.

The Language

The CoreC++ language presented here features all the essential elements of the C++ multiple inheritance model (while omitting many features not relevant to operations involving class hierarchies). The semantics of CoreC++ were designed to mirror those of C++ to the maximum extent possible.

The theories are formalised in the theorem prover Isabelle/HOL and can be found in the Archive of Formal Proofs.

Executing the Semantics

Isabelle enables one to automatically create ML files from theories ("rapid prototyping") by using its built-in code generator. We have done so for the semantics and the type system. A C++ program can then be formulated in ML as well. By executing these files with an ML interpreter (e.g. PolyML) one can check if the program can be typed and if so, with which type, and what result executing the semantics on the programs will return---i.e. if the semantics does what it should, compared to the C++ standard.

Projektbeteiligte

Lehrstuhlinhaber
Prof. Gregor Snelting

Ehemalige Mitarbeiter
Dr.-Ing. Daniel Wasserrab

Veröffentlichungen

2007
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip: C++ ist typsicher? Garantiert!. SE 2007
2006
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip: An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++. OOPSLA 2006
D. Wasserrab: CoreC++. AFP 2006
2005
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip: An Operational Semantics and Type Safety Proof for C++-like Multiple Inheritance.