equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/BV/JVM.thy |
1 (* Title: HOL/MicroJava/BV/JVM.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Gerwin Klein |
2 Author: Tobias Nipkow, Gerwin Klein |
4 Copyright 2000 TUM |
3 Copyright 2000 TUM |
5 *) |
4 *) |
6 |
5 |
7 header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *} |
6 header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *} |
8 |
7 |
9 theory Typing_Framework_JVM imports Typing_Framework_err JVMType EffectMono BVSpec begin |
8 theory Typing_Framework_JVM |
10 |
9 imports "../DFA/Abstract_BV" JVMType EffectMono BVSpec |
|
10 begin |
11 |
11 |
12 constdefs |
12 constdefs |
13 exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state step_type" |
13 exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state step_type" |
14 "exec G maxs rT et bs == |
14 "exec G maxs rT et bs == |
15 err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)" |
15 err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)" |