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

[Gabriel Scherer]

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 <huohuohuomumu at gmail.com> 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
>
>
>