equal
deleted
inserted
replaced
24 types aheap = "loc \<leadsto> obj" -- {* "@{text heap}" used in a translation below *} |
24 types aheap = "loc \<leadsto> obj" -- {* "@{text heap}" used in a translation below *} |
25 locals = "vname \<leadsto> val" -- "simple state, i.e. variable contents" |
25 locals = "vname \<leadsto> val" -- "simple state, i.e. variable contents" |
26 |
26 |
27 state = "aheap \<times> locals" -- "heap, local parameter including This" |
27 state = "aheap \<times> locals" -- "heap, local parameter including This" |
28 xstate = "xcpt option \<times> state" -- "state including exception information" |
28 xstate = "xcpt option \<times> state" -- "state including exception information" |
29 |
|
30 |
|
31 text {* |
|
32 System exceptions are allocated in all heaps, |
|
33 and they don't carry any information other than their type: *} |
|
34 axioms |
|
35 system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)" |
|
36 |
|
37 |
29 |
38 syntax |
30 syntax |
39 heap :: "state => aheap" |
31 heap :: "state => aheap" |
40 locals :: "state => locals" |
32 locals :: "state => locals" |
41 Norm :: "state => xstate" |
33 Norm :: "state => xstate" |