[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
My entry point to the "formalizing C++" litterature is Tahina Ramananandro's PhD thesis work, which does model (multiple) inheritance and casts, but focuses in particular on object initialization/destruction and object layout -- formalized in Coq. Mechanized Formal Semantics and Verified Compilation for C++ Objects Tahina Ramananandro, 2011 http://gallium.inria.fr/~tramanan/cpp/ It contains a nice "Related Work" section mention several earlier works on C++ inheritance and casts, and in particular builds upon Daniel Wasserab's 2010 thesis (formalized in Isabelle) and the corresponding conference article An operational semantics and type safety proof for multiple inheritance in C++ Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, and Frank Tip 2006 and Michael Norrish's more complete HOL formalization A Formal Semantics for C++ Michael Norrish. 2008 On Mon, Jun 26, 2017 at 10:51 AM, Yanlin Wang <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear all, > > > I am formalizing a C++-like multiple inheritance model, please look at this > piece of code: > > > //g++ 5.4.0#include <iostream>class Deck { public: virtual void > draw () { > std::cout << "Deck::draw" << std::endl; > } virtual void shuffleAndDraw () { > std::cout << "Deck::shuffle" << std::endl; draw(); > }};class LDeck : public Deck { public: > virtual void draw () { > std::cout << "L::draw" << std::endl; > }};class Paint { public: > virtual void draw () { > std::cout << "Paint::draw" << std::endl; > }};class Top : public LDeck, public Paint {};int main(){ Top b; > Top *a = &b; a->shuffleAndDraw();//shuffle and Ldraw a->Deck::draw(); > //draw a->Paint::draw();//paint ((Deck*)a)->draw();//LDraw > ((Paint*)a)->draw();//paint return 0;} > > > > > For resolving the method call “ ((Deck*)a)->draw()”, C++ uses both the static > (Deck) and dynamic(Top) type information of object a, so that the method call > “draw()” dispatches to LDeck::draw(). > > > I was wondering whether there are any formal models that describes this > method lookup mechanism in C++. If anyone knows, could you please let me > know? Thank you! > > > Best regards, > Yanlin Wang > > >
