Quellcode-Bibliothek 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

¤ 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.0.0Bemerkung: (vorverarbeitet am 2026-09-10) ¤

*Bot Zugriff

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.