10 |
10 |
11 types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)" (* same as env of WellType.thy *) |
11 types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)" (* same as env of WellType.thy *) |
12 |
12 |
13 constdefs |
13 constdefs |
14 |
14 |
15 hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50) |
15 hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) |
16 "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
16 "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
17 |
17 |
18 conf :: "'c prog => aheap => val => ty => bool" ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) |
18 conf :: "'c prog => aheap => val => ty => bool" |
19 "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T" |
19 ("_,_ |- _ ::<= _" [51,51,51,51] 50) |
|
20 "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T" |
20 |
21 |
21 lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool" |
22 lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool" |
22 ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) |
23 ("_,_ |- _ [::<=] _" [51,51,51,51] 50) |
23 "G,h\<turnstile>vs[::\<preceq>]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h\<turnstile>v::\<preceq>T)" |
24 "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)" |
24 |
25 |
25 oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) |
26 oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50) |
26 "G,h\<turnstile>obj\<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))" |
27 "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))" |
27 |
28 |
28 hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50) |
29 hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50) |
29 "G\<turnstile>h h\<surd> == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj\<surd>" |
30 "G|-h h [ok] == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]" |
30 |
31 |
31 conforms :: "state => java_mb env_ => bool" ("_ ::\<preceq> _" [51,51] 50) |
32 conforms :: "state => java_mb env_ => bool" ("_ ::<= _" [51,51] 50) |
32 "s::\<preceq>E == prg E\<turnstile>h heap s\<surd> \<and> prg E,heap s\<turnstile>locals s[::\<preceq>]localT E" |
33 "s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E" |
33 |
34 |
34 |
35 |
35 syntax (HTML) |
36 syntax (xsymbols) |
36 hext :: "aheap => aheap => bool" |
37 hext :: "aheap => aheap => bool" |
37 ("_ <=| _" [51,51] 50) |
38 ("_ \<le>| _" [51,51] 50) |
38 |
39 |
39 conf :: "'c prog => aheap => val => ty => bool" |
40 conf :: "'c prog => aheap => val => ty => bool" |
40 ("_,_ |- _ ::<= _" [51,51,51,51] 50) |
41 ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) |
41 |
42 |
42 lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool" |
43 lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool" |
43 ("_,_ |- _ [::<=] _" [51,51,51,51] 50) |
44 ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) |
44 |
45 |
45 oconf :: "'c prog => aheap => obj => bool" |
46 oconf :: "'c prog => aheap => obj => bool" |
46 ("_,_ |- _ [ok]" [51,51,51] 50) |
47 ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) |
47 |
48 |
48 hconf :: "'c prog => aheap => bool" |
49 hconf :: "'c prog => aheap => bool" |
49 ("_ |-h _ [ok]" [51,51] 50) |
50 ("_ \<turnstile>h _ \<surd>" [51,51] 50) |
50 |
51 |
51 conforms :: "state => java_mb env_ => bool" |
52 conforms :: "state => java_mb env_ => bool" |
52 ("_ ::<= _" [51,51] 50) |
53 ("_ ::\<preceq> _" [51,51] 50) |
53 |
54 |
54 |
55 |
55 section "hext" |
56 section "hext" |
56 |
57 |
57 lemma hextI: |
58 lemma hextI: |