wfenv.abs

// This file defines environments and the well-formedness
// constraints upon them, and other interesting things
// like searching through class hierarchies for nearest
// fields/methods.


notation syntax rels ;
import syntax wf ;

reserve TE for :tyenv;
reserve C for :id;
reserve i for :id;


// Well formed environments 
//
// We do not force environments to be finite here.
//
// RANDOM NOTES
//
// old execution problem: Cadd, Vadd etc. are almost constructors, but
// are not 1-1 (though the side conditions in the rules ensure
// they are).  
//
// Hence we resort to a concrete model of declarations.
// 
// Fix suggested by David von Oheimb: Environment well-formedness does not
// depend on order of introduction at all in Java.  Hence scrap use of 
// inductive relation and just define as a set/unary relation.
//
// The rules below have been modified from those in the tech report.
// The two return-types-wider clauses demand a minimum behaviour
// from MSigsC and MSigsI: all super-methods must continue
// to be available at the new class/interface.



def wf_tyenv TE wf_tyenv <=>
 (?methods. Cdec(TE,Object) = SOME(CLASS(NONE,EMPTY,PEMPTY,methods)))  &
 (!C. C :: PDOM(FST(TE)) -->
  !Csupo Is fields methods. Cdec(TE,C) = SOME(CLASS(Csupo,Is,fields,methods)) -->

     (!Csup. Csupo = SOME(Csup) --> 
       (~(TE |- Csup subclass_of C))  &
       (!m at rt1.  MSigsC(TE,Csup)(m,MT(at,rt1)) -->
       (?rt2. MSigsC(TE,C)(m,MT(at,rt2)) &
          TE |- rt2 expty_widens_to rt1) )) &

     (Csupo = NONE --> (C = Object)  &
                       (fields = PEMPTY)  &
                       (Is = EMPTY) ) &

     (!m mt1. (m,mt1) :: methods -->
      !mt2. (m,mt2) :: methods -->
         (if (Args(mt1) = Args(mt2)) then (mt1 = mt2) else T) ) &

     (!i. i :: Is -->
      !m at rt1. MSigsI(TE,i)(m,MT(at,rt1)) -->
      (?rt2. MSigsC(TE,C)(m,MT(at,rt2)) &
             TE |- rt2 expty_widens_to rt1) ))
& 
  (!i Is methods.
     i :: PDOM(SND(TE)) &
     Idec(TE,i) = SOME(INTERFACE(Is,methods)) -->
     (!i'. i' :: Is --> 
          (~(TE |- i' subinterface_of i)) ) &

     (!m mt1. (m,mt1) :: methods -->
      !mt2. (m,mt2) :: methods  -->
         (if (Args(mt1) = Args(mt2)) then (mt1 = mt2) else T) ) &

     (!i'. i' :: Is -->
      !m at rt1. MSigsI(TE,i')(m,MT(at,rt1)) --> 
      (?rt2. MSigsI(TE,i)(m,MT(at,rt2)) & 
             TE |- rt2 expty_widens_to rt1) ) &

     (Is = EMPTY --> 
      !m at rt1. (m,MT(at,rt1)) :: methods -->
      !rt2. MSigsC(TE,Object)(m,MT(at,rt2)) -->
         (TE |- rt1 expty_widens_to rt2) ))



// Reflexivity results for widening relations.


lemma simpty_widens_to-refl [prolog,simp,auto]
  TE |- st1 simpty_widens_to st1

thm varty_widens_to-refl [prolog,simp,auto]
  TE |- vt1 varty_widens_to vt1

thm expty_widens_to-refl [prolog,simp,auto]
  TE |- et1 expty_widens_to et1



// Results about Object
//
// In a wfenv,  Object is only a subclass of Object


lemma Object-implements TE wf_tyenv --> ~(TE |- Object implements i);
lemma Object-subclass  TE wf_tyenv --> (TE |- Object subclass_of C <=> C = Object);
lemma Object-simpty 
      TE wf_tyenv --> (TE |- Class(Object) simpty_widens_to st <=> st = Class(Object));


// Transitivity results for widening relations.


lemma simpty_widens_to-trans
  TE wf_tyenv &
   TE |- vt1 simpty_widens_to vt2 & 
   TE |- vt2 simpty_widens_to vt3 -->
   TE |- vt1 simpty_widens_to vt3

thm varty_widens_to-trans
  TE wf_tyenv &
   TE |- vt1 varty_widens_to vt2 & 
   TE |- vt2 varty_widens_to vt3 -->
   TE |- vt1 varty_widens_to vt3

thm expty_widens_to-trans
  TE wf_tyenv &
   TE |- vt1 expty_widens_to vt2 & 
   TE |- vt2 expty_widens_to vt3 -->
   TE |- vt1 expty_widens_to vt3



// subtype lemmas follow, e.g. anything that widens to an array is an 
// array of the some simple type that widens to the simple type of the array.
//
// the proofs of these are all by straight forward case analysis using the rules
thm lemma">array-widens-lemma
  TE |- expty expty_widens_to SOME(VT(simpty0,dim)) &
   0 < dim 
   --> ?simpty1. 
        expty = SOME(VT(simpty1,dim)) &
        TE |- simpty1 simpty_widens_to simpty0

thm lemma">prim-widens-lemma 
  TE |- expty expty_widens_to SOME(VT(PrimT(primty),0))
   <=> expty = SOME(VT(PrimT(primty),0))

thm lemma">var-prim-widens-lemma 
  TE |- varty varty_widens_to VT(PrimT(primty),0)
   --> varty = VT(PrimT(primty),0)

thm lemma">class-widens-lemma 
  TE wf_tyenv &
   TE |- expty expty_widens_to SOME(VT(Class(C),0)) &
   C <> Object 
   --> ?C'. TE |- C' subclass_of C &
            expty = SOME(VT(Class(C'),0));


// a lemma that need not be exported:
lemma FDecs-finds-subclasses  
   FDecs(TE,C)((Cf,f),vt) --> TE |- C subclass_of Cf;

thm object-fields-unique 
   TE wf_tyenv & FDecs(TE,C)(fspec) & FDecs(TE,C)(fspec') 
   --> fspec = fspec';

thm object-fields-form-graph
  TE wf_tyenv --> IS_GRAPH {fspec | FDecs(TE,C)(fspec)};

thm FDecs-Object  
   TE wf_tyenv --> ~(x :: FDecs(TE,Object));


// subclasses inherit (or redeclare) methods from superclasses.
//
// This says that if we did a static search for the method from class C0,
// and got a result, then did the same from C1, then we get a method
// with a return type that is narrower.
lemma class-inherited-class-methods-are-narrower 
    TE wf_tyenv &
     TE |- C1 subclass_of C0 &
     MSigsC(TE,C0)(m,MT(AT,rt0))
     --> ?rt1. MSigsC(TE,C1)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0

lemma interface-inherited-interface-methods-are-narrower 
    TE wf_tyenv &
     TE |- i1 subinterface_of i0 &
     MSigsI(TE,i0)(m,MT(AT,rt0))
     --> ?rt1. MSigsI(TE,i1)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0

lemma class-inherited-interface-methods-are-narrower 
    TE wf_tyenv &
     TE |- C1 implements i1 &
     MSigsI(TE,i0)(m,MT(AT,rt0))
     --> ?rt1. MSigsC(TE,C2)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0

// all interfaces inherit (or redeclare with narrower type) methods from Object.
lemma interface-inherited-Object-methods-are-narrower
    TE wf_tyenv &
     TE |- i wellfounded_interface &
     MSigsC(TE,Object)(m,MT(AT,rt0))
     --> ?rt1. MSigsI(TE,i)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0

// all interfaces inherit (or redeclare with narrower type) methods from Object.
lemma array-inherited-Object-methods-are-identical  
    MSigsC(TE,Object)(m,MT(AT,rt0))
     --> MSigsA(TE)(m,MT(AT,rt0))




// subclasses inherit declared fields.  Should be strengthened to be up to widening,
// so array methods can be modelled correctly.
thm inherited-fields-exist
    TE wf_tyenv &
     TE |- C1 subclass_of C0 &
     ((C',f),var0_ty) :: FDecs(TE,C0) -->
     ((C',f),var0_ty) :: FDecs(TE,C1)

// The crucial theorem about visibility of methods under widening, for all reference types.
thm inherited-methods-exist
    TE wf_tyenv &
     MSigs(TE,vt0)(m,MT(AT,rt0)) &
     TE |- vt1 varty_widens_to vt0
     --> ?rt1. MSigs(TE,vt1)(m,MT(AT,rt1)) & TE |- rt1 expty_widens_to rt0