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(Param\<mapsto>p)(reset_locs s2)) -Meth C m-n-> s3 |
57 lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_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'" |
63 |
63 |
64 Impl: " s -body M-n-> s' ==> |
64 Impl: " s -body M-n-> s' ==> |
65 s -Impl M-Suc n-> s'" |
65 s -Impl M-Suc n-> s'" |
66 |
66 |
67 |
67 |
70 "s -c1;; c2 -n\<rightarrow> t" |
70 "s -c1;; c2 -n\<rightarrow> t" |
71 "s -If(e) c1 Else c2-n\<rightarrow> t" |
71 "s -If(e) c1 Else c2-n\<rightarrow> t" |
72 "s -While(x) c -n\<rightarrow> t" |
72 "s -While(x) c -n\<rightarrow> t" |
73 "s -x:==e -n\<rightarrow> t" |
73 "s -x:==e -n\<rightarrow> t" |
74 "s -e1..f:==e2 -n\<rightarrow> t" |
74 "s -e1..f:==e2 -n\<rightarrow> t" |
75 inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t" |
75 inductive_cases Meth_elim_cases: "s -Meth Cm-n\<rightarrow> t" |
76 inductive_cases Impl_elim_cases: "s -Impl M-n\<rightarrow> t" |
76 inductive_cases Impl_elim_cases: "s -Impl Cm-n\<rightarrow> t" |
77 lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases |
77 lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases |
78 inductive_cases eval_elim_cases: |
78 inductive_cases eval_elim_cases: |
79 "s -new C \<succ>v-n\<rightarrow> t" |
79 "s -new C \<succ>v-n\<rightarrow> t" |
80 "s -Cast C e \<succ>v-n\<rightarrow> t" |
80 "s -Cast C e \<succ>v-n\<rightarrow> t" |
81 "s -LAcc x \<succ>v-n\<rightarrow> t" |
81 "s -LAcc x \<succ>v-n\<rightarrow> t" |