Theory BVExample

Up to index of Isabelle/HOL/arrays

theory BVExample = JVMListExample + BVSpecTypeSafe:
(*  Title:      HOL/MicroJava/BV/BVExample.thy
    ID:         $Id: BVExample.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
    Author:     Gerwin Klein
*)

header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}

theory BVExample = JVMListExample + BVSpecTypeSafe:

text {*
  This theory shows type correctness of the example program in section 
  \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
  explicitly providing a welltyping. It also shows that the start
  state of the program conforms to the welltyping; hence type safe
  execution is guaranteed.
*}

section "Setup"
text {*
  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
  anonymous, we describe distinctness of names in the example by axioms:
*}
axioms 
  distinct_classes [simp]: "list_nam \<noteq> test_nam"
  distinct_fields  [simp]: "val_nam \<noteq> next_nam"
  distinct_meth_list [simp]: "append_name \<noteq> init"
  distinct_meth_test [simp]: "makelist_name \<noteq> init"

declare 
  distinct_classes [symmetric, simp]
  distinct_fields  [symmetric, simp]
  distinct_meth_list [symmetric, simp]
  distinct_meth_test [symmetric, simp]

text {* Abbreviations for theorem sets we will have to use often in the
proofs below: *}
lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def
lemmas system_defs = JVMSystemClasses_def SystemClassC_defs
lemmas class_defs  = list_class_def test_class_def

text {* These auxiliary proofs are for efficiency: class lookup,
subclass relation, method and field lookup are computed only once:
*}
lemma class_list [simp]:
  "class E list_name = Some list_class"
  by (simp add: class_def system_defs E_def name_defs)
 
lemma class_test [simp]:
  "class E test_name = Some test_class"
  by (simp add: class_def system_defs E_def name_defs)

lemma E_classes [simp]:
  "{C. is_class E C} = 
  {list_name, test_name, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory, 
  Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize, Xcpt ArrayStore, Object}"
  by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)

text {* The subclass relation spelt out: *}
lemma subcls1:
  "subcls1 E = 
  {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
  (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object), (Xcpt ArrayStore, Object),
  (Xcpt ArrayIndexOutOfBounds, Object), (Xcpt NegativeArraySize, Object)}"
  (is "_ = ?set")
proof
  show "?set \<subseteq> subcls1 E" 
    apply (simp add: subcls1_def2)
    apply (unfold E_def system_defs class_def class_defs name_defs)
    apply auto
    done
  show "subcls1 E \<subseteq> ?set"
    apply rule
    apply (erule subcls1.elims)
    apply (drule class_SomeD)
    apply (unfold E_def class_defs system_defs)
    apply auto
    done
qed

text {* The subclass relation is acyclic; hence its converse is well founded: *}
lemma notin_rtrancl:
  "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
  by (auto elim: converse_rtranclE)  

lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
  apply (rule acyclicI)
  apply (simp add: subcls1)
  apply (auto dest!: tranclD)
  apply (auto elim!: notin_rtrancl simp add: name_defs)
  done

lemma wf_subcls1_E: "wf ((subcls1 E)¯)"
  apply (rule finite_acyclic_wf_converse)
  apply (simp add: subcls1)
  apply (rule acyclic_subcls1_E)
  done  

text {* Method and field lookup: *}

lemma unique: "unique E"
  by (unfold E_def class_defs system_defs name_defs) auto

lemma sys_classes_G: "sys_classes E"
  apply (rule sys_classes.intro)
    apply (clarsimp simp add: E_def)
   apply (rule unique)
  apply (rule wf_subcls1_E)
  done  

lemmas lookups [simp] = sys_lemmas [OF sys_classes_G]

lemma method_append [simp]:
  "method (E, list_name) (append_name, [Class list_name]) =
  Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
  apply (insert class_list)
  apply (unfold list_class_def)
  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
  apply (simp add: name_defs Default_ctor_def)
  done

lemma method_makelist [simp]:
  "method (E, test_name) (makelist_name, []) = 
  Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
  apply (insert class_test)
  apply (unfold test_class_def)
  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
  apply (simp add: name_defs Default_ctor_def)
  done

