Theory JTypeSafe

Up to index of Isabelle/HOL/MicroJava

(*  Title:      HOL/MicroJava/J/JTypeSafe.thy
    ID:         $Id: JTypeSafe.thy,v 1.1 1999/11/11 11:24:03 nipkow Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Type Safety of Java
*)

JTypeSafe = Eval + Conform

theorem NewC_conforms:

  [| h a = None; (h, l) ::<= (G, lT); wf_prog wf_mb G; is_class G C |]
  ==> (h(a|->(C, init_vars (fields (G, C)))), l) ::<= (G, lT)

theorem Cast_conf:

  [| wf_prog wf_mb G; G,h |- v ::<= Class C; G |- C <=? D; cast_ok G D h v |]
  ==> G,h |- v ::<= Class D

theorem FAcc_type_sound:

  [| wf_prog wf_mb G; field (G, C) fn = Some (fd, ft); (h, l) ::<= (G, lT);
     x' = None --> G,h |- a' ::<= Class C; np a' x' = None |]
  ==> G,h |- the (snd (the (h (the_Addr a'))) (fn, fd)) ::<= ft

theorem FAss_type_sound:

  [| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); (G, lT) |- v :: T';
     G |- T' <= ft; (G, lT) |- aa :: Class C; field (G, C) fn = Some (fd, ft);
     h'' <=| h'; x' = None --> G,h' |- a' ::<= Class C; h' <=| h;
     (h, l) ::<= (G, lT); G,h |- x ::<= T'; np a' x' = None |]
  ==> h'' <=| h(a|->(c, fs((fn, fd)|->x))) &
      (h(a|->(c, fs((fn, fd)|->x))), l) ::<= (G, lT) & G,h(a
      |->(c, fs((fn, fd)|->x))) |- x ::<= T'

theorem Call_lemma2:

  [| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;
     list_all2 (%T T'. G |- T <= T') pTs pTs'; wf_mhead G (mn, pTs') rT;
     length pTs' = length pns; nodups pns;
     Ball (set lvars) (split (%vn. is_type G)) |]
  ==> G,h |- init_vars lvars(pns[|->]pvs) [::<=] map_of lvars(pns[|->]pTs')

theorem Call_type_sound:

  [| wf_java_prog G; a' ~= Null; (h, l) ::<= (G, lT);
     max_spec G C (mn, pTsa) = {((mda, rTa), pTs')}; xc <=| xh; xh <=| h;
     list_all2 (conf G h) pvs pTsa;
     (md, rT, pns, lvars, blk, res) =
     the (method (G, fst (the (h (the_Addr a')))) (mn, pTs'));
     ALL lT.
        (h, init_vars lvars(pns[|->]pvs)(This|->a')) ::<= (G, lT) -->
        (G, lT) |- blk [ok] --> h <=| xi & (xi, xl) ::<= (G, lT);
     ALL lT.
        (xi, xl) ::<= (G, lT) -->
        (ALL T. (G, lT) |- res :: T -->
                xi <=| h' &
                (h', xj) ::<= (G, lT) & (x' = None --> G,h' |- v ::<= T));
     G,xh |- a' ::<= Class C |]
  ==> xc <=| h' & (h', l) ::<= (G, lT) & (x' = None --> G,h' |- v ::<= rTa)

theorem eval_evals_exec_type_sound:

  wf_java_prog G
  ==> (((x, h, l), e, v, x', h', l') : eval G -->
       (ALL lT.
           (h, l) ::<= (G, lT) -->
           (ALL T. (G, lT) |- e :: T -->
                   h <=| h' &
                   (h', l') ::<= (G, lT) & (x' = None --> G,h' |- v ::<= T)))) &
      (((x, h, l), es, vs, x', h', l') : evals G -->
       (ALL lT.
           (h, l) ::<= (G, lT) -->
           (ALL Ts.
               (G, lT) |- es [::] Ts -->
               h <=| h' &
               (h', l') ::<= (G, lT) &
               (x' = None --> list_all2 (conf G h') vs Ts)))) &
      (((x, h, l), c, x', h', l') : exec G -->
       (ALL lT.
           (h, l) ::<= (G, lT) -->
           (G, lT) |- c [ok] --> h <=| h' & (h', l') ::<= (G, lT)))

theorem eval_type_sound:

  [| G = fst E; wf_java_prog G; G |- (x, s) -e>v-> (x', s'); s ::<= E;
     E |- e :: T |]
  ==> s' ::<= E & (x' = None --> G,fst s' |- v ::<= T)

theorem exec_type_sound:

  [| G = fst E; wf_java_prog G; G |- (x, s) -s0-> (x', s'); s ::<= E;
     E |- s0 [ok] |]
  ==> s' ::<= E

theorem all_methods_understood:

  [| G = fst E; wf_java_prog G; G |- (x, s) -e>a'-> Norm s'; a' ~= Null; s ::<= E;
     E |- e :: Class C; method (G, C) sig ~= None |]
  ==> method (G, fst (the (fst s' (the_Addr a')))) sig ~= None