Quelle Typing_Framework_JVM.thy Sprache: Isabelle

(*  Title:      HOL/MicroJava/BV/Typing_Framework_JVM.thy
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

section \<open>The Typing Framework for the JVM \label{sec:JVM}\<close>

theory Typing_Framework_JVM
imports "../DFA/Abstract_BV" JVMType EffectMono BVSpec
begin

definition exec :: "jvm_prog \ nat \ ty \ exception_table \ instr list \ JVMType.state step_type" where
  "exec G maxs rT et bs ==
  err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"

definition opt_states :: "'c prog \ nat \ nat \ (ty list \ ty err list) option set" where
  "opt_states G maxs maxr \ opt (\{list n (types G) |n. n \ maxs} \ list maxr (err (types G)))"

subsection \<open>Executability of \<^term>\<open>check_bounded\<close>\<close>

primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
where
  "list_all'_rec P n [] = True"
| "list_all'_rec P n (x#xs) = (P x n \ list_all'_rec P (Suc n) xs)"

definition list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  "list_all' P xs \ list_all'_rec P 0 xs"

lemma list_all'_rec:
  "list_all'_rec P n xs = (\p < size xs. P (xs!p) (p+n))"
  apply (induct xs arbitrary: n)
  apply auto
  apply (case_tac p)
  apply auto
  done

lemma list_all' [iff]:
  "list_all' P xs = (\n < size xs. P (xs!n) n)"
  by (unfold list_all'_def) (simp add: list_all'_rec)

lemma [code]:
  "check_bounded ins et =
  (list_all' (\i pc. list_all (\pc'. pc' < length ins) (succs i pc)) ins \
   list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
  by (simp add: list_all_iff check_bounded_def)


subsection \<open>Connecting JVM and Framework\<close>

lemma check_bounded_is_bounded:
  "check_bounded ins et \ bounded (\pc. eff (ins!pc) G pc et) (length ins)"
  by (unfold bounded_def) (blast dest: check_boundedD)

lemma special_ex_swap_lemma [iff]:
  "(\X. (\n. X = A n \ P n) & Q X) = (\n. Q(A n) \ P n)"
  by blast

lemmas [iff del] = not_None_eq

theorem exec_pres_type:
  "wf_prog wf_mb S \
  pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
  apply (unfold exec_def JVM_states_unfold)
  apply (rule pres_type_lift)
  apply clarify
  apply (case_tac s)
   apply simp
   apply (drule effNone)
   apply simp
  apply (simp add: eff_def xcpt_eff_def norm_eff_def)
  apply (case_tac "bs!p")

  apply clarsimp
  apply (drule listE_nth_in, assumption)
  apply fastforce

  apply (fastforce simp add: not_None_eq)

  apply (fastforce simp add: not_None_eq typeof_empty_is_type)

  apply clarsimp
  apply (erule disjE)
   apply fastforce
  apply clarsimp
  apply (rule_tac x="1" in exI)
  apply fastforce

  apply clarsimp
  apply (erule disjE)
   apply (fastforce dest: field_fields fields_is_type)
  apply (simp add: match_some_entry image_iff)
  apply (rule_tac x=1 in exI)
  apply fastforce

  apply clarsimp
  apply (erule disjE)
   apply fastforce
  apply (simp add: match_some_entry image_iff)
  apply (rule_tac x=1 in exI)
  apply fastforce

  apply clarsimp
  apply (erule disjE)
   apply fastforce
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastforce

  defer

  apply fastforce
  apply fastforce

  apply clarsimp
  apply (rule_tac x="n'+2" in exI)
  apply simp

  apply clarsimp
  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
  apply simp

  apply clarsimp
  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)
  apply simp

  apply fastforce
  apply fastforce
  apply fastforce
  apply fastforce

  apply clarsimp
  apply (erule disjE)
   apply fastforce
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastforce

  apply (erule disjE)
   apply clarsimp
   apply (drule method_wf_mdecl, assumption+)
   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
   apply fastforce
  apply clarsimp
  apply (rule_tac x=1 in exI)
  apply fastforce
  done

lemmas [iff] = not_None_eq

lemma sup_state_opt_unfold:
  "sup_state_opt G \ Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
  by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)

lemma app_mono:
  "app_mono (sup_state_opt G) (\pc. app (bs!pc) G maxs rT pc et) (length bs) (opt_states G maxs maxr)"
  by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)


lemma list_appendI:
  "\a \ list x A; b \ list y A\ \ a @ b \ list (x+y) A"
  apply (unfold list_def)
  apply (simp (no_asm))
  apply blast
  done

lemma list_map [simp]:
  "(map f xs \ list (length xs) A) = (f ` set xs \ A)"
  apply (unfold list_def)
  apply simp
  done

