LoadAndStore.thy

LoadAndStore = Runtime +

(** load and store instructions transfer values between local variables 
    and operand stack **)

datatype load_and_store =
  IAload  ins_type nat  ("_ load _" 30)     (* load int/ref from local variable *)	
| IAstore ins_type nat  ("_ store _" 30)    (* store int into/ref local variable *)
| Bipush int					(* push int *)			
| Aconst_null					(* push null *)


consts
 exec_las :: "[load_and_store,opstack,locvars,p_count] => (opstack * locvars * p_count)" 
primrec
 "exec_las (X load idx) stk vars pc = ((vars ! idx) # stk , vars , pc+1)"

 "exec_las (X store idx) stk vars pc = (tl stk , vars[idx:=hd stk] , pc+1)"	

 "exec_las (Bipush ival) stk vars pc = (Intg ival # stk , vars , pc+1)"

 "exec_las Aconst_null stk vars pc = (Null # stk , vars , pc+1)"

end