lemma method_default_ctor [simp]:
  "method (E, list_name) (init, []) = 
  Some (list_name,PrimT Void,1,0,[Load 0,Invoke_special Object init [],Return],[])"
  apply (insert class_list)
  apply (unfold list_class_def)
  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
  apply (simp add: name_defs Default_ctor_def)
  done

lemma field_val [simp]:
  "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
  apply (unfold field_def)
  apply (insert class_list)
  apply (unfold list_class_def)
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
  apply simp
  done

lemma field_next [simp]:
  "field (E, list_name) next_name = Some (list_name, Class list_name)"
  apply (unfold field_def)
  apply (insert class_list)
  apply (unfold list_class_def)
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
  apply (simp add: name_defs distinct_fields [symmetric])
  done

lemma [simp]: "fields (E, test_name) = []"
  apply (insert class_test)
  apply (unfold test_class_def)
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
  apply simp
  done

lemmas [simp] = is_class_def

text {*
  The next definition and three proof rules implement an algorithm to
  enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
  transforms a goal of the form
  @{prop [display] "pc < n \<Longrightarrow> P pc"} 
  into a series of goals
  @{prop [display] "P 0"} 
  @{prop [display] "P (Suc 0)"} 

  @{text "\<dots>"}

  @{prop [display] "P n"} 
*}
constdefs 
  intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
  "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"

lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
  by (simp add: intervall_def)

lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
  apply (cases "x=n0")
  apply (auto simp add: intervall_def) 
  done

lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
  by (unfold intervall_def) arith


section "Program structure"

text {*
  The program is structurally wellformed:
*}
lemma wf_struct:
  "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
proof -
  note simps [simp] = wf_mdecl_def wf_mhead_def wf_cdecl_def system_defs max_dim_def
  have "unique E" by (rule unique)
  moreover
  have "wf_syscls E" by simp
  moreover
  have "wf_cdecl ?mb E ObjectC" by simp
  moreover
  have "wf_cdecl ?mb E NullPointerC" 
    by (auto elim: notin_rtrancl simp add: name_defs subcls1)
  moreover
  have "wf_cdecl ?mb E ClassCastC" 
    by (auto elim: notin_rtrancl simp add: name_defs subcls1)
  moreover
  have "wf_cdecl ?mb E OutOfMemoryC" 
    by (auto elim: notin_rtrancl simp add: name_defs subcls1)
  moreover
  have "wf_cdecl ?mb E ArrayIndexOutOfBoundsC" 
    by (auto elim: notin_rtrancl simp add: name_defs subcls1)
  moreover
  have "wf_cdecl ?mb E NegativeArraySizeC" 
    by (auto elim: notin_rtrancl simp add: name_defs subcls1)
  moreover
  have "wf_cdecl ?mb E ArrayStoreC" 
    by (auto elim: notin_rtrancl simp add: name_defs subcls1)
  moreover
  have "wf_cdecl ?mb E (list_name, list_class)"
    apply (auto elim!: notin_rtrancl 
            simp add: wf_fdecl_def list_class_def subcls1)
    apply (auto simp add: name_defs)
    done    
  moreover
  have "wf_cdecl ?mb E (test_name, test_class)" 
    apply (auto elim!: notin_rtrancl 
            simp add: wf_fdecl_def test_class_def subcls1)
    apply (auto simp add: name_defs)
    done      
  ultimately
  show ?thesis by (simp del: simps add: wf_prog_def E_def JVMSystemClasses_def)
qed

section "Welltypings"
text {*
  We show welltypings of all methods in the program @{text E}. 
  The more interesting ones are @{term append_name} in class @{term list_name}, 
  and @{term makelist_name} in class @{term test_name}. The rest are
  default constructors.
*}
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def eff_bool_def 
declare 
  appInvoke [simp del] 
  appInvoke_special [simp del]

constdefs
  phi_obj_ctor :: method_type ("\<phi>\<^sub>o")
  "\<phi>\<^sub>o \<equiv> [{(([],                  [OK (Init (Class Object))]), True)},
         {(([Init (PrimT Void)], [OK (Init (Class Object))]), True)}]"


