Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: JVMState.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/JVM/JVMState.thy
    Author:     Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
*)

chapter \<open>Java Virtual Machine \label{cha:jvm}\<close>

section \<open>State of the JVM\<close>

theory JVMState
imports "../J/Conform"
begin

subsection \<open>Frame Stack\<close>
type_synonym opstack = "val list"
type_synonym locvars = "val list"
type_synonym p_count = nat

type_synonym
frame = "opstack \
          locvars \<times>
          cname \<times>
          sig \<times>
          p_count"

  \<comment> \<open>operand stack\<close>
  \<comment> \<open>local variables (including this pointer and method parameters)\<close>
  \<comment> \<open>name of class where current method is defined\<close>
  \<comment> \<open>method name + parameter types\<close>
  \<comment> \<open>program counter within frame\<close>

subsection \<open>Exceptions\<close>
definition raise_system_xcpt :: "bool \ xcpt \ val option" where
  "raise_system_xcpt b x \ raise_if b x None"

subsection \<open>Runtime State\<close>
type_synonym
  jvm_state = "val option \ aheap \ frame list" \ \exception flag, heap, frames\

subsection \<open>Lemmas\<close>

lemma new_Addr_OutOfMemory:
  "snd (new_Addr hp) = Some xcp \ xcp = Addr (XcptRef OutOfMemory)"
proof -
  obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
  moreover
  assume "snd (new_Addr hp) = Some xcp"
  ultimately
  show ?thesis by (auto dest: new_AddrD)
qed

end

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.