Exec.thy

Exec = LoadAndStore + Object + Method + Opstack + Control + RelPow + 

datatype
 instr	= LAS load_and_store	
        | CO  create_object	
        | MO  manipulate_object	
        | MA  manipulate_array	
	| CH  check_object	
	| MI  meth_inv		
	| MR  meth_ret		
	| OS  op_stack		
	| CB  cond_branch	
	| UB  uncond_branch	
	
types
 bytecode = (instr list) classfiles
consts
 exec :: "bytecode * jvm_state => jvm_state option"

(** exec is not recursive. recdef is just used because of its pattern matching facilities **)
recdef exec "{}"
 "exec (CFS, None, hp, []) = None"

 "exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) = 
  (let cp = get_cpool (CFS !! cn)
   in
   Some (case (get_code CFS cn ml) ! pc of
     LAS ins => (let (stk',loc',pc') = exec_las ins stk loc pc
		in		
		(None,hp,(stk',loc',cn,ml,pc')#frs))

    | CO ins => (let (xp',hp',stk',pc') = exec_co ins CFS cp hp stk pc
		in
		(xp',hp',(stk',loc,cn,ml,pc')#frs))	    

    | MO ins => (let (xp',hp',stk',pc') = exec_mo ins cp hp stk pc
		in
		(xp',hp',(stk',loc,cn,ml,pc')#frs))	

    | MA ins => (let (xp',hp',stk',pc') = exec_ma ins CFS hp stk pc
		in
		(xp',hp',(stk',loc,cn,ml,pc')#frs)) 

    | CH ins => (let (xp',pc') = exec_ch ins CFS cp hp stk pc
		in
		(xp',hp,(stk,loc,cn,ml,pc')#frs))

    | MI ins => (let (xp',f',stk',pc') = exec_mi ins CFS cp hp stk pc 
		in
		(xp',hp,f'#(stk',loc,cn,ml,pc')#frs))

    | MR ins => (let frs' = exec_mr ins stk frs
		in
		(None,hp,frs'))

    | OS ins => (let (stk',pc') = exec_os ins stk pc
		in
		(None,hp,(stk',loc,cn,ml,pc')#frs))

    | CB ins => (let (stk',pc') = exec_cb ins stk pc
		in
		(None,hp,(stk',loc,cn,ml,pc')#frs))

    | UB ins => (let pc' = exec_ub ins pc
		in
		(None,hp,(stk,loc,cn,ml,pc')#frs))))"

 "exec (CFS, Some xp, hp, frs) = None"


constdefs
 exec_all :: "[bytecode,jvm_state,jvm_state] => bool"  ("_ |- _ -jvm-> _")
 "CFS |- s -jvm-> t == (s,t) : {(s,t). exec (CFS,s) = Some t}^*"

end