lemma check_types_lemma [simp]:
  "(\<forall>((a,b),x)\<in>A. b \<in> list mxr (err (init_tys E mpc)) \<and>
                            a \<in> list (length a) (init_tys E mpc) \<and>
                            length a \<le> mxs)
  \<Longrightarrow>
  OK A \<in> states E mxs mxr mpc"
  apply (unfold states_def address_types_def)
  apply simp
  apply (rule subsetI)
  apply clarify
  apply (drule bspec, assumption)
  apply blast
  done

lemma Object_init [simp]:
  "wt_method E Object init [] (PrimT Void) (Suc 0) 0 [LitPush Unit, Return] [] \<phi>\<^sub>o"
  apply (simp add: wt_method_def phi_obj_ctor_def
                   wt_start_def wt_instr_def)
  apply (simp add: check_types_def init_tys_def)
  apply clarify
  apply (elim pc_end pc_next pc_0)
  apply fastsimp
  apply fastsimp
  done  

constdefs
  phi_default_ctor :: "cname \<Rightarrow> method_type" ("\<phi>\<^sub>c _")
  "\<phi>\<^sub>c C \<equiv> [{(([],                  [OK (PartInit C)]), False)},
           {(([PartInit C],        [OK (PartInit C)]), False)},
           {(([Init (PrimT Void)], [OK (Init (Class C))]),  True)}]"

lemma [simp]: "Ex Not" by fast
lemma [simp]: "\<exists>z. z" by fast

lemma default_ctor [simp]:
  "E \<turnstile> C \<prec>C1 Object \<Longrightarrow>  is_class E C \<Longrightarrow> 
  wt_method E C init [] (PrimT Void) (Suc 0) 0 
            [Load 0, Invoke_special Object init [], Return] [] (\<phi>\<^sub>c C)"
  apply (simp add: wt_method_def phi_default_ctor_def
                   wt_start_def wt_instr_def check_types_def init_tys_def)
  apply (rule conjI)
  apply clarify
  apply (elim pc_end pc_next pc_0)
  apply simp
  apply (simp add: app_def xcpt_app_def replace_def)
  apply (simp add: Object_ctor_def)
  apply simp
  apply (fast dest: subcls1_wfD [OF _ wf_struct])
  done  


constdefs
  phi_append :: method_type ("\<phi>\<^sub>a")
  "\<phi>\<^sub>a \<equiv> map (image (\<lambda>ST. ((map Init ST, map (OK \<circ> Init) [Class list_name, Class list_name]), False)))
  [{                                    []},
   {                     [Class list_name]},
   {                     [Class list_name]},
   {    [Class list_name, Class list_name]},
   {[NT, Class list_name, Class list_name]},
   {                     [Class list_name]},
   {    [Class list_name, Class list_name]},
   {                          [PrimT Void]},
   {                     [Class list_name], [Class (Xcpt NullPointer)]},
   {                                    []},
   {                     [Class list_name]},
   {    [Class list_name, Class list_name]},
   {                                    []},
   {                          [PrimT Void]}]"

