products/sources/formale Sprachen/Isabelle/HOL/MicroJava/JVM/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: mf8nbo.bat   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      HOL/MicroJava/JVM/JVMExec.thy
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

section \<open>Program Execution in the JVM\<close>

theory JVMExec imports JVMExecInstr JVMExceptions begin


fun
  exec :: "jvm_prog \ jvm_state => jvm_state option"
\<comment> \<open>exec is not recursive. fun is just used for pattern matching\<close>
where
  "exec (G, xp, hp, []) = None"

| "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
  (let 
     i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc;
     (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs
   in Some (find_handler G xcpt' hp' frs'))"

| "exec (G, Some xp, hp, frs) = None" 


definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
              ("_ \ _ \jvm\ _" [61,61,61]60) where
  "G \ s \jvm\ t == (s,t) \ {(s,t). exec(G,s) = Some t}\<^sup>*"


text \<open>
  The start configuration of the JVM: in the start heap, we call a 
  method \<open>m\<close> of class \<open>C\<close> in program \<open>G\<close>. The 
  \<open>this\<close> pointer of the frame is set to \<open>Null\<close> to simulate
  a static method invokation.
\<close>
definition start_state :: "jvm_prog \ cname \ mname \ jvm_state" where
  "start_state G C m \
  let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
    (None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])"

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.38Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff