| author | kleing |
| Mon, 21 Jun 2004 10:25:57 +0200 | |
| changeset 14981 | e73f8140af78 |
| parent 13688 | a0b16d42d489 |
| child 16417 | 9bc16273c2d4 |
| permissions | -rw-r--r-- |
| 12857 | 1 |
(* Title: HOL/Bali/Value.thy |
| 12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
4 |
*) |
|
5 |
header {* Java values *}
|
|
6 |
||
7 |
||
8 |
||
9 |
theory Value = Type: |
|
10 |
||
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
11 |
typedecl loc --{* locations, i.e. abstract references on objects *}
|
| 12854 | 12 |
arities loc :: "type" |
13 |
||
14 |
datatype val |
|
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
15 |
= Unit --{* dummy result value of void methods *}
|
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
16 |
| Bool bool --{* Boolean value *}
|
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
17 |
| Intg int --{* integer value *}
|
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
18 |
| Null --{* null reference *}
|
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
19 |
| Addr loc --{* addresses, i.e. locations of objects *}
|
| 12854 | 20 |
|
21 |
||
22 |
translations "val" <= (type) "Term.val" |
|
23 |
"loc" <= (type) "Term.loc" |
|
24 |
||
25 |
consts the_Bool :: "val \<Rightarrow> bool" |
|
26 |
primrec "the_Bool (Bool b) = b" |
|
27 |
consts the_Intg :: "val \<Rightarrow> int" |
|
28 |
primrec "the_Intg (Intg i) = i" |
|
29 |
consts the_Addr :: "val \<Rightarrow> loc" |
|
30 |
primrec "the_Addr (Addr a) = a" |
|
31 |
||
32 |
types dyn_ty = "loc \<Rightarrow> ty option" |
|
33 |
consts |
|
34 |
typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" |
|
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
35 |
defpval :: "prim_ty \<Rightarrow> val" --{* default value for primitive types *}
|
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
36 |
default_val :: " ty \<Rightarrow> val" --{* default value for all types *}
|
| 12854 | 37 |
|
38 |
primrec "typeof dt Unit = Some (PrimT Void)" |
|
39 |
"typeof dt (Bool b) = Some (PrimT Boolean)" |
|
40 |
"typeof dt (Intg i) = Some (PrimT Integer)" |
|
41 |
"typeof dt Null = Some NT" |
|
42 |
"typeof dt (Addr a) = dt a" |
|
43 |
||
44 |
primrec "defpval Void = Unit" |
|
45 |
"defpval Boolean = Bool False" |
|
46 |
"defpval Integer = Intg 0" |
|
47 |
primrec "default_val (PrimT pt) = defpval pt" |
|
48 |
"default_val (RefT r ) = Null" |
|
49 |
||
50 |
end |