Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Conform.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/J/Conform.thy
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

section \<open>Conformity Relations for Type Soundness Proof\<close>

theory Conform imports State WellType Exceptions begin

type_synonym 'c env' = "'c prog \ (vname \ ty)" \ \same as \env\ of \WellType.thy\\

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

definition conf :: "'c prog => aheap => val => ty => bool"
                                   ("_,_ \ _ ::\ _" [51,51,51,51] 50) where
"G,h\v::\T == \T'. typeof (map_option obj_ty o h) v = Some T' \ G\T'\T"

definition lconf :: "'c prog => aheap => ('a \ val) => ('a \ ty) => bool"
                                   ("_,_ \ _ [::\] _" [51,51,51,51] 50) where
"G,h\vs[::\]Ts == \n T. Ts n = Some T --> (\v. vs n = Some v \ G,h\v::\T)"

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

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

definition xconf :: "aheap \ val option \ bool" where
  "xconf hp vo == preallocated hp \ (\ v. (vo = Some v) \ (\ xc. v = (Addr (XcptRef xc))))"

definition conforms :: "xstate => java_mb env' => bool" ("_ ::\ _" [51,51] 50) where
"s::\E == prg E\h heap (store s) \ \
            prg E,heap (store s)\<turnstile>locals (store s)[::\<preceq>]localT E \<and>
            xconf (heap (store s)) (abrupt s)"

subsection "hext"

lemma hextI:
" \a C fs . h a = Some (C,fs) -->
      (\<exists>fs'. h' a = Some (C,fs')) ==> h\<le>|h'"
apply (unfold hext_def)
apply auto
done

lemma hext_objD: "[|h\|h'; h a = Some (C,fs) |] ==> \fs'. h' a = Some (C,fs')"
apply (unfold hext_def)
apply (force)
done

lemma hext_refl [simp]: "h\|h"
apply (rule hextI)
apply (fast)
done

lemma hext_new [simp]: "h a = None ==> h\|h(a\x)"
apply (rule hextI)
apply auto
done

lemma hext_trans: "[|h\|h'; h'\|h''|] ==> h\|h''"
apply (rule hextI)
apply (fast dest: hext_objD)
done

lemma hext_upd_obj: "h a = Some (C,fs) ==> h\|h(a\(C,fs'))"
apply (rule hextI)
apply auto
done

subsection "conf"

lemma conf_Null [simp]: "G,h\Null::\T = G\RefT NullT\T"
apply (unfold conf_def)
apply (simp (no_asm))
done

lemma conf_litval [rule_format (no_asm), simp]:
  "typeof (\v. None) v = Some T --> G,h\v::\T"
apply (unfold conf_def)
apply (rule val.induct)
apply auto
done

lemma conf_AddrI: "[|h a = Some obj; G\obj_ty obj\T|] ==> G,h\Addr a::\T"
apply (unfold conf_def)
apply (simp)
done

lemma conf_obj_AddrI: "[|h a = Some (C,fs); G\C\C D|] ==> G,h\Addr a::\ Class D"
apply (unfold conf_def)
apply (simp)
done

lemma defval_conf [rule_format (no_asm)]:
  "is_type G T --> G,h\default_val T::\T"
apply (unfold conf_def)
apply (rule_tac y = "T" in ty.exhaust)
apply  (erule ssubst)
apply  (rename_tac prim_ty, rule_tac y = "prim_ty" in prim_ty.exhaust)
apply    (auto simp add: widen.null)
done

lemma conf_upd_obj:
"h a = Some (C,fs) ==> (G,h(a\(C,fs'))\x::\T) = (G,h\x::\T)"
apply (unfold conf_def)
apply (rule val.induct)
apply auto
done

lemma conf_widen [rule_format (no_asm)]:
  "wf_prog wf_mb G ==> G,h\x::\T --> G\T\T' --> G,h\x::\T'"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto intro: widen_trans)
done

lemma conf_hext [rule_format (no_asm)]: "h\|h' ==> G,h\v::\T --> G,h'\v::\T"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto dest: hext_objD)
done

lemma new_locD: "[|h a = None; G,h\Addr t::\T|] ==> t\a"
apply (unfold conf_def)
apply auto
done

lemma conf_RefTD [rule_format]:
"G,h\a'::\RefT T \ a' = Null \
  (\<exists>a obj T'. a' = Addr a \<and>  h a = Some obj \<and>  obj_ty obj = T' \<and>  G\<turnstile>T'\<preceq>RefT T)"
