author schirmer
Thu, 31 Oct 2002 18:27:10 +0100
changeset 13688 a0b16d42d489
parent 12858 6214f03d6d27
child 14981 e73f8140af78
permissions -rw-r--r--
"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.

(*  Title:      HOL/Bali/Value.thy
    ID:         $Id$
    Author:     David von Oheimb
header {* Java values *}

theory Value = Type:

typedecl loc            --{* locations, i.e. abstract references on objects *}
arities	 loc :: "type"

datatype val
	= Unit          --{* dummy result value of void methods *}
	| Bool bool     --{* Boolean value *}
	| Intg int      --{* integer value *}
	| Null          --{* null reference *}
	| Addr loc      --{* addresses, i.e. locations of objects *}

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

consts   the_Bool   :: "val \<Rightarrow> bool"  
primrec "the_Bool (Bool b) = b"
consts   the_Intg   :: "val \<Rightarrow> int"
primrec "the_Intg (Intg i) = i"
consts   the_Addr   :: "val \<Rightarrow> loc"
primrec "the_Addr (Addr a) = a"

types	dyn_ty      = "loc \<Rightarrow> ty option"
  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
  defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
  default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}

primrec "typeof dt  Unit    = Some (PrimT Void)"
	"typeof dt (Bool b) = Some (PrimT Boolean)"
	"typeof dt (Intg i) = Some (PrimT Integer)"
	"typeof dt  Null    = Some NT"
	"typeof dt (Addr a) = dt a"

primrec	"defpval Void    = Unit"
	"defpval Boolean = Bool False"
	"defpval Integer = Intg 0"
primrec	"default_val (PrimT pt) = defpval pt"
	"default_val (RefT  r ) = Null"