| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Jinja/JVM/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 960 B |
|
Quelle JVMState.thySprache: 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
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09