equal
deleted
inserted
replaced
6 |
6 |
7 |
7 |
8 header {* \isaheader{JVM Instruction Semantics} *} |
8 header {* \isaheader{JVM Instruction Semantics} *} |
9 |
9 |
10 |
10 |
11 theory JVMExecInstr = JVMInstructions + JVMState: |
11 theory JVMExecInstr imports JVMInstructions JVMState begin |
12 |
12 |
13 |
13 |
14 consts |
14 consts |
15 exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, |
15 exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, |
16 cname, sig, p_count, frame list] => jvm_state" |
16 cname, sig, p_count, frame list] => jvm_state" |