lemma [iff]:
  "(OK ` A \ err B) = (A \ B)"
  apply (unfold err_def)
  apply blast
  done

lemma [intro]:
  "x \ A \ replicate n x \ list n A"
  by (induct n, auto)

lemma lesubstep_type_simple:
  "a <=[Product.le (=) r] b \ a \|r| b"
  apply (unfold lesubstep_type_def)
  apply clarify
  apply (simp add: set_conv_nth)
  apply clarify
  apply (drule le_listD, assumption)
  apply (clarsimp simp add: lesub_def Product.le_def)
  apply (rule exI)
  apply (rule conjI)
   apply (rule exI)
   apply (rule conjI)
    apply (rule sym)
    apply assumption
   apply assumption
  apply assumption
  done


lemma eff_mono:
  "\p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\
  \<Longrightarrow> eff (bs!p) G p et s \<le>|sup_state_opt G| eff (bs!p) G p et t"
  apply (unfold eff_def)
  apply (rule lesubstep_type_simple)
  apply (rule le_list_appendI)
   apply (simp add: norm_eff_def)
   apply (rule le_listI)
    apply simp
   apply simp
   apply (simp add: lesub_def)
   apply (case_tac s)
    apply simp
   apply (simp del: split_paired_All split_paired_Ex)
   apply (elim exE conjE)
   apply simp
   apply (drule eff'_mono, assumption)
   apply assumption
  apply (simp add: xcpt_eff_def)
  apply (rule le_listI)
    apply simp
  apply simp
  apply (simp add: lesub_def)
  apply (case_tac s)
   apply simp
  apply simp
  apply (case_tac t)
   apply simp
  apply (clarsimp simp add: sup_state_conv)
  done

lemma order_sup_state_opt:
  "ws_prog G \ order (sup_state_opt G)"
  by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)

theorem exec_mono:
  "ws_prog G \ bounded (exec G maxs rT et bs) (size bs) \
  mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"
  apply (unfold exec_def JVM_le_unfold JVM_states_unfold)
  apply (rule mono_lift)
     apply (fold sup_state_opt_unfold opt_states_def)
     apply (erule order_sup_state_opt)
    apply (rule app_mono)
   apply assumption
  apply clarify
  apply (rule eff_mono)
  apply assumption+
  done

theorem semilat_JVM_slI:
  "ws_prog G \ semilat (JVMType.sl G maxs maxr)"
  apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
  apply (rule semilat_opt)
  apply (rule err_semilat_Product_esl)
  apply (rule err_semilat_upto_esl)
  apply (rule err_semilat_JType_esl, assumption+)
  apply (rule err_semilat_eslI)
  apply (rule Listn_sl)
  apply (rule err_semilat_JType_esl, assumption+)
  done

lemma sl_triple_conv:
  "JVMType.sl G maxs maxr ==
  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
  by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)

lemma is_type_pTs:
  "\ wf_prog wf_mb G; (C,S,fs,mdecls) \ set G; ((mn,pTs),rT,code) \ set mdecls \
  \<Longrightarrow> set pTs \<subseteq> types G"
proof
  assume "wf_prog wf_mb G"
         "(C,S,fs,mdecls) \ set G"
         "((mn,pTs),rT,code) \ set mdecls"
  hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
    by (rule wf_prog_wf_mdecl)
  hence "\t \ set pTs. is_type G t"
    by (unfold wf_mdecl_def wf_mhead_def) auto
  moreover
  fix t assume "t \ set pTs"
  ultimately
  have "is_type G t" by blast
  thus "t \ types G" ..
qed

lemma jvm_prog_lift:
  assumes wf:
  "wf_prog (\G C bd. P G C bd) G"

  assumes rule:
  "\wf_mb C mn pTs C rT maxs maxl b et bd.
   wf_prog wf_mb G \<Longrightarrow>
   method (G,C) (mn,pTs) = Some (C,rT,maxs,maxl,b,et) \<Longrightarrow>
   is_class G C \<Longrightarrow>
   set pTs \<subseteq> types G \<Longrightarrow>
   bd = ((mn,pTs),rT,maxs,maxl,b,et) \<Longrightarrow>
   P G C bd \<Longrightarrow>
   Q G C bd"

  shows
  "wf_prog (\G C bd. Q G C bd) G"
  using wf
  apply (unfold wf_prog_def wf_cdecl_def)
  apply clarsimp
  apply (drule bspec, assumption)
  apply (unfold wf_cdecl_mdecl_def)
  apply clarsimp
  apply (drule bspec, assumption)
  apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
  apply (frule is_type_pTs [OF wf], assumption+)
  apply clarify
  apply (drule rule [OF wf], assumption+)
  apply (rule HOL.refl)
  apply assumption+
  done

end

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.