equal
deleted
inserted
replaced
52 Cast: "[| s -e>v-n-> s'; |
52 Cast: "[| s -e>v-n-> s'; |
53 case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==> |
53 case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==> |
54 s -Cast C e>v-n-> s'" |
54 s -Cast C e>v-n-> s'" |
55 |
55 |
56 Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; |
56 Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; |
57 lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s2)) -Meth (C,m)-n-> s3 |
57 lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n-> s3 |
58 |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3" |
58 |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3" |
59 |
59 |
60 Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C; |
60 Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C; |
61 init_locs D m s -Impl (D,m)-n-> s' |] ==> |
61 init_locs D m s -Impl (D,m)-n-> s' |] ==> |
62 s -Meth (C,m)-n-> s'" |
62 s -Meth (C,m)-n-> s'" |