Up to index of Isabelle/Bali4
theory State = TypeRel(* Title: isabelle/Bali/State.thy
ID: $Id: State.thy,v 1.59 2000/08/07 21:07:49 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
State for evaluation of Java expressions and statements
design issues:
* all kinds of objects (class instances, arrays, and class objects)
are handeled via a general object abstraction
* the heap and the map for class objects are combined into a single table
(recall (loc, obj) table × (tname, obj) table ~= (loc + tname, obj) table)
simplifications:
*)
State = TypeRel +
datatype obj_tag = (* tag for generic object *)
CInst tname (* class instance *)
| Arr ty int (* array with component type and length *)
(* | CStat the tag is irrelevant for a class object,
i.e. the static fields of a class *)
types vn = "fspec + int" (* variable name *)
obj = "obj_tag × (vn, val) table" (* generalized object *)
constdefs
the_Arr :: "obj option \<Rightarrow> ty × int × (vn, val) table"
"the_Arr obj \<equiv> \<epsilon>(T,k,t). obj = Some (Arr T k,t)"
upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj"
"upd_obj n v \<equiv> \<lambda>(oi,vs). (oi,vs(n\<mapsto>v))"
obj_ty :: "obj \<Rightarrow> ty"
"obj_ty obj \<equiv> case fst obj of CInst C \<Rightarrow> Class C | Arr T k \<Rightarrow> T.[]"
obj_class :: "obj \<Rightarrow> tname"
"obj_class obj \<equiv> case fst obj of CInst C \<Rightarrow> C | Arr T k \<Rightarrow> Object"
types oref = "loc + tname" (* generalized object reference *)
syntax
Heap :: "loc \<Rightarrow> oref"
Stat :: "tname \<Rightarrow> oref"
translations
"Heap" => "Inl"
"Stat" => "Inr"
constdefs
fields_table :: "prog \<Rightarrow> tname \<Rightarrow> (modi \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table"
"fields_table G C P \<equiv> option_map snd \<circ> table_of([(fn,(m,fT))\<in>fields G C. P m])"
var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table"
"var_tys G oi r \<equiv> case r of Heap a \<Rightarrow> (case oi of
CInst C \<Rightarrow> fields_table G C (Not \<circ> static) (+) empty
| Arr T k \<Rightarrow> empty (+) (\<lambda>i. if #0\<le>i\<and>i<k then Some T else None))
| Stat C \<Rightarrow> fields_table G C static (+) empty"
types globs (* global variables: heap and static variables *)
= "(oref , obj) table"
heap
= "(loc , obj) table"
locals
= "(lname, val) table" (* local variables *)
datatype st = (* pure state, i.e. contents of all variables *)
st globs locals
constdefs
globs :: "st \<Rightarrow> globs"
"globs \<equiv> st_case (\<lambda>g l. g)"
locals :: "st \<Rightarrow> locals"
"locals \<equiv> st_case (\<lambda>g l. l)"
heap :: "st \<Rightarrow> heap"
"heap s \<equiv> globs s \<circ> Heap"
syntax
val_this :: "st \<Rightarrow> val"
lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
translations
"val_this s" == "the (locals s This)"
"lookup_obj s a'" == "the (heap s (the_Addr a'))"
syntax
init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
translations
"init_vals vs" == "option_map default_val \<circ> vs"
constdefs
gupd :: "oref \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')"[10,10]1000)
"gupd r obj \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')"[10,10]1000)
"lupd vn v \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
"upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
set_locals :: "locals \<Rightarrow> st \<Rightarrow> st"
"set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
"init_obj G oi r \<equiv> gupd(r\<mapsto>(oi, init_vals (var_tys G oi r)))"
syntax
init_class_obj :: "prog \<Rightarrow> tname \<Rightarrow> st \<Rightarrow> st"
translations
"init_class_obj G C" == "init_obj G arbitrary (Inr C)"
datatype xcpt (* exception *)
= XcptLoc loc (* location of allocated execption object *)
| StdXcpt xname (* intermediate standard exception, see Eval.thy *)
consts
the_XcptLoc :: "xcpt \<Rightarrow> loc"
the_StdXcpt :: "xcpt \<Rightarrow> xname"
defs
the_XcptLoc_def "the_XcptLoc xc \<equiv> \<epsilon>a. xc = XcptLoc a"
the_StdXcpt_def "the_StdXcpt xc \<equiv> \<epsilon>x. xc = StdXcpt x"
types
xopt = "xcpt option"
constdefs
xcpt_if :: "bool \<Rightarrow> xopt \<Rightarrow> xopt \<Rightarrow> xopt"
"xcpt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
syntax
raise_if :: "bool \<Rightarrow> xname \<Rightarrow> xopt \<Rightarrow> xopt"
np :: "val \<spacespace> \<Rightarrow> xopt \<Rightarrow> xopt"
check_neg:: "val \<spacespace> \<Rightarrow> xopt \<Rightarrow> xopt"
translations
"raise_if c xn" == "xcpt_if c (Some (StdXcpt xn))"
"np v" == "raise_if (v = Null) NullPointer"
"check_neg i'" == "raise_if (the_Intg i'<0) NegArrSize"
types
state = "xopt × st" (* state including exception information *)
syntax
Norm :: "st \<Rightarrow> state"
translations
"Norm s" == "(None,s)"
"xopt" <= (type) "State.xcpt option"
"xopt" <= (type) "xcpt option"
"state" <= (type) "xopt × State.st"
"state" <= (type) "xopt × st"
constdefs
normal :: "state \<Rightarrow> bool"
"normal \<equiv> \<lambda>s. fst s = None"
inited :: "tname \<Rightarrow> globs \<Rightarrow> bool"
"inited C g \<equiv> g (Stat C) \<noteq> None"
initd :: "tname \<Rightarrow> state \<Rightarrow> bool"
"initd C \<equiv> inited C \<circ> globs \<circ> snd"
xupd :: "(xopt \<Rightarrow> xopt) \<Rightarrow> state \<Rightarrow> state"
"xupd f \<equiv> prod_fun f id"
supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
"supd \<equiv> prod_fun id"
syntax
set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state"
restore_lvars :: "state \<Rightarrow> state \<Rightarrow> state"
translations
"set_lvars l" == "supd (set_locals l)"
"restore_lvars s' s" == "set_lvars (locals (snd s')) s"
end
theorem the_Arr_Arr:
the_Arr (Some (Arr T k, cs)) = (T, k, cs)
theorem obj_tagE:
[| !!C. oi = CInst C ==> P; !!T k. oi = Arr T k ==> P |] ==> P
theorem upd_obj_def2:
upd_obj n v (oi, vs) = (oi, vs(n|->v))
theorem obj_ty_eq:
obj_ty (oi, x) = obj_ty (oi, y)
theorem obj_ty_cong:
obj_ty (oi, vs(n|->v)) = obj_ty (oi, vs)
theorem obj_ty_CInst:
obj_ty (CInst C, x) = Class C
theorem obj_ty_Arr:
obj_ty (Arr T i, x) = T.[]
theorem obj_ty_widenD:
G|-obj_ty (oi, vs)<=:RefT t ==> (EX C. oi = CInst C) | (EX T k. oi = Arr T k)
theorem obj_class_CInst:
obj_class (CInst C, fs) = C
theorem obj_class_Arr:
obj_class (Arr T k, fs) = Object
theorem fields_table_SomeI:
[| table_of (fields G C) f = Some (m, T); P m |] ==> fields_table G C P f = Some T
theorem fields_table_SomeD:
fields_table G C P fn = Some T ==> EX m. (fn, m, T) : set (fields G C)
theorem fields_table_SomeD:
[| fields_table G C P fn = Some T; unique (fields G C) |] ==> EX m. table_of (fields G C) fn = Some (m, T)
theorem var_tys_Some_eq:
(var_tys G oi r n = Some T) =
(case r of
Inl a =>
case oi of CInst C => EX nt. n = Inl nt & fields_table G C Not nt = Some T
| Arr t k => EX i. n = Inr i & #0 <= i & i < k & t = T
| Inr C => EX nt. n = Inl nt & fields_table G C id nt = Some T)
theorem globs_def2:
globs (st g l) = g
theorem locals_def2:
locals (st g l) = l
theorem heap_def2:
heap s a = globs s (Inl a)
theorem gupd_def2:
gupd(r\<mapsto>obj) (st g l) = st (g(r|->obj)) l
theorem lupd_def2:
lupd(vn\<mapsto>v) (st g l) = st g (l(vn|->v))
theorem globs_gupd:
globs (gupd(r\<mapsto>obj) s) = globs s(r|->obj)
theorem globs_lupd:
globs (lupd(vn\<mapsto>v) s) = globs s
theorem locals_gupd:
locals (gupd(r\<mapsto>obj) s) = locals s
theorem locals_lupd:
locals (lupd(vn\<mapsto>v) s) = locals s(vn|->v)
theorem globs_upd_gobj_new:
globs s r = None ==> globs (upd_gobj r n v s) = globs s
theorem globs_upd_gobj_upd:
globs s r = Some obj ==> globs (upd_gobj r n v s) = globs s(r|->upd_obj n v obj)
theorem locals_upd_gobj:
locals (upd_gobj r n v s) = locals s
theorem globs_init_obj:
globs (init_obj G oi r s) t = (if t = r then Some (oi, init_vals (var_tys G oi r)) else globs s t)
theorem locals_init_obj:
locals (init_obj G oi r s) = locals s
theorem surjective_st:
st (globs s) (locals s) = s
theorem surjective_st_init_obj:
st (globs (init_obj G oi r s)) (locals s) = init_obj G oi r s
theorem normal_def2:
normal s = (fst s = None)
theorem single_stateE:
ALL Z. Z = s ==> False
theorem state_not_single:
All (op = x) ==> R
theorem the_XcptLoc_XcptLoc:
the_XcptLoc (XcptLoc a) = a
theorem the_StdXcpt_StdXcpt:
the_StdXcpt (StdXcpt xn) = xn
theorem xcpt_exh:
(EX a. xc = XcptLoc a) | (EX x. xc = StdXcpt x)
theorem xcptE:
[| !!a. xc = XcptLoc a ==> P; !!x. xc = StdXcpt x ==> P |] ==> P
theorem xcpt_if_True_None:
xcpt_if True x None = x
theorem xcpt_if_True_not_None:
x ~= None ==> xcpt_if True x y ~= None
theorem xcpt_if_False:
xcpt_if False x y = y
theorem xcpt_if_Some:
xcpt_if c x (Some y) = Some y
theorem xcpt_if_not_None:
y ~= None ==> xcpt_if c x y = y
theorem split_xcpt_if:
P (xcpt_if c x' x) = ((c & x = None --> P x') & (¬ (c & x = None) --> P x))
theorem raise_if_None:
((raise_if c x) y = None) = (¬ c & y = None)
theorem if_raise_if_None:
((if b then y else (raise_if c x) y) = None) = ((c --> b) & y = None)
theorem raise_if_SomeD:
(raise_if c x) y = Some z ==> c & z = StdXcpt x & y = None | y = Some z
theorem not_inited_empty:
¬ inited C empty
theorem inited_gupdate:
inited C (g(r|->obj)) = (inited C g | r = Inr C)
theorem inited_init_class_obj:
inited C (globs ((init_class_obj G C) s))
theorem not_initedD:
¬ inited C g ==> g (Inr C) = None
theorem initedD:
inited C g ==> EX oi fs. g (Inr C) = Some (oi, fs)
theorem initd_def2:
initd C s = inited C (globs (snd s))
theorem xupd_def2:
xupd f (x, s) = (f x, s)
theorem xupd_xcpt_if_False:
xupd (xcpt_if False xo) s = s
theorem supd_def2:
supd f (x, s) = (x, f s)
theorem supd_lupd:
supd lupd(vn\<mapsto>v) s = (fst s, lupd(vn\<mapsto>v) (snd s))
theorem supd_gupd:
supd gupd(r\<mapsto>obj) s = (fst s, gupd(r\<mapsto>obj) (snd s))
theorem supd_init_obj:
supd (init_obj G oi r) s = (fst s, init_obj G oi r (snd s))
theorem set_locals_def2:
set_locals l (st g l') = st g l
theorem set_locals_id:
set_locals (locals s) s = s
theorem set_set_locals:
set_locals l (set_locals l' s) = set_locals l s
theorem locals_set_locals:
locals (set_locals l s) = l
theorem globs_set_locals:
globs (set_locals l s) = globs s
theorem heap_set_locals:
heap (set_locals l s) = heap s
theorem set_set_lvars:
(set_lvars l) ((set_lvars l') s) = (set_lvars l) s
theorem set_lvars_id:
(set_lvars (locals (snd s))) s = s