equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/J/Exceptions.thy |
1 (* Title: HOL/MicroJava/J/Exceptions.thy |
2 ID: $Id$ |
|
3 Author: Gerwin Klein, Martin Strecker |
2 Author: Gerwin Klein, Martin Strecker |
4 Copyright 2002 Technische Universitaet Muenchen |
3 Copyright 2002 Technische Universitaet Muenchen |
5 *) |
4 *) |
6 |
5 |
7 theory Exceptions imports State begin |
6 theory Exceptions imports State begin |
15 "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
14 "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
16 (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
15 (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
17 (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
16 (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
18 |
17 |
19 |
18 |
20 consts |
19 abbreviation |
21 cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname" |
20 cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname" |
22 |
21 where "cname_of hp v == fst (the (hp (the_Addr v)))" |
23 translations |
|
24 "cname_of hp v" == "fst (CONST the (hp (the_Addr v)))" |
|
25 |
22 |
26 |
23 |
27 constdefs |
24 constdefs |
28 preallocated :: "aheap \<Rightarrow> bool" |
25 preallocated :: "aheap \<Rightarrow> bool" |
29 "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |
26 "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |