| changeset 10042 | 7164dc0d24d8 |
| parent 9550 | 19a6d1289f5e |
| child 10056 | 9f84ffa4a8d0 |
| 10041:30693ebd16ae | 10042:7164dc0d24d8 |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 JVMExecInstr = JVMInstructions + JVMState + |
9 JVMExecInstr = JVMInstructions + JVMState + |
10 |
10 |
11 consts |
11 consts |
12 exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] \\<Rightarrow> jvm_state" |
12 exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state" |
13 primrec |
13 primrec |
14 "exec_instr (Load idx) G hp stk vars Cl sig pc frs = |
14 "exec_instr (Load idx) G hp stk vars Cl sig pc frs = |
15 (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
15 (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
16 |
16 |
17 "exec_instr (Store idx) G hp stk vars Cl sig pc frs = |
17 "exec_instr (Store idx) G hp stk vars Cl sig pc frs = |