Java and the Java Virtual Machine: Definition, Verification, Validation

✍ Scribed by Prof. Dr. Robert F. Stärk, Dipl.-Inf. Joachim Schmid, Prof. Dr. Egon Börger (auth.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2001
• Tongue: English
• Leaves: 375
• Edition: 1
• Category: Library

✦ Synopsis

This book provides a high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including a standard compiler of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The description is structured into language layers and machine components. It comes with a natural executable refinement which can be used for testing code. The method developed for this purpose is based on Abstract State Machines (ASMs) and can be applied to other virtual machines and to other programming languages as well. The book is written for advanced students and for professionals and practitioners in research and development who need for their work a complete and transparent definition and an executable model of the language and of the virtual machine underlying its intended implementation.

✦ Table of Contents

Front Matter....Pages I-X
Introduction....Pages 1-13
Abstract State Machines....Pages 15-28
Front Matter....Pages 29-32
The imperative core Java I of Java....Pages 33-46
The procedural extension Java C of Java I ....Pages 47-69
The object-oriented extension $${\text{Jav}}{{\text{a}}\mathcal{O}}$$ of Java c ....Pages 71-85
The exception-handling extension Java ε of $${\text{Jav}}{{\text{a}}\mathcal{O}}$$ ....Pages 87-94
The concurrent extension Java T of Java ε ....Pages 95-110
Java is type safe....Pages 111-134
Front Matter....Pages 135-137
The JVM I submachine....Pages 139-146
The procedural extension JVM C of JVM I ....Pages 147-154
The object-oriented extension $${\text{JV}}{{\text{M}}\mathcal{O}}$$ of JVM c ....Pages 155-158
The exception-handling extension JVM ε of $${\text{JV}}{{\text{M}}\mathcal{O}}$$ ....Pages 159-164
Executing the JVM N ....Pages 165-166
Correctness of the compiler....Pages 167-203
Front Matter....Pages 205-207
The defensive virtual machine....Pages 209-222
Bytecode type assignments....Pages 223-271
The diligent virtual machine....Pages 273-287
The dynamic virtual machine....Pages 289-303
Back Matter....Pages 305-381

✦ Subjects

Programming Languages, Compilers, Interpreters; Software Engineering