author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 41778  5f79a9e42507 
child 58249  180f1b3508ed 
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 

37956  20 
primrec the_Bool :: "val \<Rightarrow> bool" 
21 
where "the_Bool (Bool b) = b" 

22 

23 
primrec the_Intg :: "val \<Rightarrow> int" 

24 
where "the_Intg (Intg i) = i" 

25 

26 
primrec the_Addr :: "val \<Rightarrow> loc" 

27 
where "the_Addr (Addr a) = a" 

12854  28 

41778  29 
type_synonym dyn_ty = "loc \<Rightarrow> ty option" 
37956  30 

31 
primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" 

32 
where 

33 
"typeof dt Unit = Some (PrimT Void)" 

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

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

36 
 "typeof dt Null = Some NT" 

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

12854  38 

37956  39 
primrec defpval :: "prim_ty \<Rightarrow> val" {* default value for primitive types *} 
40 
where 

41 
"defpval Void = Unit" 

42 
 "defpval Boolean = Bool False" 

43 
 "defpval Integer = Intg 0" 

12854  44 

37956  45 
primrec default_val :: "ty \<Rightarrow> val" {* default value for all types *} 
46 
where 

47 
"default_val (PrimT pt) = defpval pt" 

48 
 "default_val (RefT r ) = Null" 

12854  49 

50 
end 