Skip to main content
SpringerLink
Log in

Java and the Java Virtual Machine

Definition, Verification, Validation

  • Textbook
  • © 2001

Overview

Authors:
  1. Robert F. Stärk

    1. Theoretische Informatik, ETH Zentrum, Zürich, Switzerland

    View author publications

    You can also search for this author in PubMed   Google Scholar

  2. Joachim Schmid

    1. Siemens AG, München, Germany

    View author publications

    You can also search for this author in PubMed   Google Scholar

  3. Egon Börger

    1. Dipartimento di Informatica, Università di Pisa, Pisa, Italy

    View author publications

    You can also search for this author in PubMed   Google Scholar

  • The first book to provide a rigorous mathematical analysis of Java

  • Includes supplementary material: sn.pub/extras

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 54.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (18 chapters)

  1. Front Matter

    Pages I-X
    Download chapter PDF

  2. Introduction

    1. Introduction

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 1-13

  3. Abstract State Machine

    1. Abstract State Machines

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 15-28

  4. Java

    1. Front Matter

      Pages 29-32
      Download chapter PDF

    2. The imperative core Java I of Java

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 33-46

    3. The procedural extension Java C of Java I

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 47-69

    4. The object-oriented extension \({\text{Jav}}{{\text{a}}_\mathcal{O}}\) of Java c

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 71-85

    5. The exception-handling extension Java ε of \({\text{Jav}}{{\text{a}}_\mathcal{O}}\)

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 87-94

    6. The concurrent extension Java T of Java ε

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 95-110

    7. Java is type safe

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 111-134

  5. Compilation of Java: The Trustful JVM

    1. Front Matter

      Pages 135-137
      Download chapter PDF

    2. The JVM I submachine

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 139-146

    3. The procedural extension JVM C of JVM I

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 147-154

    4. The object-oriented extension \({\text{JV}}{{\text{M}}_\mathcal{O}}\) of JVM c

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 155-158

    5. The exception-handling extension JVM ε of \({\text{JV}}{{\text{M}}_\mathcal{O}}\)

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 159-164

    6. Executing the JVM N

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 165-166

    7. Correctness of the compiler

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 167-203

  6. Bytecode Verification: The Secure JVM

    1. Front Matter

      Pages 205-207
      Download chapter PDF

    2. The defensive virtual machine

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 209-222

    3. Bytecode type assignments

      • Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 223-271
Back to top

Keywords

About this book

The origin of this book goes back to the Dagstuhl seminar on Logic for System Engineering, organized during the first week of March 1997 by S. Jiihnichen, J. Loeckx, and M. Wirsing. During that seminar, after Egon Borger's talk on How to Use Abstract State Machines in Software Engineering, Wolfram Schulte, at the time a research assistant at the University of Ulm, Germany, questioned whether ASMs provide anything special as a scientifically well­ founded and rigorous yet simple and industrially viable framework for high­ level design and analysis of complex systems, and for natural refinements of models to executable code. Wolfram Schulte argued, referring to his work with K. Achatz on A Formal Object-Oriented Method Inspired by Fusion and Object-Z [1], that with current techniques of functional programming and of axiomatic specification, one can achieve the same result. An intensive and long debate arose from this discussion. At the end of the week, it led Egon Borger to propose a collaboration on a real-life specification project of Wolfram Schulte's choice, as a comparative field test of purely functional­ declarative methods and of their enhancement within an integrated abstract state-based operational (ASM) approach. After some hesitation, in May 1997 Wolfram Schulte accepted the offer and chose as the theme a high-level specification of Java and of the Java Virtual Machine.

Reviews

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)

Authors and Affiliations

  • Theoretische Informatik, ETH Zentrum, Zürich, Switzerland

    Robert F. Stärk

  • Siemens AG, München, Germany

    Joachim Schmid

  • Dipartimento di Informatica, Università di Pisa, Pisa, Italy

    Egon Börger

Bibliographic Information

  • Book Title: Java and the Java Virtual Machine

  • Book Subtitle: Definition, Verification, Validation

  • Authors: Robert F. Stärk, Joachim Schmid, Egon Börger

  • DOI: https://doi.org/10.1007/978-3-642-59495-3

  • Publisher: Springer Berlin, Heidelberg

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer-Verlag Berlin Heidelberg 2001

  • Hardcover ISBN: 978-3-540-42088-0Published: 20 June 2001

  • Softcover ISBN: 978-3-642-63997-5Published: 23 August 2014

  • eBook ISBN: 978-3-642-59495-3Published: 06 December 2012

  • Edition Number: 1

  • Number of Pages: X, 381

  • Number of Illustrations: 13 b/w illustrations

  • Topics: Programming Techniques, Programming Languages, Compilers, Interpreters, Software Engineering

Publish with us

Policies and ethics

Back to top

Search

Navigation