equal
deleted
inserted
replaced
63 definition locvars_locals :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> State.locals \<Rightarrow> locvars" where |
63 definition locvars_locals :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> State.locals \<Rightarrow> locvars" where |
64 "locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs" |
64 "locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs" |
65 |
65 |
66 definition locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals" where |
66 definition locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals" where |
67 "locals_locvars G C S lvs == |
67 "locals_locvars G C S lvs == |
68 Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))" |
68 Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs), This\<mapsto>(hd lvs))" |
69 |
69 |
70 definition locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars" where |
70 definition locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars" where |
71 "locvars_xstate G C S xs == locvars_locals G C S (gl xs)" |
71 "locvars_xstate G C S xs == locvars_locals G C S (gl xs)" |
72 |
72 |
73 |
73 |