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.
This book provides a high-level desription of Java and of the Java Virtual Machine.
The first book to provide a rigorous mathematical analysis of Java Includes supplementary material: sn.pub/extras
Robert F. Stärk
C programming language Constraint Java Java Card Java Virtual Machine Natural programming programming language security testing validation virtual machine
From the reviews:"A professional Java programmer must know what his program exactly will do, if it is run on a Java Virtual Machine (JVM). To help these professionals, the book presents a mathematical framework using the notation of Abstract State Machines (ASMs). … it is addressed to professional software engineers and to advanced students who require a complete and exact definition of Java and of the behaviour of the JVM. With AsmGofer an interesting experimental system for program verification is available." (W. Brecht, Zentralblatt MATH, Vol. 978, 2002)
()