118 tprg ::"java_mb prog" where |
118 tprg ::"java_mb prog" where |
119 "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]" |
119 "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]" |
120 |
120 |
121 abbreviation |
121 abbreviation |
122 obj1 :: obj where |
122 obj1 :: obj where |
123 "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))" |
123 "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False, (vee, Ext )\<mapsto>Intg 0))" |
124 |
124 |
125 abbreviation "s0 == Norm (Map.empty, Map.empty)" |
125 abbreviation "s0 == Norm (Map.empty, Map.empty)" |
126 abbreviation "s1 == Norm (Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))" |
126 abbreviation "s1 == Norm (Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))" |
127 abbreviation "s2 == Norm (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
127 abbreviation "s2 == Norm (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null, This\<mapsto>Addr a))" |
128 abbreviation "s3 == (Some NP, Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))" |
128 abbreviation "s3 == (Some NP, Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))" |
129 |
129 |
130 lemmas map_of_Cons = map_of.simps(2) |
130 lemmas map_of_Cons = map_of.simps(2) |
131 |
131 |
132 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |
132 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |