author  schirmer 
Thu, 31 Oct 2002 18:27:10 +0100  
changeset 13688  a0b16d42d489 
parent 12858  6214f03d6d27 
child 14981  e73f8140af78 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Value.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 
header {* Java values *} 

7 

8 

9 

10 
theory Value = Type: 

11 

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

12 
typedecl loc {* locations, i.e. abstract references on objects *} 
12854  13 
arities loc :: "type" 
14 

15 
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

16 
= 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

17 
 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

18 
 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

19 
 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

20 
 Addr loc {* addresses, i.e. locations of objects *} 
12854  21 

22 

23 
translations "val" <= (type) "Term.val" 

24 
"loc" <= (type) "Term.loc" 

25 

26 
consts the_Bool :: "val \<Rightarrow> bool" 

27 
primrec "the_Bool (Bool b) = b" 

28 
consts the_Intg :: "val \<Rightarrow> int" 

29 
primrec "the_Intg (Intg i) = i" 

30 
consts the_Addr :: "val \<Rightarrow> loc" 

31 
primrec "the_Addr (Addr a) = a" 

32 

33 
types dyn_ty = "loc \<Rightarrow> ty option" 

34 
consts 

35 
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

36 
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

37 
default_val :: " ty \<Rightarrow> val" {* default value for all types *} 
12854  38 

39 
primrec "typeof dt Unit = Some (PrimT Void)" 

40 
"typeof dt (Bool b) = Some (PrimT Boolean)" 

41 
"typeof dt (Intg i) = Some (PrimT Integer)" 

42 
"typeof dt Null = Some NT" 

43 
"typeof dt (Addr a) = dt a" 

44 

45 
primrec "defpval Void = Unit" 

46 
"defpval Boolean = Bool False" 

47 
"defpval Integer = Intg 0" 

48 
primrec "default_val (PrimT pt) = defpval pt" 

49 
"default_val (RefT r ) = Null" 

50 

51 
end 