unfolding conf_def by (induct a') auto

lemma conf_NullTD: "G,h\a'::\RefT NullT ==> a' = Null"
apply (drule conf_RefTD)
apply auto
done

lemma non_npD: "[|a' \ Null; G,h\a'::\RefT t|] ==>
  \<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t"
apply (drule conf_RefTD)
apply auto
done

lemma non_np_objD: "!!G. [|a' \ Null; G,h\a'::\ Class C|] ==>
  (\<exists>a C' fs. a' = Addr a \<and>  h a = Some (C',fs) \<and>  G\<turnstile>C'\<preceq>C C)"
apply (fast dest: non_npD)
done

lemma non_np_objD' [rule_format (no_asm)]:
  "a' \ Null ==> wf_prog wf_mb G ==> G,h\a'::\RefT t -->
  (\<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t)"
apply(rule_tac y = "t" in ref_ty.exhaust)
apply (fast dest: conf_NullTD)
apply (fast dest: non_np_objD)
done

lemma conf_list_gext_widen [rule_format (no_asm)]:
  "wf_prog wf_mb G ==> \Ts Ts'. list_all2 (conf G h) vs Ts -->
  list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'"
apply(induct_tac "vs")
apply(clarsimp)
apply(clarsimp)
apply(frule list_all2_lengthD [symmetric])
apply(simp (no_asm_use) add: length_Suc_conv)
apply(safe)
apply(frule list_all2_lengthD [symmetric])
apply(simp (no_asm_use) add: length_Suc_conv)
apply(clarify)
apply(fast elim: conf_widen)
done

subsection "lconf"

lemma lconfD: "[| G,h\vs[::\]Ts; Ts n = Some T |] ==> G,h\(the (vs n))::\T"
apply (unfold lconf_def)
apply (force)
done

lemma lconf_hext [elim]: "[| G,h\l[::\]L; h\|h' |] ==> G,h'\l[::\]L"
apply (unfold lconf_def)
apply  (fast elim: conf_hext)
done

lemma lconf_upd: "!!X. [| G,h\l[::\]lT;
  G,h\<turnstile>v::\<preceq>T; lT va = Some T |] ==> G,h\<turnstile>l(va\<mapsto>v)[::\<preceq>]lT"
apply (unfold lconf_def)
apply auto
done

lemma lconf_init_vars_lemma [rule_format (no_asm)]:
  "\x. P x --> R (dv x) x ==> (\x. map_of fs f = Some x --> P x) -->
  (\<forall>T. map_of fs f = Some T -->
  (\<exists>v. map_of (map (\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \<and>  R v T))"
apply( induct_tac "fs")
apply auto
done

lemma lconf_init_vars [intro!]:
"\n. \T. map_of fs n = Some T --> is_type G T ==> G,h\init_vars fs[::\]map_of fs"
apply (unfold lconf_def init_vars_def)
apply auto
apply( rule lconf_init_vars_lemma)
apply(   erule_tac [3] asm_rl)
apply(  intro strip)
apply(  erule defval_conf)
apply auto
done

lemma lconf_ext: "[|G,s\l[::\]L; G,s\v::\T|] ==> G,s\l(vn\v)[::\]L(vn\T)"
apply (unfold lconf_def)
apply auto
done

lemma lconf_ext_list [rule_format (no_asm)]:
  "G,h\l[::\]L ==> \vs Ts. distinct vns --> length Ts = length vns -->
  list_all2 (\<lambda>v T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
apply (unfold lconf_def)
apply( induct_tac "vns")
apply(  clarsimp)
apply( clarsimp)
apply( frule list_all2_lengthD)
apply( auto simp add: length_Suc_conv)
done

lemma lconf_restr: "\lT vn = None; G, h \ l [::\] lT(vn\T)\ \ G, h \ l [::\] lT"
apply (unfold lconf_def)
apply (intro strip)
apply (case_tac "n = vn")
apply auto
done

subsection "oconf"

lemma oconf_hext: "G,h\obj\ ==> h\|h' ==> G,h'\obj\"
apply (unfold oconf_def)
apply (fast)
done

lemma oconf_obj: "G,h\(C,fs)\ =
  (\<forall>T f. map_of(fields (G,C)) f = Some T --> (\<exists>v. fs f = Some v \<and>  G,h\<turnstile>v::\<preceq>T))"
apply (unfold oconf_def lconf_def)
apply auto
done

lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]

subsection "hconf"

lemma hconfD: "[|G\h h\; h a = Some obj|] ==> G,h\obj\"
apply (unfold hconf_def)
apply (fast)
done

lemma hconfI: "\a obj. h a=Some obj --> G,h\obj\ ==> G\h h\"
apply (unfold hconf_def)
apply (fast)
done

subsection "xconf"

lemma xconf_raise_if: "xconf h x \ xconf h (raise_if b xcn x)"
by (simp add: xconf_def raise_if_def)

subsection "conforms"

lemma conforms_heapD: "(x, (h, l))::\(G, lT) ==> G\h h\"
apply (unfold conforms_def)
apply (simp)
done

lemma conforms_localD: "(x, (h, l))::\(G, lT) ==> G,h\l[::\]lT"
apply (unfold conforms_def)
apply (simp)
done

lemma conforms_xcptD: "(x, (h, l))::\(G, lT) ==> xconf h x"
apply (unfold conforms_def)
apply (simp)
done

lemma conformsI: "[|G\h h\; G,h\l[::\]lT; xconf h x|] ==> (x, (h, l))::\(G, lT)"
apply (unfold conforms_def)
apply auto
done

lemma conforms_restr: "\lT vn = None; s ::\ (G, lT(vn\T)) \ \ s ::\ (G, lT)"
by (simp add: conforms_def, fast intro: lconf_restr)

lemma conforms_xcpt_change: "\ (x, (h,l))::\ (G, lT); xconf h x \ xconf h x' \ \ (x', (h,l))::\ (G, lT)"
by (simp add: conforms_def)

lemma preallocated_hext: "\ preallocated h; h\|h'\ \ preallocated h'"
by (simp add: preallocated_def hext_def)

lemma xconf_hext: "\ xconf h vo; h\|h'\ \ xconf h' vo"
by (simp add: xconf_def preallocated_def hext_def)

lemma conforms_hext: "[|(x,(h,l))::\(G,lT); h\|h'; G\h h'\ |]
  ==> (x,(h',l))::\(G,lT)"
by (fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)

lemma conforms_upd_obj:
  "[|(x,(h,l))::\(G, lT); G,h(a\obj)\obj\; h\|h(a\obj)|]
  ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)"
apply(rule conforms_hext)
apply  auto
apply(rule hconfI)
apply(drule conforms_heapD)
apply(auto elim: oconf_hext dest: hconfD)
done

lemma conforms_upd_local:
"[|(x,(h, l))::\(G, lT); G,h\v::\T; lT va = Some T|]
  ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"
apply (unfold conforms_def)
apply( auto elim: lconf_upd)
done

end

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.