canonical start state
authorkleing
Sat Mar 09 20:39:46 2002 +0100 (2002-03-09)
changeset 130523bf41c474a88
parent 13051 8efb5d92cf55
child 13053 68ffc262c766
canonical start state
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/JVM/JVMExceptions.thy
src/HOL/MicroJava/JVM/JVMExec.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
src/HOL/MicroJava/JVM/JVMState.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sat Mar 09 20:39:19 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat Mar 09 20:39:46 2002 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
     1.6  
     1.7 -theory BVExample = JVMListExample + Correct:
     1.8 +theory BVExample = JVMListExample + BVSpecTypeSafe:
     1.9  
    1.10  text {*
    1.11    This theory shows type correctness of the example program in section 
    1.12 @@ -365,20 +365,11 @@
    1.13  text {* Execution of the program will be typesafe, because its
    1.14    start state conforms to the welltyping: *}
    1.15  
    1.16 -lemma [simp]: "preallocated start_heap"
    1.17 -  apply (unfold start_heap_def preallocated_def)
    1.18 -  apply auto
    1.19 -  apply (case_tac x)
    1.20 -  apply auto
    1.21 -  done
    1.22 -
    1.23 -lemma "E,\<Phi> \<turnstile>JVM start_state \<surd>"
    1.24 -  apply (simp add: correct_state_def start_state_def test_class_def)
    1.25 -  apply (simp add: hconf_def start_heap_def oconf_def lconf_def)
    1.26 -  apply (simp add: Phi_def phi_makelist_def)
    1.27 -  apply (simp add: correct_frame_def)
    1.28 -  apply (simp add: make_list_ins_def)
    1.29 -  apply (simp add: conf_def start_heap_def)
    1.30 +lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
    1.31 +  apply (rule BV_correct_initial)
    1.32 +    apply (rule wf_prog)
    1.33 +   apply simp
    1.34 +  apply simp
    1.35    done
    1.36  
    1.37  end
     2.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Mar 09 20:39:19 2002 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Mar 09 20:39:46 2002 +0100
     2.3 @@ -264,16 +264,21 @@
     2.4    assume xcpt: ?xcpt with pre show ?thesis 
     2.5    proof (cases "ins!pc")
     2.6      case New with xcpt pre
     2.7 -    show ?thesis by (auto dest: new_Addr_OutOfMemory) 
     2.8 +    show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD) 
     2.9    next
    2.10      case Throw with xcpt wt
    2.11      show ?thesis
    2.12        by (auto simp add: wt_instr_def correct_state_def correct_frame_def 
    2.13 -               dest: non_npD)
    2.14 -  qed auto
    2.15 +               dest: non_npD dest!: preallocatedD)
    2.16 +  qed (auto dest!: preallocatedD)
    2.17  qed
    2.18  
    2.19  
    2.20 +lemma cname_of_xcp [intro]:
    2.21 +  "\<lbrakk>preallocated hp; xcp = Addr (XcptRef x)\<rbrakk> \<Longrightarrow> cname_of hp xcp = Xcpt x"
    2.22 +  by (auto elim: preallocatedE [of hp x])
    2.23 +
    2.24 +
    2.25  text {*
    2.26    Finally we can state that, whenever an exception occurs, the
    2.27    resulting next state always conforms:
    2.28 @@ -358,7 +363,7 @@
    2.29        with some_handler xp'
    2.30        have xcp: "xcp = Addr (XcptRef OutOfMemory)"
    2.31          by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory)
    2.32 -      with prehp have "cname_of hp xcp = Xcpt OutOfMemory" by simp
    2.33 +      with prehp have "cname_of hp xcp = Xcpt OutOfMemory" ..
    2.34        with New some_handler phi_pc eff 
    2.35        obtain ST' LT' where
    2.36          phi': "phi C sig ! handler = Some (ST', LT')" and
    2.37 @@ -369,7 +374,7 @@
    2.38        moreover
    2.39        { from xcp prehp
    2.40          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)"
    2.41 -          by (simp add: conf_def obj_ty_def)
    2.42 +          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
    2.43          moreover
    2.44          from wf less loc
    2.45          have "approx_loc G hp loc LT'"
    2.46 @@ -388,7 +393,7 @@
    2.47        with some_handler xp'
    2.48        have xcp: "xcp = Addr (XcptRef NullPointer)"
    2.49          by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
    2.50 -      with prehp have "cname_of hp xcp = Xcpt NullPointer" by simp
    2.51 +      with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
    2.52        with Getfield some_handler phi_pc eff 
    2.53        obtain ST' LT' where
    2.54          phi': "phi C sig ! handler = Some (ST', LT')" and
    2.55 @@ -399,7 +404,7 @@
    2.56        moreover
    2.57        { from xcp prehp
    2.58          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
    2.59 -          by (simp add: conf_def obj_ty_def)
    2.60 +          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
    2.61          moreover
    2.62          from wf less loc
    2.63          have "approx_loc G hp loc LT'"
    2.64 @@ -418,7 +423,7 @@
    2.65        with some_handler xp'
    2.66        have xcp: "xcp = Addr (XcptRef NullPointer)"
    2.67          by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
    2.68 -      with prehp have "cname_of hp xcp = Xcpt NullPointer" by simp
    2.69 +      with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
    2.70        with Putfield some_handler phi_pc eff 
    2.71        obtain ST' LT' where
    2.72          phi': "phi C sig ! handler = Some (ST', LT')" and
    2.73 @@ -429,7 +434,7 @@
    2.74        moreover
    2.75        { from xcp prehp
    2.76          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
    2.77 -          by (simp add: conf_def obj_ty_def)
    2.78 +          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
    2.79          moreover
    2.80          from wf less loc
    2.81          have "approx_loc G hp loc LT'"
    2.82 @@ -448,7 +453,7 @@
    2.83        with some_handler xp'
    2.84        have xcp: "xcp = Addr (XcptRef ClassCast)"
    2.85          by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
    2.86 -      with prehp have "cname_of hp xcp = Xcpt ClassCast" by simp
    2.87 +      with prehp have "cname_of hp xcp = Xcpt ClassCast" ..
    2.88        with Checkcast some_handler phi_pc eff 
    2.89        obtain ST' LT' where
    2.90          phi': "phi C sig ! handler = Some (ST', LT')" and
    2.91 @@ -459,7 +464,7 @@
    2.92        moreover
    2.93        { from xcp prehp
    2.94          have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ClassCast)"
    2.95 -          by (simp add: conf_def obj_ty_def)
    2.96 +          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
    2.97          moreover
    2.98          from wf less loc
    2.99          have "approx_loc G hp loc LT'"
   2.100 @@ -1296,6 +1301,7 @@
   2.101  apply (auto intro: BV_correct_1)
   2.102  done
   2.103  
   2.104 +
   2.105  theorem BV_correct_implies_approx:
   2.106  "\<lbrakk> wt_jvm_prog G phi; 
   2.107      G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
   2.108 @@ -1307,4 +1313,45 @@
   2.109              split: option.splits)
   2.110  done
   2.111  
   2.112 +lemma 
   2.113 +  fixes G :: jvm_prog ("\<Gamma>")
   2.114 +  assumes wf: "wf_prog wf_mb \<Gamma>"
   2.115 +  shows hconf_start: "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
   2.116 +  apply (unfold hconf_def start_heap_def)
   2.117 +  apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm)
   2.118 +  apply (simp add: fields_is_type [OF _ wf is_class_xcpt [OF wf]])+
   2.119 +  done
   2.120 +    
   2.121 +lemma 
   2.122 +  fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
   2.123 +  shows BV_correct_initial: 
   2.124 +  "wt_jvm_prog \<Gamma> \<Phi> \<Longrightarrow> is_class \<Gamma> C \<Longrightarrow> method (\<Gamma>,C) (m,[]) = Some (C, b)
   2.125 +  \<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM start_state G C m \<surd>"
   2.126 +  apply (cases b)
   2.127 +  apply (unfold  start_state_def)
   2.128 +  apply (unfold correct_state_def)
   2.129 +  apply (auto simp add: preallocated_start)
   2.130 +   apply (simp add: wt_jvm_prog_def hconf_start)
   2.131 +  apply (drule wt_jvm_prog_impl_wt_start, assumption+)
   2.132 +  apply (clarsimp simp add: wt_start_def)
   2.133 +  apply (auto simp add: correct_frame_def)
   2.134 +   apply (simp add: approx_stk_def sup_state_conv)
   2.135 +  apply (auto simp add: sup_state_conv approx_val_def dest!: widen_RefT split: err.splits)
   2.136 +  done  
   2.137 +
   2.138 +theorem
   2.139 +  fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
   2.140 +  assumes welltyped:   "wt_jvm_prog \<Gamma> \<Phi>" and
   2.141 +          main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"  
   2.142 +  shows typesafe:
   2.143 +  "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s  \<Longrightarrow>  \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
   2.144 +proof -
   2.145 +  from welltyped main_method
   2.146 +  have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
   2.147 +  moreover
   2.148 +  assume "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s"
   2.149 +  ultimately  
   2.150 +  show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
   2.151 +qed
   2.152 +  
   2.153  end
     3.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Sat Mar 09 20:39:19 2002 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Sat Mar 09 20:39:46 2002 +0100
     3.3 @@ -158,6 +158,14 @@
     3.4  apply assumption
     3.5  done
     3.6  
     3.7 +lemma loc_widen_Err [dest]:
     3.8 +  "\<And>XT. G \<turnstile> replicate n Err <=l XT \<Longrightarrow> XT = replicate n Err"
     3.9 +  by (induct n) auto
    3.10 +  
    3.11 +lemma approx_loc_Err [iff]:
    3.12 +  "approx_loc G hp (replicate n v) (replicate n Err)"
    3.13 +  by (induct n) auto
    3.14 +
    3.15  lemma approx_loc_subst:
    3.16    "\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
    3.17    \<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
    3.18 @@ -280,10 +288,19 @@
    3.19    apply (simp del: split_paired_All)
    3.20    done  
    3.21  
    3.22 -lemma preallocated_newref:
    3.23 -  "\<lbrakk> hp oref = None; preallocated hp \<rbrakk> \<Longrightarrow> preallocated (hp(oref\<mapsto>obj))"
    3.24 -  by (unfold preallocated_def) auto
    3.25  
    3.26 +lemma 
    3.27 +  assumes none: "hp oref = None" and alloc: "preallocated hp"
    3.28 +  shows preallocated_newref: "preallocated (hp(oref\<mapsto>obj))"
    3.29 +proof (cases oref)
    3.30 +  case (XcptRef x) 
    3.31 +  with none alloc have "False" by (auto elim: preallocatedE [of _ x])
    3.32 +  thus ?thesis ..
    3.33 +next
    3.34 +  case (Loc l)
    3.35 +  with alloc show ?thesis by (simp add: preallocated_def)
    3.36 +qed
    3.37 +  
    3.38  section {* correct-frames *}
    3.39  
    3.40  lemmas [simp del] = fun_upd_apply
     4.1 --- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sat Mar 09 20:39:19 2002 +0100
     4.2 +++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sat Mar 09 20:39:46 2002 +0100
     4.3 @@ -50,17 +50,20 @@
     4.4  
     4.5  
     4.6  text {*
     4.7 -  System exceptions are allocated in all heaps, 
     4.8 -  and they don't carry any information other than their type: 
     4.9 +  System exceptions are allocated in all heaps:
    4.10  *}
    4.11  constdefs
    4.12    preallocated :: "aheap \<Rightarrow> bool"
    4.13 -  "preallocated hp \<equiv> \<forall>x. hp (XcptRef x) = Some (Xcpt x, empty)"
    4.14 +  "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
    4.15  
    4.16 -lemma preallocated_iff [iff]:
    4.17 -  "preallocated hp \<Longrightarrow> hp (XcptRef x) = Some (Xcpt x, empty)"
    4.18 +lemma preallocatedD:
    4.19 +  "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
    4.20    by (unfold preallocated_def) fast
    4.21  
    4.22 +lemma preallocatedE [elim?]:
    4.23 +  "preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp"
    4.24 +  by (fast dest: preallocatedD)
    4.25 +
    4.26  lemma cname_of_xcp:
    4.27    "raise_system_xcpt b x = Some xcp \<Longrightarrow> preallocated hp 
    4.28    \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
    4.29 @@ -70,9 +73,18 @@
    4.30      by (simp add: raise_system_xcpt_def split: split_if_asm)
    4.31    moreover
    4.32    assume "preallocated hp" 
    4.33 -  hence "hp (XcptRef x) = Some (Xcpt x, empty)" ..
    4.34 +  then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
    4.35    ultimately
    4.36    show ?thesis by simp
    4.37  qed
    4.38  
    4.39 +lemma preallocated_start:
    4.40 +  "preallocated (start_heap G)"
    4.41 +  apply (unfold preallocated_def)
    4.42 +  apply (unfold start_heap_def)
    4.43 +  apply (rule allI)
    4.44 +  apply (case_tac x)
    4.45 +  apply (auto simp add: blank_def)
    4.46 +  done
    4.47 +
    4.48  end
     5.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Sat Mar 09 20:39:19 2002 +0100
     5.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Sat Mar 09 20:39:46 2002 +0100
     5.3 @@ -36,4 +36,16 @@
     5.4    exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
     5.5                ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
     5.6  
     5.7 +text {*
     5.8 +  The start configuration of the JVM: in the start heap, we call a 
     5.9 +  method @{text m} of class @{text C} in program @{text G}. The 
    5.10 +  @{text this} pointer of the frame is set to @{text Null} to simulate
    5.11 +  a static method invokation.
    5.12 +*}
    5.13 +constdefs  
    5.14 +  start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state"
    5.15 +  "start_state G C m \<equiv>
    5.16 +  let (C',rT,mxs,mxl,ins,et) = the (method (G,C) (m,[])) in
    5.17 +    (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])"
    5.18 +
    5.19  end
     6.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sat Mar 09 20:39:19 2002 +0100
     6.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sat Mar 09 20:39:46 2002 +0100
     6.3 @@ -14,7 +14,6 @@
     6.4    makelist_name :: mname
     6.5    val_nam :: vnam
     6.6    next_nam :: vnam
     6.7 -  test_name_loc :: loc_
     6.8  
     6.9  constdefs
    6.10    list_name :: cname
    6.11 @@ -87,15 +86,6 @@
    6.12    E :: jvm_prog
    6.13    "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
    6.14  
    6.15 -  start_heap :: aheap
    6.16 -  "start_heap == empty (XcptRef NullPointer \<mapsto> (Xcpt NullPointer, empty))
    6.17 -                       (XcptRef ClassCast \<mapsto> (Xcpt ClassCast, empty))
    6.18 -                       (XcptRef OutOfMemory \<mapsto> (Xcpt OutOfMemory, empty))
    6.19 -                       (Loc test_name_loc \<mapsto> (test_name, empty))"
    6.20 -
    6.21 -  start_state :: jvm_state
    6.22 -  "start_state ==
    6.23 -    (None, start_heap, [([], [Addr (Loc test_name_loc), arbitrary, arbitrary], test_name, (makelist_name, []), 0)])"
    6.24  
    6.25  types_code
    6.26    cnam ("string")
    6.27 @@ -112,8 +102,6 @@
    6.28    "arbitrary" :: "val" ("{* Unit *}")
    6.29    "arbitrary" :: "cname" ("Object")
    6.30  
    6.31 -  "test_name_loc" ("0")
    6.32 -
    6.33    "list_nam" ("\"list\"")
    6.34    "test_nam" ("\"test\"")
    6.35    "append_name" ("\"append\"")
    6.36 @@ -130,7 +118,7 @@
    6.37  subsection {* Single step execution *}
    6.38  
    6.39  generate_code 
    6.40 -  test = "exec (E, start_state)"
    6.41 +  test = "exec (E, start_state E test_name makelist_name)"
    6.42  
    6.43  ML {* test *}
    6.44  ML {* exec (E, the it) *}
     7.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Sat Mar 09 20:39:19 2002 +0100
     7.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sat Mar 09 20:39:46 2002 +0100
     7.3 @@ -46,6 +46,16 @@
     7.4    jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
     7.5  
     7.6  
     7.7 +text {* a new, blank object with default values in all fields: *}
     7.8 +constdefs
     7.9 +  blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
    7.10 +  "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
    7.11 +
    7.12 +  start_heap :: "'c prog \<Rightarrow> aheap"
    7.13 +  "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
    7.14 +                      (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
    7.15 +                      (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
    7.16 +
    7.17  section {* Lemmas *}
    7.18  
    7.19  lemma new_AddrD:
    7.20 @@ -68,6 +78,6 @@
    7.21    assume "snd (new_Addr hp) = Some xcp" 
    7.22    ultimately
    7.23    show ?thesis by (auto dest: new_AddrD)
    7.24 -qed  
    7.25 -
    7.26 +qed
    7.27 +  
    7.28  end
    7.29 \ No newline at end of file