equal
deleted
inserted
replaced
23 datatype xcpt (* exceptions *) |
23 datatype xcpt (* exceptions *) |
24 = NullPointer |
24 = NullPointer |
25 | ClassCast |
25 | ClassCast |
26 | OutOfMemory |
26 | OutOfMemory |
27 |
27 |
28 types aheap = "loc \<leadsto> obj" (* "heap" used in a translation below *) |
28 types aheap = "loc \<leadsto> obj" (** "heap" used in a translation below **) |
29 locals = "vname \<leadsto> val" |
29 locals = "vname \<leadsto> val" |
30 |
30 |
31 state (* simple state, i.e. variable contents *) |
31 state (* simple state, i.e. variable contents *) |
32 = "aheap \<times> locals" |
32 = "aheap \<times> locals" |
33 (* heap, local parameter including This *) |
33 (* heap, local parameter including This *) |