author  wenzelm 
Sun, 28 Aug 2005 16:04:44 +0200  
changeset 17160  fb65eda72fc7 
parent 16417  9bc16273c2d4 
child 32960  69916a850301 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Value.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

5 
header {* Java values *} 

6 

7 

8 

16417  9 
theory Value imports Type begin 
12854  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 

13 
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

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

15 
 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

16 
 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

17 
 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

18 
 Addr loc {* addresses, i.e. locations of objects *} 
12854  19 

20 

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

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

23 

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

25 
primrec "the_Bool (Bool b) = b" 

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

27 
primrec "the_Intg (Intg i) = i" 

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

29 
primrec "the_Addr (Addr a) = a" 

30 

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

32 
consts 

33 
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

34 
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

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

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

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

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

40 
"typeof dt Null = Some NT" 

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

42 

43 
primrec "defpval Void = Unit" 

44 
"defpval Boolean = Bool False" 

45 
"defpval Integer = Intg 0" 

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

47 
"default_val (RefT r ) = Null" 

48 

49 
end 