author  wenzelm 
Wed, 10 Feb 2010 00:50:36 +0100  
changeset 35069  09154b995ed8 
parent 32960  69916a850301 
child 35431  8758fe1fc9f8 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Value.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* Java values *} 

5 

6 

7 

16417  8 
theory Value imports Type begin 
12854  9 

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

10 
typedecl loc {* locations, i.e. abstract references on objects *} 
12854  11 

12 
datatype val 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

13 
= Unit {* dummy result value of void methods *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

14 
 Bool bool {* Boolean value *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

15 
 Intg int {* integer value *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

16 
 Null {* null reference *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

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

19 

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

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

22 

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

24 
primrec "the_Bool (Bool b) = b" 

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

26 
primrec "the_Intg (Intg i) = i" 

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

28 
primrec "the_Addr (Addr a) = a" 

29 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

30 
types dyn_ty = "loc \<Rightarrow> ty option" 
12854  31 
consts 
32 
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

33 
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

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

37 
"typeof dt (Bool b) = Some (PrimT Boolean)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

38 
"typeof dt (Intg i) = Some (PrimT Integer)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

39 
"typeof dt Null = Some NT" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

42 
primrec "defpval Void = Unit" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

43 
"defpval Boolean = Bool False" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

44 
"defpval Integer = Intg 0" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

45 
primrec "default_val (PrimT pt) = defpval pt" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
17160
diff
changeset

46 
"default_val (RefT r ) = Null" 
12854  47 

48 
end 