[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Don't know if it's helpful, but here's another reference... --Mitch Jonathan~G. Rossie, Daniel~P. Friedman, and Mitchell Wand. Modeling Subobject-based Inheritance. In Pierre Cointe, editor, *Proc. European Conference on Object-Oriented Programming*, volume 1098 of *Lecture Notes in Computer Science*, pages 248--274, Berlin, Heidelberg, and New York, July 1996. Springer-Verlag. On Mon, Jun 26, 2017 at 1:51 PM, Gabriel Scherer <[email protected]> wrote: > [ 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 > > > > > > >
