--- 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,\<Phi> \<turnstile>JVM start_state \<surd>"
- 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,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
+ apply (rule BV_correct_initial)
+ apply (rule wf_prog)
+ apply simp
+ apply simp
done
end
--- 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]:
+ "\<lbrakk>preallocated hp; xcp = Addr (XcptRef x)\<rbrakk> \<Longrightarrow> 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 \<turnstile> xcp ::\<preceq> 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 \<turnstile> xcp ::\<preceq> 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 \<turnstile> xcp ::\<preceq> 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 \<turnstile> xcp ::\<preceq> 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:
"\<lbrakk> wt_jvm_prog G phi;
G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk>
@@ -1307,4 +1313,45 @@
split: option.splits)
done
+lemma
+ fixes G :: jvm_prog ("\<Gamma>")
+ assumes wf: "wf_prog wf_mb \<Gamma>"
+ shows hconf_start: "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
+ 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 ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
+ shows BV_correct_initial:
+ "wt_jvm_prog \<Gamma> \<Phi> \<Longrightarrow> is_class \<Gamma> C \<Longrightarrow> method (\<Gamma>,C) (m,[]) = Some (C, b)
+ \<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM start_state G C m \<surd>"
+ 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 ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
+ assumes welltyped: "wt_jvm_prog \<Gamma> \<Phi>" and
+ main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ shows typesafe:
+ "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s \<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+proof -
+ from welltyped main_method
+ have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
+ moreover
+ assume "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s"
+ ultimately
+ show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
+qed
+
end
--- 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]:
+ "\<And>XT. G \<turnstile> replicate n Err <=l XT \<Longrightarrow> 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:
"\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
\<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
@@ -280,10 +288,19 @@
apply (simp del: split_paired_All)
done
-lemma preallocated_newref:
- "\<lbrakk> hp oref = None; preallocated hp \<rbrakk> \<Longrightarrow> preallocated (hp(oref\<mapsto>obj))"
- by (unfold preallocated_def) auto
+lemma
+ assumes none: "hp oref = None" and alloc: "preallocated hp"
+ shows preallocated_newref: "preallocated (hp(oref\<mapsto>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
--- 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 \<Rightarrow> bool"
- "preallocated hp \<equiv> \<forall>x. hp (XcptRef x) = Some (Xcpt x, empty)"
+ "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
-lemma preallocated_iff [iff]:
- "preallocated hp \<Longrightarrow> hp (XcptRef x) = Some (Xcpt x, empty)"
+lemma preallocatedD:
+ "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
by (unfold preallocated_def) fast
+lemma preallocatedE [elim?]:
+ "preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp"
+ by (fast dest: preallocatedD)
+
lemma cname_of_xcp:
"raise_system_xcpt b x = Some xcp \<Longrightarrow> preallocated hp
\<Longrightarrow> 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
--- 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"
("_ \<turnstile> _ -jvm\<rightarrow> _" [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 \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state"
+ "start_state G C m \<equiv>
+ 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
--- 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 \<mapsto> (Xcpt NullPointer, empty))
- (XcptRef ClassCast \<mapsto> (Xcpt ClassCast, empty))
- (XcptRef OutOfMemory \<mapsto> (Xcpt OutOfMemory, empty))
- (Loc test_name_loc \<mapsto> (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) *}
--- 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 \<times> aheap \<times> frame list" -- "exception flag, heap, frames"
+text {* a new, blank object with default values in all fields: *}
+constdefs
+ blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
+ "blank G C \<equiv> (C,init_vars (fields(G,C)))"
+
+ start_heap :: "'c prog \<Rightarrow> aheap"
+ "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
+ (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
+ (XcptRef OutOfMemory \<mapsto> 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