equal
deleted
inserted
replaced
6 State for evaluation of Java expressions and statements |
6 State for evaluation of Java expressions and statements |
7 *) |
7 *) |
8 |
8 |
9 State = WellType + |
9 State = WellType + |
10 |
10 |
11 constdefs |
11 consts |
12 |
|
13 the_Bool :: "val \\<Rightarrow> bool" |
12 the_Bool :: "val \\<Rightarrow> bool" |
14 "the_Bool v \\<equiv> \\<epsilon>b. v = Bool b" |
|
15 |
|
16 the_Int :: "val \\<Rightarrow> int" |
13 the_Int :: "val \\<Rightarrow> int" |
17 "the_Int v \\<equiv> \\<epsilon>i. v = Intg i" |
|
18 |
|
19 the_Addr :: "val \\<Rightarrow> loc" |
14 the_Addr :: "val \\<Rightarrow> loc" |
20 "the_Addr v \\<equiv> \\<epsilon>a. v = Addr a" |
|
21 |
|
22 consts |
|
23 |
15 |
24 defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *) |
16 defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *) |
25 default_val :: "ty \\<Rightarrow> val" (* default value for all types *) |
17 default_val :: "ty \\<Rightarrow> val" (* default value for all types *) |
|
18 |
|
19 primrec |
|
20 "the_Bool (Bool b) = b" |
|
21 |
|
22 primrec |
|
23 "the_Int (Intg i) = i" |
|
24 |
|
25 primrec |
|
26 "the_Addr (Addr a) = a" |
26 |
27 |
27 primrec |
28 primrec |
28 "defpval Void = Unit" |
29 "defpval Void = Unit" |
29 "defpval Boolean = Bool False" |
30 "defpval Boolean = Bool False" |
30 "defpval Integer = Intg (#0)" |
31 "defpval Integer = Intg (#0)" |