equal
deleted
inserted
replaced
6 |
6 |
7 header "Java Values" |
7 header "Java Values" |
8 |
8 |
9 theory Value = Type: |
9 theory Value = Type: |
10 |
10 |
11 typedecl loc (* locations, i.e. abstract references on objects *) |
11 typedecl loc_ -- "locations, i.e. abstract references on objects" |
|
12 |
|
13 datatype loc |
|
14 = XcptRef xcpt -- "special locations for pre-allocated system exceptions" |
|
15 | Loc loc_ -- "usual locations (references on objects)" |
12 |
16 |
13 datatype val |
17 datatype val |
14 = Unit (* dummy result value of void methods *) |
18 = Unit -- "dummy result value of void methods" |
15 | Null (* null reference *) |
19 | Null -- "null reference" |
16 | Bool bool (* Boolean value *) |
20 | Bool bool -- "Boolean value" |
17 | Intg int (* integer value, name Intg instead of Int because |
21 | Intg int -- "integer value, name Intg instead of Int because |
18 of clash with HOL/Set.thy *) |
22 of clash with HOL/Set.thy" |
19 | Addr loc (* addresses, i.e. locations of objects *) |
23 | Addr loc -- "addresses, i.e. locations of objects " |
20 |
24 |
21 consts |
25 consts |
22 the_Bool :: "val => bool" |
26 the_Bool :: "val => bool" |
23 the_Intg :: "val => int" |
27 the_Intg :: "val => int" |
24 the_Addr :: "val => loc" |
28 the_Addr :: "val => loc" |
31 |
35 |
32 primrec |
36 primrec |
33 "the_Addr (Addr a) = a" |
37 "the_Addr (Addr a) = a" |
34 |
38 |
35 consts |
39 consts |
36 defpval :: "prim_ty => val" (* default value for primitive types *) |
40 defpval :: "prim_ty => val" -- "default value for primitive types" |
37 default_val :: "ty => val" (* default value for all types *) |
41 default_val :: "ty => val" -- "default value for all types" |
38 |
42 |
39 primrec |
43 primrec |
40 "defpval Void = Unit" |
44 "defpval Void = Unit" |
41 "defpval Boolean = Bool False" |
45 "defpval Boolean = Bool False" |
42 "defpval Integer = Intg 0" |
46 "defpval Integer = Intg 0" |