WellForm.thy

Back to the index of JVM0_ASCII

WellForm = Classfile + Runtime +

constdefs
 method_over_ok :: "['code classfiles,cname,cname] => bool"
 "method_over_ok CFS cn cn' ==  
	!ml rd ins rd' ins'. 
		get_methods (CFS !! cn) ml = Some (rd ,ins ) & 
		get_methods (CFS !! cn') ml = Some (rd',ins') 
			--> rd=rd'"


 method_impl_ok :: "['code classfiles,cname,cname] => bool"
 "method_impl_ok CFS cn si ==  
	!ml rd ins. 
		get_methods (CFS !! si) ml = Some (rd,ins)
		--> (? cn' ins'. (cn',cn) : (d_superclass_rel CFS)^* & 
				get_methods (CFS !! cn') ml = Some (rd,ins'))" 


 wf_inter :: "['code classfiles,cname] => bool" 
 "wf_inter CFS i ==
	(get_superclass (CFS !! i) = Object) & 
	(!si : get_superinterfaces (CFS !! i).
		 is_inter CFS si &  
		 (i,si) ~: (d_superinterface_rel CFS)^*)"


 wf_class :: "['code classfiles,cname] => bool" 
 "wf_class CFS cn ==
	if no_super (CFS !! cn) 
	    then cn=Object &  
                 get_superinterfaces (CFS !! cn)={} 
	    else let sc = get_superclass (CFS !! cn)
		 in
		 is_class CFS sc &  
                 (cn,sc) ~: (d_superclass_rel CFS)^* & 
		 (!sc'. (sc',cn) : (d_superclass_rel CFS)^+ --> method_over_ok CFS cn sc') &  
	         (!si : get_superinterfaces (CFS !! cn). 
			   is_inter CFS si &  
			   (!si'. (si',si) : (d_superinterface_rel CFS)^*
				--> method_impl_ok CFS cn si'))"


 wf_classfiles :: "'code classfiles => bool" 
 "wf_classfiles CFS ==
    (finite {cn. CFS cn ~= None}) &  
    (is_class CFS Object &  no_super (CFS !! Object)) & 
    (get_fields (CFS !! Object) = empty) & 
    (!cn. CFS cn ~= None 
	     --> (get_thisclass (CFS !! cn) = cn) & 
		(is_inter CFS cn --> wf_inter CFS cn) & 
		(is_class CFS cn --> wf_class CFS cn))"

end

Theorems proved in WellForm.ML:

rtrancl_eq_or_trancl

((dc, oc) : r^*) = (oc = dc | (dc, oc) : r^+)

finite_d_superinterface_rel

wf_classfiles CFS ==> finite (d_superinterface_rel CFS)

finite_d_superclass_rel

wf_classfiles CFS ==> finite (d_superclass_rel CFS)

wf_cs1

[| wf_classfiles CFS; si : get_superinterfaces CFS !! i; is_inter CFS i |]
==> (i, si) ~: (d_superinterface_rel CFS)^*

d_superinterface_rel_irrefl

[| wf_classfiles CFS; (si, i) : (d_superinterface_rel CFS)^+ |] ==> i ~= si

acyclic_d_superinterface_rel

wf_classfiles CFS ==> acyclic (d_superinterface_rel CFS)

wf_d_superinterface_rel

wf_classfiles CFS ==> wf (d_superinterface_rel CFS)

in_d_superclass_rel_is_class

[| (cn, sc) : (d_superclass_rel CFS)^*; is_class CFS cn |] ==> is_class CFS sc

in_d_superclass_rel_is_class2

[| (cn, sc) : (d_superclass_rel CFS)^*; is_class CFS sc |] ==> is_class CFS cn

in_superclasses_not_Object

[| wf_classfiles CFS; (sc, cn) : (d_superclass_rel CFS)^+ |] ==> cn ~= Object

in_superclasses_not_Object2

[| wf_classfiles CFS; sc ~= Object; (sc, cn) : (d_superclass_rel CFS)^* |] ==> cn ~= Object

in_superclasses_not_Object3

[| wf_classfiles CFS; (sc, Object) : (d_superclass_rel CFS)^* |] ==> sc = Object

wf_cs0

wf_classfiles CFS ==> (sc, Object) ~: (d_superclass_rel CFS)^+

wf_cs3

[| wf_classfiles CFS; get_superclass CFS !! cn = sc; is_class CFS cn; cn ~= Object |]
==> (cn, sc) ~: (d_superclass_rel CFS)^*

wf_cs4

[| wf_classfiles CFS; cn ~= Object; get_superclass CFS !! cn = sc; is_class CFS cn |]
==> sc ~= cn & is_class CFS sc

d_superclass_rel_irrefl

[| wf_classfiles CFS; (sc, cn) : (d_superclass_rel CFS)^+ |] ==> cn ~= sc

acyclic_d_superclass_rel

wf_classfiles CFS ==> acyclic (d_superclass_rel CFS)

wf_d_superclass_rel

wf_classfiles CFS ==> wf (d_superclass_rel CFS)

wf_implements_term_rel

wf implements_term_rel

implements_rec

wf_classfiles CFS
==> implements (CFS, cn, si) =
    (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)))

wf_get_all_fields_term_rel

wf get_all_fields_term_rel

get_all_fields_rec

[| wf_classfiles CFS; is_class CFS cn |]
==> get_all_fields (CFS, cn) =
    (let fs = get_fields CFS !! cn
     in if cn = Object then fs else let sc = get_superclass CFS !! cn in get_all_fields (CFS, sc) ++ fs)

wf_cs6

wf_classfiles CFS
==> is_class CFS Object & get_superinterfaces CFS !! Object = {} & get_fields CFS !! Object = empty

not_implements_Object

wf_classfiles CFS ==> ~ implements (CFS, Object, i)

in_superinterface_rel_imp_is_inter

(si, i) : (d_superinterface_rel CFS)^+ ==> is_inter CFS si & is_inter CFS i

implements_impl_is_inter

[| wf_classfiles CFS; implements (CFS, cn, si) |] ==> is_class CFS cn & is_inter CFS si

not_in_superclass_rel_Object

wf_classfiles CFS ==> (sc, Object) ~: (d_superclass_rel CFS)^+

implements_superinterface_trans

[| wf_classfiles CFS; implements (CFS, cn, i); (si, i) : (d_superinterface_rel CFS)^+ |]
==> implements (CFS, cn, si)

implements_superinterface_trans2

[| wf_classfiles CFS; implements (CFS, cn, i); (si, i) : (d_superinterface_rel CFS)^* |]
==> implements (CFS, cn, si)

implements_superclass_rel_trans

[| wf_classfiles CFS; (sc, cn) : (d_superclass_rel CFS)^+; implements (CFS, sc, si) |]
==> implements (CFS, cn, si)

implements_superclass_rel_trans2

[| wf_classfiles CFS; (sc, cn) : (d_superclass_rel CFS)^*; implements (CFS, sc, si) |]
==> implements (CFS, cn, si)

in_superclass_rel_Object

[| wf_classfiles CFS; is_class CFS cn & cn ~= Object |] ==> (Object, cn) : (d_superclass_rel CFS)^+

in_superclass_rel_Object2

[| wf_classfiles CFS; is_class CFS cn |] ==> (Object, cn) : (d_superclass_rel CFS)^*

wf_dyn_class_term_rel

wf dyn_class_term_rel

dyn_class_rec

[| wf_classfiles CFS; is_class CFS cn |]
==> dyn_class (CFS, ml, cn) =
    (let ms = get_methods CFS !! cn
     in if ms ml ~= None then cn
        else if cn = Object then arbitrary
             else let sc = get_superclass CFS !! cn in dyn_class (CFS, ml, sc))

d_superclass_imp_class

(sc, cn) : d_superclass_rel CFS
==> is_class CFS cn & is_class CFS sc & cn ~= Object & get_superclass CFS !! cn = sc

in_superclass_rel_imp_is_class

(sc, cn) : (d_superclass_rel CFS)^+ ==> is_class CFS cn & is_class CFS sc

d_implements_imp_class_inter

d_implements CFS cn si ==> is_class CFS cn & is_inter CFS si