Home

Module Dynamic

Require Import LibLists.
Require Import Cplusconcepts.
Require Import Coqlib.
Require Import Tactics.
Require Import LibMaps.
Require Import LibPos.
Load Param.


A class is dynamic if, and only if, one of the following conditions holds: This definition is common to both algorithms studied in POPL 2011, Section 6. Moreover, it is formalized in the C++ Standard (since 1999) as "to have a polymorphic behaviour". However, it plays no role in the correctness of conditions stated in Section 4 and proved in Section 5.

Section DYN.


Variable A : ATOM.t.

Variable hierarchy : PTree.t (Class.t A).

Inductive is_dynamic : ident -> Prop :=
| is_dynamic_virtual_methods : forall i c
  (H_i_c : hierarchy ! i = Some c)
  (H_methods : exists m, In m (Class.methods c) /\ Method.virtual m = true),
    is_dynamic i
| is_dynamic_direct_virtual_base : forall i c
  (H_i_c : hierarchy ! i = Some c)
  b
  (Hb : In (Class.Inheritance.Shared, b) (Class.super c)),
  is_dynamic i
| is_dynamic_base : forall i c
  (H_i_c : hierarchy ! i = Some c)
  h b
  (H_h_b : In (h, b) (Class.super c))
  (H_is_dynamic_b : is_dynamic b),
  is_dynamic i
.

Lemma is_dynamic_virtual_base : forall i b,
  is_virtual_base_of hierarchy b i ->
  is_dynamic i.
Proof.
  induction 1.
  eauto using is_dynamic_direct_virtual_base.
  eauto using is_dynamic_base.
Qed.

Lemma is_dynamic_path : forall to via from by
  (Hpath : path hierarchy to via from by)
  (H_dyn_to : is_dynamic to),
  is_dynamic from.
Proof.
  intros.
  generalize (path_path2 Hpath).
  clear Hpath.
  intro Hpath.
  revert H_dyn_to.
  induction Hpath ; intros ; eauto 10 using is_dynamic_base.
Qed.

Lemma method_dispatch_dynamic : forall ms cn ccn dh dp mh mp,
  method_dispatch hierarchy ms cn ccn dh dp mh mp ->
  is_dynamic cn.
Proof.
 inversion 1; subst.
 eapply is_dynamic_path.
 eassumption.
 eapply is_dynamic_virtual_methods.
 eassumption.
 generalize (Method.find_in H2).
 eauto.
Qed.

End DYN.