--- a/src/HOL/IsaMakefile Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 26 15:45:32 2002 +0100
@@ -468,7 +468,7 @@
MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
- MicroJava/BV/Kildall_Lift.thy \
+ MicroJava/BV/Kildall_Lift.thy MicroJava/BV/BVExample.thy \
MicroJava/document/root.bib MicroJava/document/root.tex \
MicroJava/document/introduction.tex
@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Feb 26 15:45:32 2002 +0100
@@ -0,0 +1,377 @@
+(* Title: HOL/MicroJava/BV/BVExample.thy
+ ID: $Id$
+ Author: Gerwin Klein
+*)
+
+header {* Example Welltypings *}
+
+theory BVExample = JVMListExample + Correct:
+
+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: "list_nam \<noteq> test_nam"
+ distinct_fields: "val_nam \<noteq> next_nam"
+
+text {* Shorthands for definitions 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 = SystemClasses_def ObjectC_def NullPointerC_def
+ OutOfMemoryC_def ClassCastC_def
+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_Object [simp]:
+ "class E Object = Some (arbitrary, [],[])"
+ by (simp add: class_def system_defs E_def)
+
+lemma class_NullPointer [simp]:
+ "class E (Xcpt NullPointer) = Some (Object, [], [])"
+ by (simp add: class_def system_defs E_def)
+
+lemma class_OutOfMemory [simp]:
+ "class E (Xcpt OutOfMemory) = Some (Object, [], [])"
+ by (simp add: class_def system_defs E_def)
+
+lemma class_ClassCast [simp]:
+ "class E (Xcpt ClassCast) = Some (Object, [], [])"
+ by (simp add: class_def system_defs E_def)
+
+lemma class_list [simp]:
+ "class E list_name = Some list_class"
+ by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
+
+lemma class_test [simp]:
+ "class E test_name = Some test_class"
+ by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
+
+lemma E_classes [simp]:
+ "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer,
+ Xcpt ClassCast, Xcpt OutOfMemory, Object}"
+ by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
+
+text {* The subclass releation spelled out: *}
+lemma subcls1:
+ "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
+ (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
+ apply (simp add: subcls1_def2)
+ apply (simp add: name_defs class_defs system_defs E_def class_def)
+ apply (auto split: split_if_asm)
+ done
+
+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 distinct_classes)
+ done
+
+lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
+ apply (rule finite_acyclic_wf_converse)
+ apply (simp add: subcls1)
+ apply (rule acyclic_subcls1_E)
+ done
+
+text {* Method and field lookup: *}
+lemma method_Object [simp]:
+ "method (E, Object) = empty"
+ by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
+
+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
+ 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
+ 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, Object) = []"
+ by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
+
+lemma [simp]: "fields (E, Xcpt NullPointer) = []"
+ by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
+
+lemma [simp]: "fields (E, Xcpt ClassCast) = []"
+ by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
+
+lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
+ by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
+
+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)
+ apply arith
+ 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 -
+ have "unique E"
+ by (simp add: system_defs E_def class_defs name_defs distinct_classes)
+ moreover
+ have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
+ hence "wf_syscls E" by (rule wf_syscls)
+ moreover
+ have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
+ moreover
+ have "wf_cdecl ?mb E NullPointerC"
+ by (auto elim: notin_rtrancl
+ simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
+ moreover
+ have "wf_cdecl ?mb E ClassCastC"
+ by (auto elim: notin_rtrancl
+ simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
+ moreover
+ have "wf_cdecl ?mb E OutOfMemoryC"
+ by (auto elim: notin_rtrancl
+ simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
+ moreover
+ have "wf_cdecl ?mb E (list_name, list_class)"
+ apply (auto elim!: notin_rtrancl
+ simp add: wf_cdecl_def wf_fdecl_def list_class_def
+ wf_mdecl_def wf_mhead_def subcls1)
+ apply (auto simp add: name_defs distinct_classes distinct_fields)
+ done
+ moreover
+ have "wf_cdecl ?mb E (test_name, test_class)"
+ apply (auto elim!: notin_rtrancl
+ simp add: wf_cdecl_def wf_fdecl_def test_class_def
+ wf_mdecl_def wf_mhead_def subcls1)
+ apply (auto simp add: name_defs distinct_classes distinct_fields)
+ done
+ ultimately
+ show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
+qed
+
+section "Welltypings"
+text {*
+ We show welltypings of the methods @{term append_name} in class @{term list_name},
+ and @{term makelist_name} in class @{term test_name}:
+*}
+lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
+declare appInvoke [simp del]
+
+constdefs
+ phi_append :: method_type ("\<phi>\<^sub>a")
+ "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [
+ ( [], [Class list_name, Class list_name]),
+ ( [Class list_name], [Class list_name, Class list_name]),
+ ( [Class list_name], [Class list_name, Class list_name]),
+ ( [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], [Class list_name, Class list_name]),
+ ( [Class list_name, Class list_name], [Class list_name, Class list_name]),
+ ( [PrimT Void], [Class list_name, Class list_name]),
+ ( [Class Object], [Class list_name, Class list_name]),
+ ( [], [Class list_name, Class list_name]),
+ ( [Class list_name], [Class list_name, Class list_name]),
+ ( [Class list_name, Class list_name], [Class list_name, Class list_name]),
+ ( [], [Class list_name, Class list_name]),
+ ( [PrimT Void], [Class list_name, Class list_name])]"
+
+lemma wt_append [simp]:
+ "wt_method E list_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)
+ apply clarify
+ apply (elim pc_end pc_next pc_0)
+ apply simp
+ apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
+ apply simp
+ apply simp
+ apply (fastsimp simp add: sup_state_conv subcls1)
+ apply simp
+ apply (simp add: app_def xcpt_app_def)
+ apply simp
+ apply simp
+ apply simp
+ apply (simp add: match_exception_entry_def)
+ apply (simp add: match_exception_entry_def)
+ apply simp
+ apply simp
+ done
+
+text {* Some shorthands to make the welltyping of method @{term
+makelist_name} easier to read *}
+syntax
+ list :: ty
+ test :: ty
+translations
+ "list" == "Class list_name"
+ "test" == "Class test_name"
+
+constdefs
+ phi_makelist :: method_type ("\<phi>\<^sub>m")
+ "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [
+ ( [], [OK test, Err , Err ]),
+ ( [list], [OK test, Err , Err ]),
+ ( [list, list], [OK test, Err , Err ]),
+ ( [list], [OK list, Err , Err ]),
+ ( [PrimT Integer, list], [OK list, Err , Err ]),
+ ( [], [OK list, Err , Err ]),
+ ( [list], [OK list, Err , Err ]),
+ ( [list, list], [OK list, Err , Err ]),
+ ( [list], [OK list, OK list, Err ]),
+ ( [PrimT Integer, list], [OK list, OK list, Err ]),
+ ( [], [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]),
+ ( [PrimT Integer, 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]),
+ ( [PrimT Void], [OK list, OK list, OK list]),
+ ( [list, PrimT Void], [OK list, OK list, OK list]),
+ ( [list, list, PrimT Void], [OK list, OK list, OK list]),
+ ( [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
+ ( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
+
+lemma wt_makelist [simp]:
+ "wt_method E test_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_of)
+ apply (simp add: wt_instr_def)
+ apply clarify
+ apply (elim pc_end pc_next pc_0)
+ apply (simp add: match_exception_entry_def)
+ apply simp
+ apply simp
+ apply simp
+ apply (simp add: match_exception_entry_def)
+ apply (simp add: match_exception_entry_def)
+ apply simp
+ apply simp
+ apply simp
+ apply (simp add: match_exception_entry_def)
+ apply (simp add: match_exception_entry_def)
+ apply simp
+ apply simp
+ apply simp
+ apply (simp add: match_exception_entry_def)
+ apply (simp add: match_exception_entry_def)
+ apply simp
+ apply (simp add: app_def xcpt_app_def)
+ apply simp
+ apply simp
+ apply (simp add: app_def xcpt_app_def)
+ apply simp
+ apply simp
+ done
+
+text {* The whole program is welltyped: *}
+constdefs
+ Phi :: prog_type ("\<Phi>")
+ "\<Phi> C sig \<equiv> 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 []"
+
+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 Phi_def)
+ apply auto
+ done
+
+
+section "Conformance"
+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)
+ done
+
+end
\ No newline at end of file
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Feb 26 15:45:32 2002 +0100
@@ -114,6 +114,14 @@
qed
qed
+lemma match_et_imp_match:
+ "match_exception_table G X pc et = Some handler
+ \<Longrightarrow> match G X pc et = [X]"
+ apply (simp add: match_some_entry)
+ apply (induct et)
+ apply (auto split: split_if_asm)
+ done
+
text {*
We can prove separately that the recursive search for exception
handlers (@{text find_handler}) in the frame stack results in
@@ -356,7 +364,7 @@
phi': "phi C sig ! handler = Some (ST', LT')" and
less: "G \<turnstile> ([Class (Xcpt OutOfMemory)], LT) <=s (ST', LT')" and
pc': "handler < length ins"
- by (simp add: xcpt_eff_def) blast
+ by (simp add: xcpt_eff_def match_et_imp_match) blast
note phi'
moreover
{ from xcp prehp
@@ -386,7 +394,7 @@
phi': "phi C sig ! handler = Some (ST', LT')" and
less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
pc': "handler < length ins"
- by (simp add: xcpt_eff_def) blast
+ by (simp add: xcpt_eff_def match_et_imp_match) blast
note phi'
moreover
{ from xcp prehp
@@ -416,7 +424,7 @@
phi': "phi C sig ! handler = Some (ST', LT')" and
less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
pc': "handler < length ins"
- by (simp add: xcpt_eff_def) blast
+ by (simp add: xcpt_eff_def match_et_imp_match) blast
note phi'
moreover
{ from xcp prehp
@@ -446,7 +454,7 @@
phi': "phi C sig ! handler = Some (ST', LT')" and
less: "G \<turnstile> ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and
pc': "handler < length ins"
- by (simp add: xcpt_eff_def) blast
+ by (simp add: xcpt_eff_def match_et_imp_match) blast
note phi'
moreover
{ from xcp prehp
--- a/src/HOL/MicroJava/BV/Effect.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Feb 26 15:45:32 2002 +0100
@@ -72,14 +72,24 @@
in
if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')"
+consts
+ match :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list"
+primrec
+ "match G X pc [] = []"
+ "match G X pc (e#es) =
+ (if match_exception_entry G X pc e then [X] else match G X pc es)"
+
+lemma match_some_entry:
+ "match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G X pc e then [X] else [])"
+ by (induct et) auto
consts
xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table => cname list"
recdef xcpt_names "{}"
- "xcpt_names (Getfield F C, G, pc, et) = [Xcpt NullPointer]"
- "xcpt_names (Putfield F C, G, pc, et) = [Xcpt NullPointer]"
- "xcpt_names (New C, G, pc, et) = [Xcpt OutOfMemory]"
- "xcpt_names (Checkcast C, G, pc, et) = [Xcpt ClassCast]"
+ "xcpt_names (Getfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et"
+ "xcpt_names (Putfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et"
+ "xcpt_names (New C, G, pc, et) = match G (Xcpt OutOfMemory) pc et"
+ "xcpt_names (Checkcast C, G, pc, et) = match G (Xcpt ClassCast) pc et"
"xcpt_names (Throw, G, pc, et) = match_any G pc et"
"xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et"
"xcpt_names (i, G, pc, et) = []"
@@ -214,23 +224,26 @@
lemma appGetField[simp]:
"(app (Getfield F C) G maxs rT pc et (Some s)) =
(\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>
- field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C) \<and> is_class G (Xcpt NullPointer))"
+ field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C) \<and> (\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x))"
by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
lemma appPutField[simp]:
"(app (Putfield F C) G maxs rT pc et (Some s)) =
(\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and>
- field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT' \<and> is_class G (Xcpt NullPointer))"
+ field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT' \<and>
+ (\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x))"
by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
lemma appNew[simp]:
"(app (New C) G maxs rT pc et (Some s)) =
- (\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and> is_class G (Xcpt OutOfMemory))"
+ (\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and>
+ (\<forall>x \<in> set (match G (Xcpt OutOfMemory) pc et). is_class G x))"
by (cases s, simp)
lemma appCheckcast[simp]:
"(app (Checkcast C) G maxs rT pc et (Some s)) =
- (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and> is_class G (Xcpt ClassCast))"
+ (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and>
+ (\<forall>x \<in> set (match G (Xcpt ClassCast) pc et). is_class G x))"
by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
lemma appPop[simp]:
--- a/src/HOL/MicroJava/BV/EffectMono.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Tue Feb 26 15:45:32 2002 +0100
@@ -151,7 +151,7 @@
"is_class G cname" and
oT: "G\<turnstile> oT\<preceq> (Class cname)" and
vT: "G\<turnstile> vT\<preceq> b" and
- xc: "is_class G (Xcpt NullPointer)"
+ xc: "Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)"
by force
moreover
from s1 G
--- a/src/HOL/MicroJava/BV/JVM.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Tue Feb 26 15:45:32 2002 +0100
@@ -107,14 +107,14 @@
apply clarsimp
apply (erule disjE)
apply (fastsimp dest: field_fields fields_is_type)
- apply simp
+ apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp
apply clarsimp
apply (erule disjE)
apply fastsimp
- apply simp
+ apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp
--- a/src/HOL/MicroJava/J/Conform.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Tue Feb 26 15:45:32 2002 +0100
@@ -165,14 +165,13 @@
apply auto
done
-lemma non_np_objD: "!!G. [|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; C \<noteq> Object|] ==>
+lemma non_np_objD: "!!G. [|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C|] ==>
(\<exists>a C' fs. a' = Addr a \<and> h a = Some (C',fs) \<and> G\<turnstile>C'\<preceq>C C)"
apply (fast dest: non_npD)
done
lemma non_np_objD' [rule_format (no_asm)]:
"a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t -->
- (\<forall>C. t = ClassT C --> C \<noteq> Object) -->
(\<exists>a C fs. a' = Addr a \<and> h a = Some (C,fs) \<and> G\<turnstile>Class C\<preceq>RefT t)"
apply(rule_tac "y" = "t" in ref_ty.exhaust)
apply (fast dest: conf_NullTD)
--- a/src/HOL/MicroJava/J/Decl.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Tue Feb 26 15:45:32 2002 +0100
@@ -23,11 +23,6 @@
'c prog = "'c cdecl list" -- "program"
-constdefs
- ObjectC :: "'c cdecl" -- "decl of root class"
- "ObjectC \<equiv> (Object, (arbitrary, [], []))"
-
-
translations
"fdecl" <= (type) "vname \<times> ty"
"sig" <= (type) "mname \<times> ty list"
--- a/src/HOL/MicroJava/J/Example.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Tue Feb 26 15:45:32 2002 +0100
@@ -6,7 +6,7 @@
header {* \isaheader{Example MicroJava Program} *}
-theory Example = Eval:
+theory Example = SystemClasses + Eval:
text {*
The following example MicroJava program includes:
@@ -72,12 +72,17 @@
axioms
Base_not_Object: "Base \<noteq> Object"
Ext_not_Object: "Ext \<noteq> Object"
- e_not_This: "e \<noteq> This"
+ Base_not_Xcpt: "Base \<noteq> Xcpt z"
+ Ext_not_Xcpt: "Ext \<noteq> Xcpt z"
+ e_not_This: "e \<noteq> This"
declare Base_not_Object [simp] Ext_not_Object [simp]
+declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp]
declare e_not_This [simp]
-declare Base_not_Object [THEN not_sym, simp]
-declare Ext_not_Object [THEN not_sym, simp]
+declare Base_not_Object [symmetric, simp]
+declare Ext_not_Object [symmetric, simp]
+declare Base_not_Xcpt [symmetric, simp]
+declare Ext_not_Xcpt [symmetric, simp]
consts
foo_Base:: java_mb
@@ -119,7 +124,7 @@
translations
"NP" == "NullPointer"
- "tprg" == "[ObjectC, BaseC, ExtC]"
+ "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
"obj1" <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
((vee, Ext )\<mapsto>Intg 0))"
"s0" == " Norm (empty, empty)"
@@ -142,11 +147,26 @@
apply (simp (no_asm))
done
+lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
lemma class_tprg_Base [simp]:
"class tprg Base = Some (Object,
[(vee, PrimT Boolean)],
[((foo, [Class Base]), Class Base, foo_Base)])"
-apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
apply (simp (no_asm))
done
@@ -174,8 +194,8 @@
done
lemma class_tprgD:
-"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext"
-apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory"
+apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
apply (auto split add: split_if_asm simp add: map_of_Cons)
done
@@ -188,7 +208,7 @@
done
lemma unique_classes: "unique tprg"
-apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def)
+apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
done
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
@@ -278,6 +298,30 @@
apply (simp (no_asm))
done
+lemma wf_NP:
+"wf_cdecl wf_java_mdecl tprg NullPointerC"
+apply (unfold wf_cdecl_def wf_fdecl_def NullPointerC_def)
+apply (simp add: class_def)
+apply (fold NullPointerC_def class_def)
+apply auto
+done
+
+lemma wf_OM:
+"wf_cdecl wf_java_mdecl tprg OutOfMemoryC"
+apply (unfold wf_cdecl_def wf_fdecl_def OutOfMemoryC_def)
+apply (simp add: class_def)
+apply (fold OutOfMemoryC_def class_def)
+apply auto
+done
+
+lemma wf_CC:
+"wf_cdecl wf_java_mdecl tprg ClassCastC"
+apply (unfold wf_cdecl_def wf_fdecl_def ClassCastC_def)
+apply (simp add: class_def)
+apply (fold ClassCastC_def class_def)
+apply auto
+done
+
lemma wf_BaseC:
"wf_cdecl wf_java_mdecl tprg BaseC"
apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
@@ -298,10 +342,14 @@
apply auto
done
+lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)
+
lemma wf_tprg:
"wf_prog wf_java_mdecl tprg"
apply (unfold wf_prog_def Let_def)
-apply(simp add: wf_ObjectC wf_BaseC wf_ExtC unique_classes)
+apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
+apply (rule wf_syscls)
+apply (simp add: SystemClasses_def)
done
lemma appl_methds_foo_Base:
--- a/src/HOL/MicroJava/J/JListExample.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Tue Feb 26 15:45:32 2002 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/MicroJava/JVM/JVMListExample.thy
+(* Title: HOL/MicroJava/J/JListExample.thy
ID: $Id$
Author: Stefan Berghofer
*)
header {* \isaheader{Example for generating executable code from Java semantics} *}
-theory JListExample = Eval:
+theory JListExample = Eval + SystemClasses:
ML {* Syntax.ambiguity_level := 100000 *}
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Feb 26 15:45:32 2002 +0100
@@ -60,8 +60,7 @@
apply( erule conjE)
apply( simp)
apply( drule non_np_objD)
-apply( assumption)
-apply( force)
+apply( assumption)
apply( clarify)
apply( simp (no_asm_use))
apply( frule (1) hext_objD)
@@ -121,7 +120,6 @@
apply( drule max_spec2mheads)
apply( clarify)
apply( drule (2) non_np_objD')
-apply( clarsimp)
apply( clarsimp)
apply( frule (1) hext_objD)
apply( clarsimp)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/SystemClasses.thy Tue Feb 26 15:45:32 2002 +0100
@@ -0,0 +1,32 @@
+(* Title: HOL/MicroJava/J/SystemClasses.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2002 Technische Universitaet Muenchen
+*)
+
+header {* \isaheader{System Classes} *}
+
+theory SystemClasses = Decl:
+
+text {*
+ This theory provides definitions for the @{text Object} class,
+ and the system exceptions.
+*}
+
+constdefs
+ ObjectC :: "'c cdecl"
+ "ObjectC \<equiv> (Object, (arbitrary,[],[]))"
+
+ NullPointerC :: "'c cdecl"
+ "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+
+ ClassCastC :: "'c cdecl"
+ "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+
+ OutOfMemoryC :: "'c cdecl"
+ "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+
+ SystemClasses :: "'c cdecl list"
+ "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+
+end
--- a/src/HOL/MicroJava/J/Type.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Tue Feb 26 15:45:32 2002 +0100
@@ -21,7 +21,7 @@
datatype cname
= Object
| Xcpt xcpt
- | Cname cname
+ | Cname cnam
typedecl vnam -- "variable or field name"
typedecl mname -- "method name"
--- a/src/HOL/MicroJava/J/WellForm.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Tue Feb 26 15:45:32 2002 +0100
@@ -6,7 +6,7 @@
header {* \isaheader{Well-formedness of Java programs} *}
-theory WellForm = TypeRel:
+theory WellForm = TypeRel + SystemClasses:
text {*
for static checks on expressions and statements, see WellType.
@@ -45,9 +45,12 @@
(\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
+ wf_syscls :: "'c prog => bool"
+"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
+
wf_prog :: "'c wf_mb => 'c prog => bool"
-"wf_prog wf_mb G ==
- let cs = set G in ObjectC \<in> cs \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
+"wf_prog wf_mb G ==
+ let cs = set G in wf_syscls G \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
lemma class_wf:
"[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
@@ -57,9 +60,9 @@
done
lemma class_Object [simp]:
- "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
-apply (unfold wf_prog_def ObjectC_def class_def)
-apply (auto intro: map_of_SomeI)
+ "wf_prog wf_mb G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
+apply (unfold wf_prog_def wf_syscls_def class_def)
+apply (auto simp: map_of_SomeI)
done
lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
@@ -158,20 +161,12 @@
lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
-lemma method_Object [simp]: "wf_prog wf_mb G ==> method (G,Object) = empty"
-apply(subst method_rec)
-apply auto
-done
-
-lemma fields_Object [simp]: "wf_prog wf_mb G ==> fields (G,Object) = []"
-apply(subst fields_rec)
-apply auto
-done
-
-lemma field_Object [simp]: "wf_prog wf_mb G ==> field (G,Object) = empty"
-apply (unfold field_def)
-apply(simp (no_asm_simp))
-done
+lemma method_Object [simp]:
+ "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> wf_prog wf_mb G \<Longrightarrow> D = Object"
+ apply (frule class_Object, clarify)
+ apply (drule method_rec, assumption)
+ apply (auto dest: map_of_SomeD)
+ done
lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
apply(erule subcls1_induct)
@@ -190,7 +185,10 @@
\<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
apply( erule subcls1_induct)
apply( assumption)
-apply( simp (no_asm_simp))
+apply( frule class_Object)
+apply( clarify)
+apply( frule fields_rec, assumption)
+apply( fastsimp)
apply( tactic "safe_tac HOL_cs")
apply( subst fields_rec)
apply( assumption)
@@ -216,8 +214,16 @@
"[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
apply( erule subcls1_induct)
apply( assumption)
-apply( safe dest!: wf_cdecl_supD)
-apply( simp (no_asm_simp))
+apply( frule class_Object)
+apply( clarify)
+apply( frule fields_rec, assumption)
+apply( drule class_wf, assumption)
+apply( simp add: wf_cdecl_def)
+apply( rule unique_map_inj)
+apply( simp)
+apply( rule injI)
+apply( simp)
+apply( safe dest!: wf_cdecl_supD)
apply( drule subcls1_wfD)
apply( assumption)
apply( subst fields_rec)
@@ -269,7 +275,16 @@
--> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
apply( erule subcls1_induct)
apply( assumption)
-apply( force)
+apply( clarify)
+apply( frule class_Object)
+apply( clarify)
+apply( frule method_rec, assumption)
+apply( drule class_wf, assumption)
+apply( simp add: wf_cdecl_def)
+apply( drule map_of_SomeD)
+apply( subgoal_tac "md = Object")
+apply( fastsimp)
+apply( fastsimp)
apply( clarify)
apply( frule_tac C = C in method_rec)
apply( assumption)
@@ -334,7 +349,10 @@
"wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code)
--> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
apply (erule (1) subcls1_induct)
- apply (simp)
+ apply clarify
+ apply (frule method_Object, assumption)
+ apply hypsubst
+ apply simp
apply (erule conjE)
apply (subst method_rec)
apply (assumption)
@@ -377,7 +395,12 @@
"[|is_class G C; wf_prog wf_mb G|] ==>
\<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
apply( erule (1) subcls1_induct)
-apply( simp (no_asm_simp))
+apply( frule class_Object)
+apply( clarify)
+apply( frule fields_rec, assumption)
+apply( drule class_wf, assumption)
+apply( simp add: wf_cdecl_def wf_fdecl_def)
+apply( fastsimp)
apply( subst fields_rec)
apply( fast)
apply( assumption)
@@ -405,24 +428,52 @@
"[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
proof -
- assume wf: "wf_prog wf_mb G"
- assume C: "(C,S,fs,mdecls) \<in> set G"
-
- assume m: "(sig,rT,code) \<in> set mdecls"
+ assume wf: "wf_prog wf_mb G" and C: "(C,S,fs,mdecls) \<in> set G" and
+ m: "(sig,rT,code) \<in> set mdecls"
moreover
- from wf have "class G Object = Some (arbitrary, [], [])" by simp
- moreover
- from wf C have c: "class G C = Some (S,fs,mdecls)"
+ from wf C have "class G C = Some (S,fs,mdecls)"
by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
+ moreover
+ from wf C
+ have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
+ hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)
+ with m
+ have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
+ by (force intro: map_of_SomeI)
ultimately
- have O: "C \<noteq> Object" by auto
-
- from wf C have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
- hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)
- with m have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
- by (force intro: map_of_SomeI)
- with wf C m c O
show ?thesis by (auto simp add: is_class_def dest: method_rec)
qed
+
+lemma wf_mb'E:
+ "\<lbrakk> wf_prog wf_mb G; \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set G; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_mb' G C m \<rbrakk>
+ \<Longrightarrow> wf_prog wf_mb' G"
+ apply (simp add: wf_prog_def)
+ apply auto
+ apply (simp add: wf_cdecl_def wf_mdecl_def)
+ apply safe
+ apply (drule bspec, assumption) apply simp
+ apply (drule bspec, assumption) apply simp
+ apply (drule bspec, assumption) apply simp
+ apply clarify apply (drule bspec, assumption) apply simp
+ apply (drule bspec, assumption) apply simp
+ apply (drule bspec, assumption) apply simp
+ apply (drule bspec, assumption) apply simp
+ apply (drule bspec, assumption) apply simp
+ apply (drule bspec, assumption) apply simp
+ apply clarify apply (drule bspec, assumption)+ apply simp
+ done
+
+
+lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast
+
+lemma wf_syscls:
+ "set SystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G"
+ apply (drule fst_mono)
+ apply (simp add: SystemClasses_def wf_syscls_def)
+ apply (simp add: ObjectC_def)
+ apply (rule allI, case_tac x)
+ apply (auto simp add: NullPointerC_def ClassCastC_def OutOfMemoryC_def)
+ done
+
end
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Feb 26 15:45:32 2002 +0100
@@ -5,49 +5,56 @@
header {* \isaheader{Example for generating executable code from JVM semantics} *}
-theory JVMListExample = JVMExec:
+theory JVMListExample = SystemClasses + JVMExec:
consts
- list_name :: cname
- test_name :: cname
+ list_nam :: cnam
+ test_nam :: cnam
append_name :: mname
makelist_name :: mname
val_nam :: vnam
next_nam :: vnam
+ test_name_loc :: loc_
constdefs
+ list_name :: cname
+ "list_name == Cname list_nam"
+
+ test_name :: cname
+ "test_name == Cname test_nam"
+
val_name :: vname
"val_name == VName val_nam"
next_name :: vname
"next_name == VName next_nam"
- list_class :: "jvm_method class"
- "list_class ==
- (Object,
- [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
- [((append_name, [RefT (ClassT list_name)]), PrimT Integer,
- (0, 0,
+ append_ins :: bytecode
+ "append_ins ==
[Load 0,
Getfield next_name list_name,
Dup,
LitPush Null,
Ifcmpeq 4,
- Load 1,
- Invoke list_name append_name [RefT (ClassT list_name)],
+ Load 1,
+ Invoke list_name append_name [Class list_name],
Return,
Pop,
Load 0,
Load 1,
Putfield next_name list_name,
LitPush Unit,
- Return],[]))])"
+ Return]"
- test_class :: "jvm_method class"
- "test_class ==
- (Object, [],
- [((makelist_name, []), PrimT Integer,
- (0, 3,
+ list_class :: "jvm_method class"
+ "list_class ==
+ (Object,
+ [(val_name, PrimT Integer), (next_name, Class list_name)],
+ [((append_name, [Class list_name]), PrimT Void,
+ (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
+
+ make_list_ins :: bytecode
+ "make_list_ins ==
[New list_name,
Dup,
Store 0,
@@ -65,22 +72,33 @@
Putfield val_name list_name,
Load 0,
Load 1,
- Invoke list_name append_name [RefT (ClassT list_name)],
+ Invoke list_name append_name [Class list_name],
Load 0,
Load 2,
- Invoke list_name append_name [RefT (ClassT list_name)],
+ Invoke list_name append_name [Class list_name],
LitPush Unit,
- Return],[]))])"
+ Return]"
+
+ test_class :: "jvm_method class"
+ "test_class ==
+ (Object, [],
+ [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
- example_prg :: jvm_prog
- "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"
+ 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, empty, [([], Unit # Unit # Unit # [], test_name, (makelist_name, []), 0)])"
+ (None, start_heap, [([], [Addr (Loc test_name_loc), arbitrary, arbitrary], test_name, (makelist_name, []), 0)])"
types_code
- cname ("string")
+ cnam ("string")
vnam ("string")
mname ("string")
loc_ ("int")
@@ -92,11 +110,12 @@
"arbitrary" ("(raise ERROR)")
"arbitrary" :: "val" ("{* Unit *}")
- "arbitrary" :: "cname" ("\"\"")
+ "arbitrary" :: "cname" ("Object")
- "Object" ("\"Object\"")
- "list_name" ("\"list\"")
- "test_name" ("\"test\"")
+ "test_name_loc" ("0")
+
+ "list_nam" ("\"list\"")
+ "test_nam" ("\"test\"")
"append_name" ("\"append\"")
"makelist_name" ("\"makelist\"")
"val_nam" ("\"val\"")
@@ -110,62 +129,62 @@
subsection {* Single step execution *}
-generate_code
- test = "exec (example_prg, start_state)"
+generate_code
+ test = "exec (E, start_state)"
ML {* test *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
end
\ No newline at end of file
--- a/src/HOL/MicroJava/ROOT.ML Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML Tue Feb 26 15:45:32 2002 +0100
@@ -10,8 +10,9 @@
use_thy "Example";
use_thy "JListExample";
use_thy "JVMListExample";
+use_thy "JVM";
use_thy "BVSpecTypeSafe";
-use_thy "JVM";
+use_thy "BVExample";
(* momentarily broken:
use_thy "LBVSpec";