lemma wt_append [simp]:
  "wt_method E list_name append_name [Class list_name] (PrimT Void) 3 0 append_ins
             [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
  apply (simp add: wt_method_def append_ins_def phi_append_def 
                   wt_start_def wt_instr_def name_defs)
  apply (fold name_defs)
  apply (simp add: check_types_def init_tys_def)
  apply clarify
  apply (elim pc_end pc_next pc_0)
  apply simp
  apply simp
  apply (clarsimp simp add: match_exception_entry_def)
  apply simp
  apply simp
  apply simp
  apply (simp add: app_def xcpt_app_def)
  apply simp
  apply simp
  apply simp
  apply simp
  apply (simp add: match_exception_entry_def)
  apply simp
  apply simp
  done


text {* Some abbreviations for readability *} 
syntax
  list :: ty 
  test :: ty
  intg :: ty
  void :: ty
translations
  "list" == "Init (Class list_name)"
  "test" == "Init (Class test_name)"
  "intg" == "Init (PrimT Integer)"
  "void" == "Init (PrimT Void)"  

constdefs
  phi_makelist :: method_type ("\<phi>\<^sub>m")
  "\<phi>\<^sub>m \<equiv> map (\<lambda>x. {(x,False)}) [ 
  (                                         [], [OK test,     Err,     Err]),
  (                       [UnInit list_name 0], [OK test,     Err,     Err]),
  (   [UnInit list_name 0, UnInit list_name 0], [OK test,     Err,     Err]),
  ([UnInit list_name 0,UnInit list_name 0,UnInit list_name 0],[OK test,Err,Err]),
  (                         [void, list, list], [OK test,     Err,     Err]),
  (                               [list, list], [OK test,     Err,     Err]),
  (                                     [list], [OK list,     Err,     Err]),
  (                               [intg, list], [OK list,     Err,     Err]),
  (                                         [], [OK list,     Err,     Err]),
  (                       [UnInit list_name 8], [OK list,     Err,     Err]),
  (   [UnInit list_name 8, UnInit list_name 8], [OK list,     Err,     Err]),
  (                               [void, list], [OK list,     Err,     Err]),
  (                                     [list], [OK list,     Err,     Err]),
  (                               [list, list], [OK list,     Err,     Err]),
  (                                     [list], [OK list, OK list,     Err]),
  (                               [intg, list], [OK list, OK list,     Err]),
  (                                         [], [OK list, OK list,     Err]),
  (                      [UnInit list_name 16], [OK list, OK list,     Err]),
  ( [UnInit list_name 16, UnInit list_name 16], [OK list, OK list,     Err]),
  (                               [void, list], [OK list, OK list,     Err]),
  (                                     [list], [OK list, OK list,     Err]),
  (                               [list, list], [OK list, OK list,     Err]),
  (                                     [list], [OK list, OK list, OK list]),
  (                               [intg, list], [OK list, OK list, OK list]),
  (                                         [], [OK list, OK list, OK list]),
  (                                     [list], [OK list, OK list, OK list]),
  (                               [list, list], [OK list, OK list, OK list]),
  (                                     [void], [OK list, OK list, OK list]),
  (                               [list, void], [OK list, OK list, OK list]),
  (                         [list, list, void], [OK list, OK list, OK list]),
  (                               [void, void], [OK list, OK list, OK list])
  ]"

lemma wt_makelist [simp]:
  "wt_method E test_name makelist_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m" 
  apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
  apply (simp add: wt_start_def nat_number)
  apply (simp add: wt_instr_def name_defs)
  apply (fold name_defs)
  apply (simp add: check_types_def init_tys_def list_class_def)
  apply clarify
  apply (elim pc_end pc_next pc_0)
  apply (simp add: replace_def)
  apply simp
  apply simp
  apply (simp add: app_def xcpt_app_def replace_def)
  apply simp
  apply simp
  apply simp
  apply simp
  apply (simp add: replace_def)
  apply simp   
  apply simp
  apply (simp add: app_def xcpt_app_def replace_def)
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply (simp add: replace_def)
  apply simp
  apply simp
  apply (simp add: app_def xcpt_app_def replace_def)
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply (simp add: app_def xcpt_app_def)
  apply simp
  apply simp
  apply (simp add: app_def xcpt_app_def)
  apply simp
  done


text {* The whole program is welltyped: *}
constdefs 
  Phi :: prog_type ("\<Phi>")
  "\<Phi> C sig \<equiv> if C = Object \<and> sig = (init,[]) then \<phi>\<^sub>o else
              if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
              if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else
              if sig = (init,[]) then \<phi>\<^sub>c C else []" 
  

lemma [simp]:
  "is_class E C = (C \<in> 
  {Cname list_nam, Cname test_nam, Xcpt NullPointer, Xcpt ClassCast, 
   Xcpt OutOfMemory, Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize, 
   Xcpt ArrayStore, Object})"
  apply (insert E_classes)
  apply (auto simp add: name_defs)
  done

declare is_class_def [simp del]

