13 |
13 |
14 obj = "cname \\<times> fields_" (* class instance with class name and fields *) |
14 obj = "cname \\<times> fields_" (* class instance with class name and fields *) |
15 |
15 |
16 constdefs |
16 constdefs |
17 |
17 |
18 obj_ty :: "obj \\<Rightarrow> ty" |
18 obj_ty :: "obj => ty" |
19 "obj_ty obj \\<equiv> Class (fst obj)" |
19 "obj_ty obj == Class (fst obj)" |
20 |
20 |
21 init_vars :: "('a \\<times> ty) list \\<Rightarrow> ('a \\<leadsto> val)" |
21 init_vars :: "('a \\<times> ty) list => ('a \\<leadsto> val)" |
22 "init_vars \\<equiv> map_of o map (\\<lambda>(n,T). (n,default_val T))" |
22 "init_vars == map_of o map (\\<lambda>(n,T). (n,default_val T))" |
23 |
23 |
24 datatype xcpt (* exceptions *) |
24 datatype xcpt (* exceptions *) |
25 = NullPointer |
25 = NullPointer |
26 | ClassCast |
26 | ClassCast |
27 | OutOfMemory |
27 | OutOfMemory |
35 |
35 |
36 xstate (* state including exception information *) |
36 xstate (* state including exception information *) |
37 = "xcpt option \\<times> state" |
37 = "xcpt option \\<times> state" |
38 |
38 |
39 syntax |
39 syntax |
40 heap :: "state \\<Rightarrow> aheap" |
40 heap :: "state => aheap" |
41 locals :: "state \\<Rightarrow> locals" |
41 locals :: "state => locals" |
42 Norm :: "state \\<Rightarrow> xstate" |
42 Norm :: "state => xstate" |
43 |
43 |
44 translations |
44 translations |
45 "heap" => "fst" |
45 "heap" => "fst" |
46 "locals" => "snd" |
46 "locals" => "snd" |
47 "Norm s" == "(None,s)" |
47 "Norm s" == "(None,s)" |
48 |
48 |
49 constdefs |
49 constdefs |
50 |
50 |
51 new_Addr :: "aheap \\<Rightarrow> loc \\<times> xcpt option" |
51 new_Addr :: "aheap => loc \\<times> xcpt option" |
52 "new_Addr h \\<equiv> \\<epsilon>(a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory" |
52 "new_Addr h == SOME (a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory" |
53 |
53 |
54 raise_if :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option" |
54 raise_if :: "bool => xcpt => xcpt option => xcpt option" |
55 "raise_if c x xo \\<equiv> if c \\<and> (xo = None) then Some x else xo" |
55 "raise_if c x xo == if c \\<and> (xo = None) then Some x else xo" |
56 |
56 |
57 np :: "val \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option" |
57 np :: "val => xcpt option => xcpt option" |
58 "np v \\<equiv> raise_if (v = Null) NullPointer" |
58 "np v == raise_if (v = Null) NullPointer" |
59 |
59 |
60 c_hupd :: "aheap \\<Rightarrow> xstate \\<Rightarrow> xstate" |
60 c_hupd :: "aheap => xstate => xstate" |
61 "c_hupd h'\\<equiv> \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))" |
61 "c_hupd h'== \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))" |
62 |
62 |
63 cast_ok :: "'c prog \\<Rightarrow> cname \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool" |
63 cast_ok :: "'c prog => cname => aheap => val => bool" |
64 "cast_ok G C h v \\<equiv> v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C" |
64 "cast_ok G C h v == v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C" |
65 |
65 |
66 end |
66 end |