Re: [TYPES] Any formal models of method lookup mechanism in C++?

[ 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
> >
> >
> >
>