Up to index of Isabelle/HOL/jsr
theory BVJSR = JVMSystemClasses + JVMExec + JVM + BVSpecTypeSafe:(* Title: HOL/MicroJava/BV/BVJSR.thy
ID: $Id: BVJSR.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
Author: Gerwin Klein
*)
header {* \isaheader{Example for a program with JSR}\label{sec:JSRExample} *}
theory BVJSR = JVMSystemClasses + JVMExec + JVM + BVSpecTypeSafe:
consts
test_nam :: cnam
m_name :: mname
constdefs
test_name :: cname
"test_name == Cname test_nam"
m_ins :: bytecode
"m_ins \<equiv> [
LitPush (Bool False),
Store 1,
Load 1,
LitPush (Bool False),
Ifcmpeq 6,
LitPush (Intg 1),
Store 3,
Jsr 16,
Load 3,
Return,
LitPush (Intg 2),
Store 2,
Load 1,
LitPush (Bool False),
Ifcmpeq 3,
Jsr 8,
Goto 14,
Jsr 6,
Goto 12,
Store 4,
Jsr 3,
Load 4,
Throw,
Store 5,
Load 1,
LitPush (Bool False),
Ifcmpeq 3,
LitPush (Intg 3),
Store 2,
Ret 5,
LitPush (Intg 4),
Store 2,
Load 2,
Return]"
test_class :: "jvm_method class"
"test_class \<equiv>
(Object, [], [Default_ctor,
((m_name, []), PrimT Integer, (2, 5, m_ins,[(0,19,19,Object)]))])"
E :: jvm_prog
"E == JVMSystemClasses @ [(test_name, test_class)]"
types_code
cnam ("string")
vnam ("string")
mname ("string")
loc_ ("int")
consts_code
"arbitrary" ("(raise ERROR)")
"arbitrary" :: "val × val" ("{* (Unit,Unit) *}")
"arbitrary" :: "val" ("{* Unit *}")
"arbitrary" :: "cname" ("Object")
"test_nam" ("\"test\"")
"m_name" ("\"m\"")
"init" ("\"init\"")
generate_code
test = "c_kil E test_name [] (PrimT Integer) False 5 10 [(0,19,19,Object)] m_ins"
ML "print_depth 100"
ML "test"
section "Setup"
axioms not_init [simp]: "m_name \<noteq> init"
text {* Abbreviations for theorem sets we will have to use often in the
proofs below: *}
lemmas name_defs = test_name_def
lemmas system_defs = JVMSystemClasses_def SystemClassC_defs
lemmas class_defs = 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, [],[Object_ctor])"
by (simp add: class_def system_defs E_def)
lemma class_NullPointer [simp]:
"class E (Xcpt NullPointer) = Some (Object, [], [Default_ctor])"
by (simp add: class_def system_defs E_def)
lemma class_OutOfMemory [simp]:
"class E (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])"
by (simp add: class_def system_defs E_def)
lemma class_ClassCast [simp]:
"class E (Xcpt ClassCast) = Some (Object, [], [Default_ctor])"
by (simp add: class_def system_defs E_def)
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} = {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 = {(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)
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 method_Object [simp]:
"method (E, Object) sig =
(if sig = (init,[]) then
Some (Object, PrimT Void, Suc 0, 0, [LitPush Unit, Return], [])
else None)"
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E] Object_ctor_def)
lemma method_makelist [simp]:
"method (E, test_name) (m_name, []) =
Some (test_name, PrimT Integer, 2, 5, m_ins, [(0,19,19,Object)])"
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 [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)
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
have "unique E"
by (simp add: E_def class_defs name_defs)
moreover
have "set JVMSystemClasses \<subseteq> set E" by (simp add: E_def)
hence "wf_syscls E" by (rule wf_syscls)
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 (test_name, test_class)"
apply (auto elim!: notin_rtrancl
simp add: wf_fdecl_def test_class_def subcls1)
apply (simp add: not_init [symmetric])
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
apply (fast dest: subcls1_wfD [OF _ wf_struct])
done
text {* Some abbreviations for readability *}
syntax
test :: init_ty
intg :: ty
boolean :: ty
translations
"test" == "Init (Class test_name)"
"intg" == "Init (PrimT Integer)"
"boolean" == "Init (PrimT Boolean)"
constdefs
phi_m :: method_type ("\<phi>\<^sub>m")
"\<phi>\<^sub>m \<equiv> map (image (\<lambda>x. (x,False))) [
{( [], [OK test, Err, Err, Err, Err, Err])},
{( [boolean], [OK test, Err, Err, Err, Err, Err])},
{( [], [OK test, OK boolean, Err, Err, Err, Err])},
{( [boolean], [OK test, OK boolean, Err, Err, Err, Err])},
{( [boolean, boolean], [OK test, OK boolean, Err, Err, Err, Err])},
{( [], [OK test, OK boolean, Err, Err, Err, Err])},
{( [intg], [OK test, OK boolean, Err, Err, Err, Err])},
{( [], [OK test, OK boolean, Err, OK intg, Err, Err])},
{( [], [OK test, OK boolean, OK intg, OK intg, Err, OK (Init (RA 8))]),
( [], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))])},
{( [intg], [OK test, OK boolean, OK intg, OK intg, Err, OK (Init (RA 8))]),
( [intg], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))])},
{( [], [OK test, OK boolean, Err, Err, Err, Err])},
{( [intg], [OK test, OK boolean, Err, Err, Err, Err])},
{( [], [OK test, OK boolean, OK intg, Err, Err, Err])},
{( [boolean], [OK test, OK boolean, OK intg, Err, Err, Err])},
{( [boolean, boolean], [OK test, OK boolean, OK intg, Err, Err, Err])},
{( [], [OK test, OK boolean, OK intg, Err, Err, Err])},
{( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))])},
{( [], [OK test, OK boolean, OK intg, Err, Err, Err])},
{( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{},
{},
{},
{},
{( [Init (RA 8)], [OK test, OK boolean, Err, OK intg, Err, Err]),
( [Init (RA 16)], [OK test, OK boolean, OK intg, Err, Err, Err]),
( [Init (RA 18)], [OK test, OK boolean, OK intg, Err, Err, Err])},
{( [], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [boolean], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))]),
( [boolean], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [boolean], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [boolean, boolean], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))]),
( [boolean, boolean], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [boolean, boolean], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [intg], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))]),
( [intg], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [intg], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [], [OK test, OK boolean, OK intg, OK intg, Err, OK (Init (RA 8))]),
( [], [OK test, OK boolean, Err, OK intg, Err, OK (Init (RA 8))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [intg], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [intg], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])},
{( [intg], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 16))]),
( [intg], [OK test, OK boolean, OK intg, Err, Err, OK (Init (RA 18))])}
]"
lemma len: "length m_ins = 34"
by (simp add: m_ins_def nat_number)
lemma wt_m [simp]:
"wt_method E test_name m_name [] (PrimT Integer) 2 5 m_ins [(0,19,19,Object)] \<phi>\<^sub>m"
apply (simp add: wt_method_def len)
apply (rule conjI)
apply (simp add: phi_m_def)
apply (rule conjI)
apply (simp add: check_types_def init_tys_def nat_number phi_m_def)
apply (rule conjI)
apply (simp add: wt_start_def phi_m_def nat_number name_defs)
apply clarify
apply (simp add: nat_number phi_m_def)
apply (elim pc_end pc_next pc_0)
apply (unfold wt_instr_def m_ins_def)
apply (simp_all only: nth_Cons_Suc nth_Cons_0)
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
defer
apply simp
apply simp
apply simp
apply simp
apply (simp add: set_SOME_lists theRA_def nat_number)
apply auto
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 = (m_name, []) then \<phi>\<^sub>m else
if sig = (init,[]) then \<phi>\<^sub>c C else []"
lemma [simp]:
"is_class E C =
(C \<in> {Cname test_nam, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory, 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 (simp_all add: not_init [symmetric])
apply (simp add: name_defs)
apply (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 m_name \<surd>"
apply (rule BV_correct_initial)
apply (rule wf_prog)
apply (auto simp add: is_class_def)
done
end
lemmas name_defs:
test_name == Cname test_nam
lemmas system_defs:
JVMSystemClasses == [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]
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)
ObjectC == ObjectC_decl [Object_ctor]
NullPointerC == NullPointerC_decl [Default_ctor]
OutOfMemoryC == OutOfMemoryC_decl [Default_ctor]
ClassCastC == ClassCastC_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:
test_class ==
(Object, [],
[Default_ctor,
((m_name, []), PrimT Integer, 2, 5, m_ins, [(0, 19, 19, Object)])])
lemma class_Object:
class E Object = Some (arbitrary, [], [Object_ctor])
lemma class_NullPointer:
class E (Xcpt NullPointer) = Some (Object, [], [Default_ctor])
lemma class_OutOfMemory:
class E (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])
lemma class_ClassCast:
class E (Xcpt ClassCast) = Some (Object, [], [Default_ctor])
lemma class_test:
class E test_name = Some test_class
lemma E_classes:
Collect (is_class E) =
{test_name, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory, Object}
lemma subcls1:
subcls1 E =
{(test_name, Object), (Xcpt NullPointer, Object), (Xcpt ClassCast, Object),
(Xcpt OutOfMemory, 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 method_Object:
method (E, Object) sig = (if sig = (init, []) then Some (Object, PrimT Void, Suc 0, 0, [LitPush Unit, Return], []) else None)
lemma method_makelist:
method (E, test_name) (m_name, []) = Some (test_name, PrimT Integer, 2, 5, m_ins, [(0, 19, 19, Object)])
lemma
fields (E, Object) = []
lemma
fields (E, Xcpt NullPointer) = []
lemma
fields (E, Xcpt ClassCast) = []
lemma
fields (E, Xcpt OutOfMemory) = []
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
lemma wf_struct:
wf_prog (%G C mb. True) E
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 len:
length m_ins = 34
lemma wt_m:
wt_method E test_name m_name [] (PrimT Integer) 2 5 m_ins [(0, 19, 19, Object)] \<phi>\<^sub>m
lemma
is_class E C =
(C : {Cname test_nam, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory,
Object})
lemma wf_prog:
wt_jvm_prog E \<Phi>
lemma
E,\<Phi> |-JVM start_state E test_name m_name [ok]