108 |
108 |
109 test_def:"test == Expr(e::=NewC Ext);; |
109 test_def:"test == Expr(e::=NewC Ext);; |
110 Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" |
110 Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" |
111 |
111 |
112 |
112 |
113 syntax |
113 abbreviation |
114 |
|
115 NP :: xcpt |
114 NP :: xcpt |
|
115 "NP == NullPointer" |
|
116 |
116 tprg ::"java_mb prog" |
117 tprg ::"java_mb prog" |
|
118 "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]" |
|
119 |
117 obj1 :: obj |
120 obj1 :: obj |
118 obj2 :: obj |
121 "obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))" |
119 s0 :: state |
122 |
120 s1 :: state |
123 "s0 == Norm (empty, empty)" |
121 s2 :: state |
124 "s1 == Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
122 s3 :: state |
125 "s2 == Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
123 s4 :: state |
126 "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
124 |
|
125 translations |
|
126 "NP" == "NullPointer" |
|
127 "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]" |
|
128 "obj1" <= "(Ext, empty((vee, Base)\<mapsto>Bool False) |
|
129 ((vee, Ext )\<mapsto>Intg 0))" |
|
130 "s0" == " Norm (empty, empty)" |
|
131 "s1" == " Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
|
132 "s2" == " Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
|
133 "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
|
134 |
|
135 |
127 |
136 ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *} |
128 ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *} |
137 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |
129 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |
138 apply (simp (no_asm)) |
130 apply (simp (no_asm)) |
139 done |
131 done |