37 |
37 |
38 primrec |
38 primrec |
39 "exec_mo (Getfield F C) hp stk pc = |
39 "exec_mo (Getfield F C) hp stk pc = |
40 (let oref = hd stk; |
40 (let oref = hd stk; |
41 xp' = raise_xcpt (oref=Null) NullPointer; |
41 xp' = raise_xcpt (oref=Null) NullPointer; |
42 (oc,fs) = hp !! (the_Addr oref); |
42 (oc,fs) = the(hp(the_Addr oref)); |
43 stk' = if xp'=None then (fs!!(F,C))#(tl stk) else tl stk |
43 stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk |
44 in |
44 in |
45 (xp' , hp , stk' , pc+1))" |
45 (xp' , hp , stk' , pc+1))" |
46 |
46 |
47 "exec_mo (Putfield F C) hp stk pc = |
47 "exec_mo (Putfield F C) hp stk pc = |
48 (let (fval,oref)= (hd stk, hd(tl stk)); |
48 (let (fval,oref)= (hd stk, hd(tl stk)); |
49 xp' = raise_xcpt (oref=Null) NullPointer; |
49 xp' = raise_xcpt (oref=Null) NullPointer; |
50 a = the_Addr oref; |
50 a = the_Addr oref; |
51 (oc,fs) = hp !! a; |
51 (oc,fs) = the(hp a); |
52 hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp |
52 hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp |
53 in |
53 in |
54 (xp' , hp' , tl (tl stk), pc+1))" |
54 (xp' , hp' , tl (tl stk), pc+1))" |
55 |
55 |
56 |
56 |