# HG changeset patch # User kleing # Date 1015702786 -3600 # Node ID 3bf41c474a8888ecdb45a92429d7beabb3e573db # Parent 8efb5d92cf552288752f10fb59928e03f86a79b6 canonical start state diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Sat Mar 09 20:39:19 2002 +0100 +++ b/src/HOL/MicroJava/BV/BVExample.thy Sat Mar 09 20:39:46 2002 +0100 @@ -5,7 +5,7 @@ header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} -theory BVExample = JVMListExample + Correct: +theory BVExample = JVMListExample + BVSpecTypeSafe: text {* This theory shows type correctness of the example program in section @@ -365,20 +365,11 @@ text {* Execution of the program will be typesafe, because its start state conforms to the welltyping: *} -lemma [simp]: "preallocated start_heap" - apply (unfold start_heap_def preallocated_def) - apply auto - apply (case_tac x) - apply auto - done - -lemma "E,\ \JVM start_state \" - apply (simp add: correct_state_def start_state_def test_class_def) - apply (simp add: hconf_def start_heap_def oconf_def lconf_def) - apply (simp add: Phi_def phi_makelist_def) - apply (simp add: correct_frame_def) - apply (simp add: make_list_ins_def) - apply (simp add: conf_def start_heap_def) +lemma "E,\ \JVM start_state E test_name makelist_name \" + apply (rule BV_correct_initial) + apply (rule wf_prog) + apply simp + apply simp done end diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sat Mar 09 20:39:19 2002 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sat Mar 09 20:39:46 2002 +0100 @@ -264,16 +264,21 @@ assume xcpt: ?xcpt with pre show ?thesis proof (cases "ins!pc") case New with xcpt pre - show ?thesis by (auto dest: new_Addr_OutOfMemory) + show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD) next case Throw with xcpt wt show ?thesis by (auto simp add: wt_instr_def correct_state_def correct_frame_def - dest: non_npD) - qed auto + dest: non_npD dest!: preallocatedD) + qed (auto dest!: preallocatedD) qed +lemma cname_of_xcp [intro]: + "\preallocated hp; xcp = Addr (XcptRef x)\ \ cname_of hp xcp = Xcpt x" + by (auto elim: preallocatedE [of hp x]) + + text {* Finally we can state that, whenever an exception occurs, the resulting next state always conforms: @@ -358,7 +363,7 @@ with some_handler xp' have xcp: "xcp = Addr (XcptRef OutOfMemory)" by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory) - with prehp have "cname_of hp xcp = Xcpt OutOfMemory" by simp + with prehp have "cname_of hp xcp = Xcpt OutOfMemory" .. with New some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -369,7 +374,7 @@ moreover { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt OutOfMemory)" - by (simp add: conf_def obj_ty_def) + by (auto simp add: conf_def obj_ty_def dest!: preallocatedD) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -388,7 +393,7 @@ with some_handler xp' have xcp: "xcp = Addr (XcptRef NullPointer)" by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) - with prehp have "cname_of hp xcp = Xcpt NullPointer" by simp + with prehp have "cname_of hp xcp = Xcpt NullPointer" .. with Getfield some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -399,7 +404,7 @@ moreover { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt NullPointer)" - by (simp add: conf_def obj_ty_def) + by (auto simp add: conf_def obj_ty_def dest!: preallocatedD) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -418,7 +423,7 @@ with some_handler xp' have xcp: "xcp = Addr (XcptRef NullPointer)" by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) - with prehp have "cname_of hp xcp = Xcpt NullPointer" by simp + with prehp have "cname_of hp xcp = Xcpt NullPointer" .. with Putfield some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -429,7 +434,7 @@ moreover { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt NullPointer)" - by (simp add: conf_def obj_ty_def) + by (auto simp add: conf_def obj_ty_def dest!: preallocatedD) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -448,7 +453,7 @@ with some_handler xp' have xcp: "xcp = Addr (XcptRef ClassCast)" by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) - with prehp have "cname_of hp xcp = Xcpt ClassCast" by simp + with prehp have "cname_of hp xcp = Xcpt ClassCast" .. with Checkcast some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -459,7 +464,7 @@ moreover { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt ClassCast)" - by (simp add: conf_def obj_ty_def) + by (auto simp add: conf_def obj_ty_def dest!: preallocatedD) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -1296,6 +1301,7 @@ apply (auto intro: BV_correct_1) done + theorem BV_correct_implies_approx: "\ wt_jvm_prog G phi; G \ s0 -jvm\ (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \JVM s0 \\ @@ -1307,4 +1313,45 @@ split: option.splits) done +lemma + fixes G :: jvm_prog ("\") + assumes wf: "wf_prog wf_mb \" + shows hconf_start: "\ \h (start_heap \) \" + apply (unfold hconf_def start_heap_def) + apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm) + apply (simp add: fields_is_type [OF _ wf is_class_xcpt [OF wf]])+ + done + +lemma + fixes G :: jvm_prog ("\") and Phi :: prog_type ("\") + shows BV_correct_initial: + "wt_jvm_prog \ \ \ is_class \ C \ method (\,C) (m,[]) = Some (C, b) + \ \,\ \JVM start_state G C m \" + apply (cases b) + apply (unfold start_state_def) + apply (unfold correct_state_def) + apply (auto simp add: preallocated_start) + apply (simp add: wt_jvm_prog_def hconf_start) + apply (drule wt_jvm_prog_impl_wt_start, assumption+) + apply (clarsimp simp add: wt_start_def) + apply (auto simp add: correct_frame_def) + apply (simp add: approx_stk_def sup_state_conv) + apply (auto simp add: sup_state_conv approx_val_def dest!: widen_RefT split: err.splits) + done + +theorem + fixes G :: jvm_prog ("\") and Phi :: prog_type ("\") + assumes welltyped: "wt_jvm_prog \ \" and + main_method: "is_class \ C" "method (\,C) (m,[]) = Some (C, b)" + shows typesafe: + "G \ start_state \ C m -jvm\ s \ \,\ \JVM s \" +proof - + from welltyped main_method + have "\,\ \JVM start_state \ C m \" by (rule BV_correct_initial) + moreover + assume "G \ start_state \ C m -jvm\ s" + ultimately + show "\,\ \JVM s \" using welltyped by - (rule BV_correct) +qed + end diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Sat Mar 09 20:39:19 2002 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Sat Mar 09 20:39:46 2002 +0100 @@ -158,6 +158,14 @@ apply assumption done +lemma loc_widen_Err [dest]: + "\XT. G \ replicate n Err <=l XT \ XT = replicate n Err" + by (induct n) auto + +lemma approx_loc_Err [iff]: + "approx_loc G hp (replicate n v) (replicate n Err)" + by (induct n) auto + lemma approx_loc_subst: "\ approx_loc G hp loc LT; approx_val G hp x X \ \ approx_loc G hp (loc[idx:=x]) (LT[idx:=X])" @@ -280,10 +288,19 @@ apply (simp del: split_paired_All) done -lemma preallocated_newref: - "\ hp oref = None; preallocated hp \ \ preallocated (hp(oref\obj))" - by (unfold preallocated_def) auto +lemma + assumes none: "hp oref = None" and alloc: "preallocated hp" + shows preallocated_newref: "preallocated (hp(oref\obj))" +proof (cases oref) + case (XcptRef x) + with none alloc have "False" by (auto elim: preallocatedE [of _ x]) + thus ?thesis .. +next + case (Loc l) + with alloc show ?thesis by (simp add: preallocated_def) +qed + section {* correct-frames *} lemmas [simp del] = fun_upd_apply diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/JVM/JVMExceptions.thy --- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Sat Mar 09 20:39:19 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Sat Mar 09 20:39:46 2002 +0100 @@ -50,17 +50,20 @@ text {* - System exceptions are allocated in all heaps, - and they don't carry any information other than their type: + System exceptions are allocated in all heaps: *} constdefs preallocated :: "aheap \ bool" - "preallocated hp \ \x. hp (XcptRef x) = Some (Xcpt x, empty)" + "preallocated hp \ \x. \fs. hp (XcptRef x) = Some (Xcpt x, fs)" -lemma preallocated_iff [iff]: - "preallocated hp \ hp (XcptRef x) = Some (Xcpt x, empty)" +lemma preallocatedD: + "preallocated hp \ \fs. hp (XcptRef x) = Some (Xcpt x, fs)" by (unfold preallocated_def) fast +lemma preallocatedE [elim?]: + "preallocated hp \ (\fs. hp (XcptRef x) = Some (Xcpt x, fs) \ P hp) \ P hp" + by (fast dest: preallocatedD) + lemma cname_of_xcp: "raise_system_xcpt b x = Some xcp \ preallocated hp \ cname_of (hp::aheap) xcp = Xcpt x" @@ -70,9 +73,18 @@ by (simp add: raise_system_xcpt_def split: split_if_asm) moreover assume "preallocated hp" - hence "hp (XcptRef x) = Some (Xcpt x, empty)" .. + then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" .. ultimately show ?thesis by simp qed +lemma preallocated_start: + "preallocated (start_heap G)" + apply (unfold preallocated_def) + apply (unfold start_heap_def) + apply (rule allI) + apply (case_tac x) + apply (auto simp add: blank_def) + done + end diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/JVM/JVMExec.thy --- a/src/HOL/MicroJava/JVM/JVMExec.thy Sat Mar 09 20:39:19 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Sat Mar 09 20:39:46 2002 +0100 @@ -36,4 +36,16 @@ exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" ("_ \ _ -jvm\ _" [61,61,61]60) +text {* + The start configuration of the JVM: in the start heap, we call a + method @{text m} of class @{text C} in program @{text G}. The + @{text this} pointer of the frame is set to @{text Null} to simulate + a static method invokation. +*} +constdefs + start_state :: "jvm_prog \ cname \ mname \ jvm_state" + "start_state G C m \ + let (C',rT,mxs,mxl,ins,et) = the (method (G,C) (m,[])) in + (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])" + end diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/JVM/JVMListExample.thy --- a/src/HOL/MicroJava/JVM/JVMListExample.thy Sat Mar 09 20:39:19 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Sat Mar 09 20:39:46 2002 +0100 @@ -14,7 +14,6 @@ makelist_name :: mname val_nam :: vnam next_nam :: vnam - test_name_loc :: loc_ constdefs list_name :: cname @@ -87,15 +86,6 @@ E :: jvm_prog "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]" - start_heap :: aheap - "start_heap == empty (XcptRef NullPointer \ (Xcpt NullPointer, empty)) - (XcptRef ClassCast \ (Xcpt ClassCast, empty)) - (XcptRef OutOfMemory \ (Xcpt OutOfMemory, empty)) - (Loc test_name_loc \ (test_name, empty))" - - start_state :: jvm_state - "start_state == - (None, start_heap, [([], [Addr (Loc test_name_loc), arbitrary, arbitrary], test_name, (makelist_name, []), 0)])" types_code cnam ("string") @@ -112,8 +102,6 @@ "arbitrary" :: "val" ("{* Unit *}") "arbitrary" :: "cname" ("Object") - "test_name_loc" ("0") - "list_nam" ("\"list\"") "test_nam" ("\"test\"") "append_name" ("\"append\"") @@ -130,7 +118,7 @@ subsection {* Single step execution *} generate_code - test = "exec (E, start_state)" + test = "exec (E, start_state E test_name makelist_name)" ML {* test *} ML {* exec (E, the it) *} diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/JVM/JVMState.thy --- a/src/HOL/MicroJava/JVM/JVMState.thy Sat Mar 09 20:39:19 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMState.thy Sat Mar 09 20:39:46 2002 +0100 @@ -46,6 +46,16 @@ jvm_state = "val option \ aheap \ frame list" -- "exception flag, heap, frames" +text {* a new, blank object with default values in all fields: *} +constdefs + blank :: "'c prog \ cname \ obj" + "blank G C \ (C,init_vars (fields(G,C)))" + + start_heap :: "'c prog \ aheap" + "start_heap G \ empty (XcptRef NullPointer \ blank G (Xcpt NullPointer)) + (XcptRef ClassCast \ blank G (Xcpt ClassCast)) + (XcptRef OutOfMemory \ blank G (Xcpt OutOfMemory))" + section {* Lemmas *} lemma new_AddrD: @@ -68,6 +78,6 @@ assume "snd (new_Addr hp) = Some xcp" ultimately show ?thesis by (auto dest: new_AddrD) -qed - +qed + end \ No newline at end of file