Quelle JVM.thy Sprache: Isabelle

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

section \<open>Kildall for the JVM \label{sec:JVM}\<close>

theory JVM
imports Typing_Framework_JVM
begin

definition kiljvm :: "jvm_prog \ nat \ nat \ ty \ exception_table \
             instr list \<Rightarrow> JVMType.state list \<Rightarrow> JVMType.state list" where
  "kiljvm G maxs maxr rT et bs ==
  kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"

definition wt_kil :: "jvm_prog \ cname \ ty list \ ty \ nat \ nat \
             exception_table \<Rightarrow> instr list \<Rightarrow> bool" where
  "wt_kil G C pTs rT mxs mxl et ins ==
   check_bounded ins et \<and> 0 < size ins \<and>
   (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
        start  = OK first#(replicate (size ins - 1) (OK None));
        result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
    in \<forall>n < size ins. result!n \<noteq> Err)"

definition wt_jvm_prog_kildall :: "jvm_prog \ bool" where
  "wt_jvm_prog_kildall G ==
  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"

theorem is_bcv_kiljvm:
  "\ wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \ \
      is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
             (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
  apply (unfold kiljvm_def sl_triple_conv)
  apply (rule is_bcv_kildall)
       apply (simp (no_asm) add: sl_triple_conv [symmetric])
       apply (force intro!: semilat_JVM_slI dest: wf_acyclic
         simp add: symmetric sl_triple_conv)
      apply (simp (no_asm) add: JVM_le_unfold)
      apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
                   dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
     apply (simp add: JVM_le_unfold)
    apply (erule exec_pres_type)
   apply assumption
  apply (drule wf_prog_ws_prog, erule exec_mono, assumption)
  done

lemma subset_replicate: "set (replicate n x) \ {x}"
  by (induct n) auto

lemma in_set_replicate:
  "x \ set (replicate n y) \ x = y"
proof -
  assume "x \ set (replicate n y)"
  also have "set (replicate n y) \ {y}" by (rule subset_replicate)
  finally have "x \ {y}" .
  thus ?thesis by simp
qed

theorem wt_kil_correct:
  assumes wf:  "wf_prog wf_mb G"
  assumes C:   "is_class G C"
  assumes pTs: "set pTs \ types G"

  assumes wtk: "wt_kil G C pTs rT maxs mxl et bs"

  shows "\phi. wt_method G C pTs rT maxs mxl bs et phi"
proof -
  let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                #(replicate (size bs - 1) (OK None))"

  from wtk obtain maxr r where
    bounded: "check_bounded bs et" and
    result:  "r = kiljvm G maxs maxr rT et bs ?start" and
    success: "\n < size bs. r!n \ Err" and
    instrs:  "0 < size bs" and
    maxr:    "maxr = Suc (length pTs + mxl)"
    by (unfold wt_kil_def) simp

  from bounded have "bounded (exec G maxs rT et bs) (size bs)"
    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
  with wf have bcv:
    "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
    (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
    by (rule is_bcv_kiljvm)

  from C pTs instrs maxr
  have "?start \ list (length bs) (states G maxs maxr)"
    apply (unfold JVM_states_unfold)
    apply (rule listI)
    apply (auto intro: list_appendI dest!: in_set_replicate)
    apply force
    done

  with bcv success result have
    "\ts\list (length bs) (states G maxs maxr).
         ?start <=[JVMType.le G maxs maxr] ts \<and>
         wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts"
    by (unfold is_bcv_def) auto
  then obtain phi' where
    phi': "phi' \<in> list (length bs) (states G maxs maxr)" and
    s: "?start <=[JVMType.le G maxs maxr] phi'" and
    w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
    by blast
  hence wt_err_step:
    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"
    by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)

  from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
    by (drule_tac p=0 in le_listD) (simp add: lesub_def)+

  from phi' have l: "size phi' = size bs" by simp
  with instrs w have "phi' ! 0 \ Err" by (unfold wt_step_def) simp
  with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
    by auto

  from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
  also from w have "phi' = map OK (map ok_val phi')"
    by (auto simp add: wt_step_def intro!: nth_equalityI)
  finally
  have check_types:
    "check_types G maxs maxr (map OK (map ok_val phi'))" .

  from l bounded
  have "bounded (\pc. eff (bs!pc) G pc et) (length phi')"
    by (simp add: exec_def check_bounded_is_bounded)
  hence bounded': "bounded (exec G maxs rT et bs) (length bs)"
    by (auto intro: bounded_lift simp add: exec_def l)
  with wt_err_step
  have "wt_app_eff (sup_state_opt G) (\pc. app (bs!pc) G maxs rT pc et)
                   (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)
  with instrs l le bounded bounded' check_types maxr
  have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
    apply (unfold wt_method_def wt_app_eff_def)
    apply simp
    apply (rule conjI)
     apply (unfold wt_start_def)
     apply (rule JVM_le_convert [THEN iffD1])
     apply (simp (no_asm) add: phi0)
    apply clarify
    apply (erule allE, erule impE, assumption)
    apply (elim conjE)
    apply (clarsimp simp add: lesub_def wt_instr_def)
    apply (simp add: exec_def)
    apply (drule bounded_err_stepD, assumption+)
    apply blast
    done

  thus ?thesis by blast
qed

theorem wt_kil_complete:
  assumes wf:  "wf_prog wf_mb G"
  assumes C:   "is_class G C"
  assumes pTs: "set pTs \ types G"

  assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi"

  shows "wt_kil G C pTs rT maxs mxl et bs"
proof -
  let ?mxr = "1+size pTs+mxl"

  from wtm obtain
    instrs:   "0 < length bs" and
    len:      "length phi = length bs" and
    bounded:  "check_bounded bs et" and
    ck_types: "check_types G maxs ?mxr (map OK phi)" and
    wt_start: "wt_start G C pTs mxl phi" and
    wt_ins:   "\pc. pc < length bs \
                    wt_instr (bs ! pc) G rT phi maxs (length bs) et pc"
    by (unfold wt_method_def) simp

  from ck_types len
  have istype_phi:
    "map OK phi \ list (length bs) (states G maxs (1+size pTs+mxl))"
    by (auto simp add: check_types_def intro!: listI)

  let ?eff  = "\pc. eff (bs!pc) G pc et"
  let ?app   = "\pc. app (bs!pc) G maxs rT pc et"

  from bounded
  have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)

  from wt_ins
  have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
    apply (unfold wt_app_eff_def wt_instr_def lesub_def)
    apply (simp (no_asm) only: len)
    apply blast
    done
  with bounded_exec
  have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
    by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len)
  hence wt_err:
    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
    by (unfold exec_def) (simp add: len)

  from wf bounded_exec
  have is_bcv:
    "is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs)
            (size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)"
    by (rule is_bcv_kiljvm)

  let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                #(replicate (size bs - 1) (OK None))"

  from C pTs instrs
  have start: "?start \ list (length bs) (states G maxs ?mxr)"
    apply (unfold JVM_states_unfold)
    apply (rule listI)
    apply (auto intro!: list_appendI dest!: in_set_replicate)
    apply force
    done

  let ?phi = "map OK phi"
  have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi"
  proof -
    from len instrs
    have "length ?start = length (map OK phi)" by simp
    moreover
    { fix n
      from wt_start
      have "G \ ok_val (?start!0) <=' phi!0"
        by (simp add: wt_start_def)
      moreover
      from instrs len
      have "0 < length phi" by simp
      ultimately
      have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)"
        by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
      moreover
      { fix n'
        have "JVMType.le G maxs ?mxr (OK None) (?phi!n)"
          by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
            split: err.splits)
        hence "\ n = Suc n'; n < length ?start \
          \<Longrightarrow> JVMType.le G maxs ?mxr (?start!n) (?phi!n)"
          by simp
      }
      ultimately
      have "n < length ?start \ (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)"
        by (unfold lesub_def) (cases n, blast+)
    }
    ultimately show ?thesis by (rule le_listI)
  qed

  from wt_err
  have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi"
    by (simp add: wt_err_step_def JVM_le_Err_conv)
  with start istype_phi less_phi is_bcv
  have "\p. p < length bs \ kiljvm G maxs ?mxr rT et bs ?start ! p \ Err"
    by (unfold is_bcv_def) auto
  with bounded instrs
  show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
qed

theorem jvm_kildall_sound_complete:
  "wt_jvm_prog_kildall G = (\Phi. wt_jvm_prog G Phi)"
proof
  let ?Phi = "\C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"

  assume "wt_jvm_prog_kildall G"
  hence "wt_jvm_prog G ?Phi"
    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
    apply (erule jvm_prog_lift)
    apply (auto dest!: wt_kil_correct intro: someI)
    done
  thus "\Phi. wt_jvm_prog G Phi" by fast
next
  assume "\Phi. wt_jvm_prog G Phi"
  thus "wt_jvm_prog_kildall G"
    apply (clarify)
    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
    apply (erule jvm_prog_lift)
    apply (auto intro: wt_kil_complete)
    done
qed

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.