21 "G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts \\<equiv> \\<forall>n T. Ts n = Some T \\<longrightarrow> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T)" |
21 "G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts \\<equiv> \\<forall>n T. Ts n = Some T \\<longrightarrow> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T)" |
22 |
22 |
23 oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50) |
23 oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50) |
24 "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))" |
24 "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))" |
25 |
25 |
26 hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_,_\\<turnstile>\\<surd>" [51,51] 50) |
26 hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50) |
27 "G,h\\<turnstile>\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>" |
27 "G\\<turnstile>h h\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>" |
28 |
28 |
29 conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50) |
29 conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50) |
30 "s\\<Colon>\\<preceq>E \\<equiv> prg E,heap s\\<turnstile>\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E" |
30 "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E" |
31 |
31 |
32 end |
32 end |