Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Jinja/JVM/   (Archive of formal Proofs Version 2026-5©)  Datei vom 31.4.2026 mit Größe 960 B image not shown  

Quelle  JVMState.thy   Sprache: Isabelle

 

(*  Title:      Jinja/JVM/JVMState.thy

    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)


chapter ‹Jinja Virtual Machine \label{cha:jvm}›

section ‹State of the JVM›

theory JVMState imports "../Common/Objects" begin

subsection ‹Frame Stack›

type_synonym 
  pc = nat

type_synonym
  frame = "val list × val list × cname × mname × pc"
  ― ‹operand stack›
  ― ‹registers (including this pointer, method parameters, and local variables)›
  ― ‹name of class where current method is defined›
  ― ‹parameter types›
  ― ‹program counter within frame›

subsection ‹Runtime State›

type_synonym
  jvm_state = "addr option × heap × frame list"  
  ― ‹exception flag, heap, frames›
  
end

Messung V0.5 in Prozent
C=93 H=99 G=95

¤ Dauer der Verarbeitung: 0.11 Sekunden  (vorverarbeitet am  2026-09-29) ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

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 und die Messung sind noch experimentell.