36 "s::<=E == prg E|-h heap (store s) [ok] \<and> |
36 "s::<=E == prg E|-h heap (store s) [ok] \<and> |
37 prg E,heap (store s)|-locals (store s)[::<=]localT E \<and> |
37 prg E,heap (store s)|-locals (store s)[::<=]localT E \<and> |
38 xconf (heap (store s)) (abrupt s)" |
38 xconf (heap (store s)) (abrupt s)" |
39 |
39 |
40 |
40 |
41 syntax (xsymbols) |
41 notation (xsymbols) |
42 hext :: "aheap => aheap => bool" |
42 hext ("_ \<le>| _" [51,51] 50) and |
43 ("_ \<le>| _" [51,51] 50) |
43 conf ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and |
44 |
44 lconf ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and |
45 conf :: "'c prog => aheap => val => ty => bool" |
45 oconf ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and |
46 ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) |
46 hconf ("_ \<turnstile>h _ \<surd>" [51,51] 50) and |
47 |
47 conforms ("_ ::\<preceq> _" [51,51] 50) |
48 lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" |
|
49 ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) |
|
50 |
|
51 oconf :: "'c prog => aheap => obj => bool" |
|
52 ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) |
|
53 |
|
54 hconf :: "'c prog => aheap => bool" |
|
55 ("_ \<turnstile>h _ \<surd>" [51,51] 50) |
|
56 |
|
57 conforms :: "state => java_mb env' => bool" |
|
58 ("_ ::\<preceq> _" [51,51] 50) |
|
59 |
48 |
60 |
49 |
61 section "hext" |
50 section "hext" |
62 |
51 |
63 lemma hextI: |
52 lemma hextI: |