lemma wf_prog:
  "wt_jvm_prog E \<Phi>"
  apply (unfold wt_jvm_prog_def)
  apply (rule wf_mb'E [OF wf_struct])
  apply (simp add: E_def)
  apply clarify
  apply (fold E_def)
  apply (simp add: system_defs class_defs)
  apply auto
  apply (auto simp add: Phi_def)
  apply (insert subcls1)
  apply (auto simp add: name_defs)
  done

section "Conformance"
text {* Execution of the program will be typesafe, because its
  start state conforms to the welltyping: *}

lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
  apply (rule BV_correct_initial)
  apply (rule wf_prog)
  apply (auto simp add: is_class_def)
  done

end

Setup

lemmas name_defs:

  list_name == Cname list_nam
  test_name == Cname test_nam
  val_name == VName val_nam
  next_name == VName next_nam

lemmas system_defs:

  JVMSystemClasses ==
  [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC, NegativeArraySizeC,
   ArrayIndexOutOfBoundsC, ArrayStoreC]
  ObjectC_decl ms == (Object, arbitrary, [], ms)
  NullPointerC_decl ms == (Xcpt NullPointer, Object, [], ms)
  ClassCastC_decl ms == (Xcpt ClassCast, Object, [], ms)
  OutOfMemoryC_decl ms == (Xcpt OutOfMemory, Object, [], ms)
  ArrayIndexOutOfBoundsC_decl ms == (Xcpt ArrayIndexOutOfBounds, Object, [], ms)
  NegativeArraySizeC_decl ms == (Xcpt NegativeArraySize, Object, [], ms)
  ArrayStoreC_decl ms == (Xcpt ArrayStore, Object, [], ms)
  ObjectC == ObjectC_decl [Object_ctor]
  NullPointerC == NullPointerC_decl [Default_ctor]
  OutOfMemoryC == OutOfMemoryC_decl [Default_ctor]
  ClassCastC == ClassCastC_decl [Default_ctor]
  NegativeArraySizeC == NegativeArraySizeC_decl [Default_ctor]
  ArrayStoreC == ArrayStoreC_decl [Default_ctor]
  ArrayIndexOutOfBoundsC == ArrayIndexOutOfBoundsC_decl [Default_ctor]
  Default_ctor ==
  ((init, []), PrimT Void, 1, 0, [Load 0, Invoke_special Object init [], Return],
   [])
  Object_ctor == ((init, []), PrimT Void, 1, 0, [LitPush Unit, Return], [])

lemmas class_defs:

  list_class ==
  (Object, [(val_name, PrimT Integer), (next_name, Class list_name)],
   [Default_ctor,
    ((append_name, [Class list_name]), PrimT Void, 3, 0, append_ins,
     [(1, 2, 8, Xcpt NullPointer)])])
  test_class ==
  (Object, [],
   [Default_ctor, ((makelist_name, []), PrimT Void, 3, 2, make_list_ins, [])])

lemma class_list:

  class E list_name = Some list_class

lemma class_test:

  class E test_name = Some test_class

lemma E_classes:

  Collect (is_class E) =
  {list_name, test_name, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory,
   Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize, Xcpt ArrayStore, Object}

lemma subcls1:

  subcls1 E =
  {(list_name, Object), (test_name, Object), (Xcpt NullPointer, Object),
   (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object),
   (Xcpt ArrayStore, Object), (Xcpt ArrayIndexOutOfBounds, Object),
   (Xcpt NegativeArraySize, Object)}

lemma notin_rtrancl:

  [| (a, b) : r^*; a ~= b; !!y. (a, y) ~: r |] ==> False

lemma acyclic_subcls1_E:

  acyclic (subcls1 E)

lemma wf_subcls1_E:

  wf ((subcls1 E)^-1)

lemma unique:

  unique E

lemma sys_classes_G:

  sys_classes E

lemmas lookups:

  fields (E, Object) = []
  class E Object = Some (arbitrary, [], [Object_ctor])
  wf_syscls E
  class E (Xcpt NullPointer) = Some (Object, [], [Default_ctor])
  class E (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])
  class E (Xcpt ClassCast) = Some (Object, [], [Default_ctor])
  class E (Xcpt ArrayStore) = Some (Object, [], [Default_ctor])
  class E (Xcpt NegativeArraySize) = Some (Object, [], [Default_ctor])
  class E (Xcpt ArrayIndexOutOfBounds) = Some (Object, [], [Default_ctor])
  fields (E, Xcpt NullPointer) = []
  fields (E, Xcpt ClassCast) = []
  fields (E, Xcpt OutOfMemory) = []
  fields (E, Xcpt ArrayIndexOutOfBounds) = []
  fields (E, Xcpt NegativeArraySize) = []
  fields (E, Xcpt ArrayStore) = []
  method (E, Object) sig =
  (if sig = (init, []) then Some (Object, snd Object_ctor) else None)
  method (E, Xcpt NullPointer) sig =
  (if sig = (init, []) then Some (Xcpt NullPointer, snd Default_ctor) else None)
  method (E, Xcpt ClassCast) sig =
  (if sig = (init, []) then Some (Xcpt ClassCast, snd Default_ctor) else None)
  method (E, Xcpt OutOfMemory) sig =
  (if sig = (init, []) then Some (Xcpt OutOfMemory, snd Default_ctor) else None)
  method (E, Xcpt ArrayIndexOutOfBounds) sig =
  (if sig = (init, []) then Some (Xcpt ArrayIndexOutOfBounds, snd Default_ctor)
   else None)
  method (E, Xcpt NegativeArraySize) sig =
  (if sig = (init, []) then Some (Xcpt NegativeArraySize, snd Default_ctor)
   else None)
  method (E, Xcpt ArrayStore) sig =
  (if sig = (init, []) then Some (Xcpt ArrayStore, snd Default_ctor) else None)

