|
Die Java Virtual Machine (JVM) bildet das Rückgrat der Programmiersprache
Java und ermöglicht erst Features von Java wie
Plattformunabhängigkeit
oder Schutz vor bösartigem Code. Nach einer kurzen Einführung in die
JVM wird eine mögliche Formalisierung einer Teilmenge der JVM, der
µJVM, aufgezeigt. Im Anschluss wird noch auf den Bytecode-Verifier
eingegangen und angerissen, wie man mittels der Formalisierung die Typsicherheit
der µJVM beweisen kann.
Literatur
- T. Lindholm, F. Yellin: The Java Virtual Machine Specification,
Addison-Wesley, 1999.
- T. Nipkow, D. von Oheimb, C. Pusch: µJava: Embedding a Programming
Language in a Theorem Prover.
|
|