Classfile.thy

Classfile = Cpool + Store + WF_Rel +

types
 iflag = bool
 this = cl_idx
 super = cl_idx
 inter = "cl_idx list"

(** fields/methods p.101 **)

 'code method_info = "nm_idx *	   
		       nm_idx *
		       'code"		(* only one m_attribute *) 

 field_info =  "nm_idx *		
		nm_idx"			


(****************** classFile p.84 ******************)

 fields		= field_info list			(* field descriptions *)
 'code methods = ('code method_info) list		(* method descriptions *)

 'code classfile = "cpool *	
		   iflag *				
		   this *	
		   super *	
		   inter *	
		   fields *	
		   'code methods"		

(** constant pool **)
(** is it an interface?	**)
(** idx to Class entry with current class **)
(** idx to Class entry with direct superclass **)
(** idxes to Class entries with direct superinterfaces	**)
(** fields **)
(** methods **) 



constdefs
 get_cpool :: "'code classfile => cpool" 
 "get_cpool == %(cp,a,t,s,is,fs,ms). cp"

 is_interface :: "'code classfile => bool" 
 "is_interface == %(cp,a,t,s,is,fs,ms). a"

 get_thisclass :: "'code classfile => cname" 
 "get_thisclass == %(cp,a,t,s,is,fs,ms). get_Id (extract_Class cp t)"

 get_superclass :: "'code classfile => cname" 
 "get_superclass == %(cp,a,t,s,is,fs,ms). get_Id (extract_Class cp s)"

 get_superinterfaces :: "'code classfile => cname set" 
 "get_superinterfaces == %(cp,a,t,s,is,fs,ms). set (map (get_Id  o  (extract_Class cp)) is)"

 get_methods :: "'code classfile => (method_loc ~=> return_desc * 'code)"
 "get_methods == %(cp,a,t,s,is,fs,ms). 
     map_of (map (%(mn,md,ins). let (pd,rd) = get_Md (get_Utf8 (cp ! md))
                                in
                                ((get_Id (get_Utf8 (cp ! mn)), pd) , (rd,ins))) 
                 ms)"


 get_fields :: "'code classfile => (field_loc ~=> field_desc)"
 "get_fields == %(cp,a,t,s,is,fs,ms). 
     map_of (map (%(fn,fd). ((get_Id (extract_Class cp t), get_Id (get_Utf8 (cp ! fn))),
                             get_Fd (get_Utf8 (cp ! fd)))) 
                 fs)"


 (** is it class Object ? **)
 no_super :: "'code classfile => bool"
 "no_super == %(cp,a,t,s,is,fs,ms). s=0"


types
 'code classfiles = "cname ~=> 'code classfile"

constdefs
 (** get code of current method **)
 get_code :: "['code classfiles,cname,method_loc] => 'code"
 "get_code CFS cn ml == let (rd,code) = ((get_methods (CFS !! cn)) !! ml) in code"



 is_class :: "['code classfiles,cname] => bool"
 "is_class CFS cn == CFS cn ~= None &  ~ is_interface (CFS !! cn)"

 d_superclass_rel :: "'code classfiles => (cname * cname) set" 
 "d_superclass_rel CFS == {(sc,cn). is_class CFS sc &  is_class CFS cn &  
				   cn~=Object & 
                                   get_superclass (CFS !! cn) = sc}"


 is_inter :: "['code classfiles,cname] => bool"
 "is_inter CFS cn == CFS cn ~= None &  is_interface (CFS !! cn)"

 d_superinterface_rel :: "'code classfiles => (cname * cname) set" 
 "d_superinterface_rel CFS == {(si,i). is_inter CFS si  &  is_inter CFS i &  
				      si : (get_superinterfaces (CFS !! i))}"

 d_implements :: "['code classfiles,cname,cname] => bool" 
 "d_implements CFS cn i == is_class CFS cn  &  is_inter CFS i &  
				i : (get_superinterfaces (CFS !! cn))"


constdefs
 implements_term_rel :: "(('code classfiles * cname * cname) * 
			  ('code classfiles * cname * cname)) set" 
 "implements_term_rel == {((CFS,sc,i),(CFS',cn,i')). 
				CFS=CFS' &  i=i' &  wf (d_superclass_rel CFS) &  
				(sc,cn) : d_superclass_rel CFS}"
consts 
 implements :: "'code classfiles * cname * cname => bool" 
recdef implements "implements_term_rel" congs "[conj_cong]"
 "implements (CFS, cn, si) = 
	(if wf (d_superclass_rel CFS) 
	    then (d_implements CFS cn si) | 
                 (? si'. d_implements CFS cn si' &  
			(si,si') : (d_superinterface_rel CFS)^+) | 
		 (? sc.  (sc,cn) : d_superclass_rel CFS &  
			implements (CFS, sc, si))
	    else arbitrary)"

end