lemma method_append:

  method (E, list_name) (append_name, [Class list_name]) =
  Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])

lemma method_makelist:

  method (E, test_name) (makelist_name, []) =
  Some (test_name, PrimT Void, 3, 2, make_list_ins, [])

lemma method_default_ctor:

  method (E, list_name) (init, []) =
  Some (list_name, PrimT Void, 1, 0,
        [Load 0, Invoke_special Object init [], Return], [])

lemma field_val:

  field (E, list_name) val_name = Some (list_name, PrimT Integer)

lemma field_next:

  field (E, list_name) next_name = Some (list_name, Class list_name)

lemma

  fields (E, test_name) = []

lemmas

  is_class G C == class G C ~= None

lemma pc_0:

  [| x < n; x \<in> [0, n) ==> P x |] ==> P x

lemma pc_next:

  [| x \<in> [n0, n); P n0; x \<in> [Suc n0, n) ==> P x |] ==> P x

lemma pc_end:

  x \<in> [n, n) ==> P x

Program structure

lemma wf_struct:

  wf_prog (%G C mb. True) E

Welltypings

lemmas eff_simps:

  eff i G pc et at ==
  map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @
  xcpt_eff i G pc at et
  norm_eff i G pc pc' at ==
  eff_bool i G pc `
  (if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)
  xcpt_eff i G pc at et ==
  map (%C. (the (match_exception_table G C pc et),
            (%s. (([Init (Class C)], snd (fst s)), snd s)) ` at))
   (xcpt_names (i, G, pc, et))
  eff_bool i G pc ==
  %((ST, LT), z).
     (eff' (i, G, pc, ST, LT),
      if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
      then True else z)

lemma check_types_lemma:

  ALL ((a, b), x):A.
     b : list mxr (err (init_tys E mpc)) &
     a : list (length a) (init_tys E mpc) & length a <= mxs
  ==> OK A : states E mxs mxr mpc

lemma Object_init:

  wt_method E Object init [] (PrimT Void) (Suc 0) 0 [LitPush Unit, Return] []
   \<phi>\<^sub>o

lemma

  Ex Not

lemma

  EX z. z

lemma default_ctor:

  [| E |- C <=C1 Object; is_class E C |]
  ==> wt_method E C init [] (PrimT Void) (Suc 0) 0
       [Load 0, Invoke_special Object init [], Return] [] \<phi>\<^sub>c C

lemma wt_append:

  wt_method E list_name append_name [Class list_name] (PrimT Void) 3 0 append_ins
   [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a

lemma wt_makelist:

  wt_method E test_name makelist_name [] (PrimT Void) 3 2 make_list_ins []
   \<phi>\<^sub>m

lemma

  is_class E C =
  (C : {Cname list_nam, Cname test_nam, Xcpt NullPointer, Xcpt ClassCast,
        Xcpt OutOfMemory, Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize,
        Xcpt ArrayStore, Object})

lemma wf_prog:

  wt_jvm_prog E \<Phi>

Conformance

lemma

  E,\<Phi> |-JVM start_state E test_name makelist_name [ok]