Theory Conform

Up to index of Isabelle/HOL/MicroJava

(*  Title:      HOL/MicroJava/J/Conform.thy
    ID:         $Id: Conform.thy,v 1.6 2000/09/22 14:28:53 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Conformity relations for type safety of Java
*)

Conform = State + WellType +

types   'c env_ = "'c prog × (vname \<leadsto> ty)" (* same as env of WellType.thy *)

constdefs

  hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50)
 "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"

  conf :: "'c prog => aheap => val => ty => bool"       ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
 "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"

  lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
                                                ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
 "G,h\<turnstile>vs[::\<preceq>]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h\<turnstile>v::\<preceq>T)"

  oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
 "G,h\<turnstile>obj\<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))"

  hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50)
 "G\<turnstile>h h\<surd>    == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj\<surd>"

  conforms :: "state => java_mb env_ => bool"   ("_ ::\<preceq> _" [51,51] 50)
 "s::\<preceq>E == prg E\<turnstile>h heap s\<surd> \<and> prg E,heap s\<turnstile>locals s[::\<preceq>]localT E"


syntax (HTML)
  hext     :: "aheap => aheap => bool"
              ("_ <=| _" [51,51] 50)

  conf     :: "'c prog => aheap => val => ty => bool"
              ("_,_ |- _ ::<= _"  [51,51,51,51] 50)

  lconf    :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
              ("_,_ |- _ [::<=] _" [51,51,51,51] 50)

  oconf    :: "'c prog => aheap => obj => bool"
              ("_,_ |- _ [ok]" [51,51,51] 50)

  hconf    :: "'c prog => aheap => bool"
              ("_ |-h _ [ok]" [51,51] 50)

  conforms :: "state => java_mb env_ => bool"
              ("_ ::<= _" [51,51] 50)

end

hext

conf

theorem conf_VoidI:

  G,s |- Unit ::<= PrimT Void

theorem conf_BooleanI:

  G,s |- Bool b ::<= PrimT Boolean

theorem conf_IntegerI:

  G,s |- Intg i ::<= PrimT Integer

theorem defval_conf:

  is_type G T ==> G,h |- default_val T ::<= T

theorem conf_widen:

  [| wf_prog wf_mb G; G,h |- x ::<= T; G |- T <= T' |] ==> G,h |- x ::<= T'

theorem conf_hext:

  [| h <=| h'; G,h |- xa ::<= x |] ==> G,h' |- xa ::<= x

theorem conf_RefTD:

  G,h |- a' ::<= RefT T
  ==> a' = Null |
      (EX a obj T'.
          a' = Addr a & h a = Some obj & obj_ty obj = T' & G |- T' <= RefT T)

theorem non_np_objD':

  [| a' ~= Null; wf_prog wf_mb G; G,h |- a' ::<= RefT t;
     ALL C. t = ClassT C --> C ~= Object |]
  ==> EX a C fs. a' = Addr a & h a = Some (C, fs) & G |- Class C <= RefT t

theorem conf_list_gext_widen:

  [| wf_prog wf_mb G; list_all2 (conf G h) vs Ts;
     list_all2 (%T T'. G |- T <= T') Ts Ts' |]
  ==> list_all2 (conf G h) vs Ts'

lconf

theorem lconf_upd:

  [| G,h |- l [::<=] lT; G,h |- v ::<= T; lT va = Some T |]
  ==> G,h |- l(va|->v) [::<=] lT

theorem lconf_init_vars_lemma:

  [| ALL x. P x --> R (dv x) x; ALL x. map_of fs f = Some x --> P x;
     map_of fs f = Some T |]
  ==> EX v. map_of (map (%(f, ft). (f, dv ft)) fs) f = Some v & R v T

theorem lconf_init_vars:

  ALL n T. map_of fs n = Some T --> is_type G T
  ==> G,h |- init_vars fs [::<=] map_of fs

theorem lconf_ext_list:

  [| G,h |- l [::<=] L; nodups vns; length Ts = length vns;
     list_all2 (conf G h) vs Ts |]
  ==> G,h |- l(vns[|->]vs) [::<=] L(vns[|->]Ts)

oconf

hconf

theorem hconfD:

  [| G |-h h [ok]; h a = Some obj |] ==> G,h |- obj [ok]

theorem hconfI:

  ALL a obj. h a = Some obj --> G,h |- obj [ok] ==> G |-h h [ok]

conforms

theorem conforms_hext:

  [| (h, l) ::<= (G, lT); h <=| h'; G |-h h' [ok] |] ==> (h', l) ::<= (G, lT)

theorem conforms_upd_obj:

  [| (h, l) ::<= (G, lT); G,h(a|->obj) |- obj [ok]; h <=| h(a|->obj) |]
  ==> (h(a|->obj), l) ::<= (G, lT)

theorem conforms_upd_local:

  [| (h, l) ::<= (G, lT); G,h |- v ::<= T; lT va = Some T |]
  ==> (h, l(va|->v)) ::<= (G, lT)